Changeset 969


Ignore:
Timestamp:
Jun 15, 2011, 5:27:48 PM (8 years ago)
Author:
mulligan
Message:

more work on paper, nearly finished policy discussion

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2011/cpp-2011.tex

    r968 r969  
    99\usepackage{graphicx}
    1010\usepackage[colorlinks]{hyperref}
     11\usepackage{hyphenat}
    1112\usepackage[utf8x]{inputenc}
    1213\usepackage{listings}
     
    257258This function fails if and only if an internal call to \texttt{assembly\_1\_pseudoinstruction} fails:
    258259\begin{lstlisting}
    259 definition sigma0: pseudo_assembly_program
    260                   $\rightarrow$ option (nat $\times$ (nat $\times$ (BitVectorTrie Word 16))) := $\ldots$
     260definition sigma0:
     261  pseudo_assembly_program $\rightarrow$ option (nat $\times$ (nat $\times$ (BitVectorTrie Word 16))) := $\ldots$
    261262\end{lstlisting}
    262263
    263264We eventually lift this to functions from program counters to program counters:
    264265\begin{lstlisting}
    265 definition sigma_safe: pseudo_assembly_program
    266                       $\rightarrow$ option (Word $\rightarrow$ Word) := $\ldots$
     266definition sigma_safe:
     267  pseudo_assembly_program $\rightarrow$ option (Word $\rightarrow$ Word) := $\ldots$
    267268\end{lstlisting}
    268269
     
    270271As mentioned, \texttt{sigma\_safe} can only fail if an assembly program fails to be assembled:
    271272\begin{lstlisting}
    272 definition policy_ok := $\lambda$policy. $\lambda$p. sigma_safe policy p $\neq$ None $\ldots$.
    273 \end{lstlisting}
    274 
    275 Finally, we obtain \texttt{sigma}, a map from program counters to program counters, which is guranteed not to fail, as we must provide a proof that our policy at hand is a `good policy'.
    276 \begin{lstlisting}
    277 definition sigma:
    278  ∀p:pseudo_assembly_program.
    279   ∀policy. policy_ok policy p. Word → Word
    280 \end{lstlisting}
    281 
     273definition policy_ok := $\lambda$p. sigma_safe p $\neq$ None $\ldots$.
     274\end{lstlisting}
     275
     276Finally, we obtain \texttt{sigma}, a map from program counters to program counters, which is guranteed not to fail as we internally provide a that
     277\begin{lstlisting}
     278definition sigma: pseudo_assembly_program $\rightarrow$ Word $\rightarrow$ Word := $\ldots$
     279\end{lstlisting}
     280
     281An \texttt{internal\_pseudo\_address\_map} positions in the memory of a \texttt{PseudoStatus} with a physical memory address.
     282\begin{lstlisting}
     283definition internal_pseudo_address_map := list (BitVector 8).
     284\end{lstlisting}
     285
     286We use \texttt{internal\_pseudo\_address\_map}s to convert the lower internal RAM of a \texttt{PseudoStatus} into the lower internal RAM of a \texttt{Status}.
     287Notice, the MCS-51's internal RAM is addressed with a 7-bit `byte'.
     288% dpm: ugly English, fix
     289The whole of the internal RAM space is addressed with bytes: the first bit is used to distinguish between the programmer addressing low and high internal memory.
    282290\begin{lstlisting}
    283291axiom low_internal_ram_of_pseudo_low_internal_ram:
    284  ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
    285 \end{lstlisting}
    286 
    287 CSC: no option using policy
     292  internal_pseudo_address_map $\rightarrow$ BitVectorTrie Byte 7 $\rightarrow$ BitVectorTrie Byte 7.
     293\end{lstlisting}
     294A similar axiom exists for high internal RAM.
     295
     296Next, we are able to translate \texttt{PseudoStatus} records into \texttt{Status} records using \texttt{status\_of\_pseudo\_status}.
     297Translating a \texttt{PseudoStatus}'s code memory requires we expand pseudoinstructions and then assemble to obtain a trie of bytes.
     298This can fail, as mentioned, in a limited number of situations, related to improper use of labels in an assembly program.
     299However, it is possible to `tighten' the type of \texttt{status\_of\_pseudo\_status}, removing the option type, by using the fact that if any `good policy' exists, assembly will never fail.
    288300\begin{lstlisting}
    289301definition status_of_pseudo_status:
     
    291303\end{lstlisting}
    292304
     305After fetching an assembly instruction we must update any \texttt{internal\_pseudo\hyp{}\_address\_map}s that may be laying around.
     306This is done with the following function:
    293307\begin{lstlisting}
    294308definition next_internal_pseudo_address_map0:
     
    296310\end{lstlisting}
    297311
    298 CSC: no 2nd, 3rd options using policy
    299 \begin{lstlisting}
    300  ∀M,M',ps,s,s''.
    301   next_internal_pseudo_address_map M ps = Some ... M' →
    302   status_of_pseudo_status M ps = Some ... s →
    303   status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory ... ps)) ps) = Some ... s'' →
    304    ∃n. execute n s = s''.
    305 \end{lstlisting}
     312Finally, we are able to state and prove our main theorem regarding
     313\begin{lstlisting}
     314lemma main_thm:
     315  ∀M,M',ps,s,s''.
     316    next_internal_pseudo_address_map M ps = Some ... M' $\rightarrow$
     317      status_of_pseudo_status M ps = Some ... s $\rightarrow$
     318        status_of_pseudo_status M'
     319          (execute_1_pseudo_instruction
     320            (ticks_of (code_memory ... ps)) ps) = Some ... s'' $\rightarrow$
     321              $\exists$n. execute n s = s''.
     322\end{lstlisting}
     323
     324% ---------------------------------------------------------------------------- %
     325% SECTION                                                                      %
     326% ---------------------------------------------------------------------------- %
     327\subsection{Proof of correctness}
     328\label{subsect.proof.of.correctness}
    306329
    307330CSC: no options using policy
Note: See TracChangeset for help on using the changeset viewer.