Changeset 1019 for src/ASM/CPP2011

Timestamp:

Jun 21, 2011, 11:39:12 AM (9 years ago)

Author:

sacerdot

Message:

Finished rewriting of Section 3.

File:

• src/ASM/CPP2011/cpp-2011.tex (modified) (6 diffs)

src/ASM/CPP2011/cpp-2011.tex

@@ -331 +331 @@
 % SECTION                                                                      %
 % ---------------------------------------------------------------------------- %
-\subsection{Total correctness of the assembler}
+\subsection{Correctness of the assembler with respect to fetching}
 \label{subsect.total.correctness.of.the.assembler}
 
 Using our policies, we now work toward proving the total correctness of the assembler.
-By total correctness, we mean that the assembly process does not change the semantics of an assembly program.
+By total correctness, we mean that the assembly process never fails when
+provided with a good strategy and that it does not change the semantics of
+a certain class of well behaved assembly program.
 Naturally, this necessitates keeping some sort of correspondence between addresses at the assembly level and addresses at the machine code level.
 For this, we use the \texttt{sigma} machinery defined at the end of Subsection~\ref{subsect.policies}.
 
-We expand pseudoinstructions using the function \texttt{expand\_pseudo\_instruction}.
-This function accepts a `policy decision'---an element of type \texttt{jump\_length}---that is used when expanding a \texttt{Call}, \texttt{Jmp} or conditional jump to a label into the correct machine instruction.
-This \texttt{policy\_decision} is asssumed to originate from a policy as defined in Subsection~\ref{subsect.policies}.
+We expand pseudoinstructions using the function \texttt{expand\_pseudo\_instruction} that takes a program made of pseudo-instructions, a good policy for
+the program and a pointer to the pseudo memory. It returns the list of
+instructions that correspond to the pseudo-instruction referenced by the
+pointer. The policy is used to decide how to expand
+\texttt{Call}s, \texttt{Jmp}s and conditional jumps. The function is given
+a dependent type that incorporates its specification. The pre and
+post-conditions are omitted in the paper due to lack of space. We show them
+as an example for the next function, \texttt{build\_maps}.
 \begin{lstlisting}
 definition expand_pseudo_instruction:
-  ∀lookup_labels, lookup_datalabels, pc, policy_decision.
-    pseudo_instruction $\rightarrow$ list instruction := $\ldots$
+  ∀program.∀pol:policy program.∀ppc:Word. ... $\Sigma$res.list instruction. ...
+   := $\ldots$
 \end{lstlisting}
 
@@ -363 +370 @@
 \end{lstlisting}
 The rather complex type of \texttt{build\_maps} owes to our use of Matita's Russell facility to provide a strong specification for the function in the type (c.f. the use of sigma types, through which Russell is implemented in Matita).
-In particular, we express that any label should only appear exactly in any assembly program, and looking up a label in the newly created map is the same as applying the \texttt{sigma} function, recording the correspondence between pseudo program counters and program counters.
+In particular, we express that for all labels that appear exactly once in any assembly program, the newly created map used in the implementation and the
+stronger \texttt{sigma} function used in the specification agree.
 
 Using \texttt{build\_maps}, we can express the following lemma, expressing the correctness of the assembly function:
@@ -410 +418 @@
 Or, in plainer words, assembling and then immediately fetching again gets you back to where you started.
 
-Lemma \texttt{fetch\_assembly\_pseudo} establishes a basic relationship between \texttt{expand\_pseudo\_instruction} and \texttt{assembly\_1\_pseudoinstruction}:
-\begin{lstlisting}
-lemma fetch_assembly_pseudo: $\forall$p. $\forall$pol: policy p. $\forall$ppc, lk_lbl, lk_dlbl.
-  $\forall$pi, code_memory, len, assembled, instructions, pc.
-  let exp := pol ppc in
-  let expand := expand_pseudo_instruction lk_lbls lk_dlbl pc exp pi in
-  let ass := assembly_1_pseudoinstruction p pol ppc pc lk_lbl lk_dlbl pi in
-  Some ? instructions = expand $\rightarrow$
-  Some $\ldots$ $\langle$len, assembled$\rangle$ = ass $\rightarrow$
-  encoding_check code_memory pc (pc + len) assembled $\rightarrow$
-    fetch_many code_memory (pc + len) pc instructions.
+Lemma \texttt{fetch\_assembly\_pseudo} (whose type is shown here slightly
+simplified) is obtained by composition of
+\texttt{expand\_pseudo\_instruction} and
+\texttt{assembly\_1\_pseudoinstruction}:
+\begin{lstlisting}
+lemma fetch_assembly_pseudo:
+ ∀program.∀pol:policy program.∀ppc.∀code_memory.
+  let pi := fst (fetch_pseudo_instruction (snd program) ppc) in
+  let instructions := expand_pseudo_instruction program pol ppc ... in
+  let $\langle$len,assembled$\rangle$ := assembly_1_pseudoinstruction program pol ppc ... in
+  encoding_check code_memory pc (pc + len) assembled →
+  fetch_many code_memory (pc + len) pc instructions.
 \end{lstlisting}
 Here, \texttt{len} is the number of machine code instructions the pseudoinstruction at hand has been expanded into, and \texttt{encoding\_check} is a recursive function that checks that assembled machine code is correctly stored in code memory.
@@ -427 +436 @@
 
 Intuitively, Lemma \texttt{fetch\_assembly\_pseudo} can be read as follows.
-Suppose our policy \texttt{jump\_expansion} dictates that the pseudoinstruction indexed by the pseudo program counter \texttt{ppc} in assembly program \texttt{program} gives us the policy decision \texttt{jexp}.
-Further, suppose we expand the pseudoinstruction at \texttt{ppc} with the policy decision \texttt{jexp}, obtaining an (optional) list of machine code instructions \texttt{exp}.
-Suppose we also assemble the pseudoinstruction at \texttt{ppc} to obtain \texttt{ass}, a list of bytes.
+Suppose our policy \texttt{jump\_expansion} dictates that the pseudoinstruction indexed by the pseudo program counter \texttt{ppc} in assembly program \texttt{program} gives us the policy decision \texttt{pol}.
+Further, suppose we expand the pseudoinstruction at \texttt{ppc} with the policy decision \texttt{pol}, obtaining the list of machine code instructions \texttt{instructions}.
+Suppose we also assemble the pseudoinstruction at \texttt{ppc} to obtain \texttt{assembled}, a list of bytes.
 Then, we check with \texttt{fetch\_many} that the number of machine instructions that were fetched matches the number of instruction that \texttt{expand\_pseudo\_instruction} expanded.
 
-At first sight, Lemma \texttt{fetch\_assembly\_pseudo2} appears to nearly establish the correctness of the assembler:
-\begin{lstlisting}
-lemma fetch_assembly_pseudo2: $\forall$p. $\forall$pol: policy p. $\forall$assembled, costs, labels.
-  Some $\ldots$ $\langle$labels, costs$\rangle$ = build_maps program $\rightarrow$
-  Some $\ldots$ $\langle$assembled, costs$\rangle$ = assembly program $\rightarrow$ $\forall$ppc.
+The final lemma in this series is
+\texttt{fetch\_assembly\_pseudo2} that combines the previous one with the
+correctness of the operations that load the object code in the processor
+memory. At first, the lemmas appears to nearly establish the correctness of
+the assembler:
+\begin{lstlisting}
+lemma fetch_assembly_pseudo2:
+ ∀program,pol,ppc.
+  let $\langle$labels,costs$\rangle$ := build_maps program pol in
+  let assembled := \fst (assembly program pol) in
   let code_memory := load_code_memory assembled in
-  let preamble := $\pi_1$ program in
-  let data_labels := construct_datalabels preamble in
-  let lk_labels :=
-    λx. sigma program (address_of_word_labels_code_mem ($\pi_2$ program) x) in
-  let lk_dlabels := λx. lookup ? ? x data_labels (zero ?) in
-  let expansion := jump_expansion ppc program in
-  let $\langle$pi, newppc$\rangle$ := fetch_pseudo_instruction ($\pi_2$ program) ppc in
-  let ppc' := sigma program ppc in
-  let newppc' := sigma program newppc in
-  let instructions' :=
-    expand_pseudo_instruction lk_labels lk_dlabels ppc' expansion pi in
-  let fetched := $\lambda$instr. fetch_many code_memory newppc' ppc' instr in
-    $\exists$instrs. Some ? instrs = instructions' $\wedge$ fetched instrs.
+  let data_labels := construct_datalabels (\fst program) in
+  let lookup_labels :=
+    λx. sigma $\ldots$ pol (address_of_word_labels_code_mem (\snd program) x) in
+  let lookup_datalabels := λx. lookup ? ? x data_labels (zero ?) in
+  let $\langle$pi,newppc$\rangle$ := fetch_pseudo_instruction (\snd program) ppc in
+  let instructions ≝ expand_pseudo_instruction program pol ppc ... in
+   fetch_many code_memory (sigma program pol newppc)
+     (sigma program pol ppc) instructions.
 \end{lstlisting}
 
 Intuitively, we may read \texttt{fetch\_assembly\_pseudo2} as follows.
-Suppose we are able to successfully assemble an assembly program using \texttt{assembly} and produce a code memory, \texttt{code\_memory}.
-Then there exists some list of machine instructions equal to the expansion of a pseudoinstruction and the number of machine instructions that need to be fetched is equal to the number of machine instructions that the pseudoinstruction was expanded into.
-
-However, this property is \emph{not} strong enough to establish that the semantics of an assembly program has been preserved by the assembly process.
-In particular, \texttt{fetch\_assembly\_pseudo2} says nothing about how memory addresses evolve during assembly.
-Memory addresses in one memory space may be mapped to memory addresses in a completely different memory space during assembly.
-To handle this problem, we need some more machinery in order to track how memory addresses are moved around, and to record a correspondence between addresses at the pseudo assembly level and the machine code level.
-
-We use an \texttt{internal\_pseudo\_address\_map} for this purpose.
-An \texttt{internal\_pseudo\_address\_map} associates memory addresses in the lower internal RAM of a \texttt{PseudoStatus} with a physical memory address at the machine code level:
-\begin{lstlisting}
-definition internal_pseudo_address_map := list (BitVector 8).
-\end{lstlisting}
-
-We use a map associating memory addresses, of type \texttt{internal\_pseudo\_address\_map}, to convert the lower internal RAM of a \texttt{PseudoStatus} into the lower internal RAM of a \texttt{Status}.
-The actual conversion process is performed by \texttt{low\_internal\_ram\_of\_pseudo\_low\_internal\_ram}:\footnote{An associated set of axioms describe how \texttt{low\_internal\_ram\_of\_pseudo\_low\_internal\_ram} behaves.  This is a form of parametricity.  We don't care about the particulars of the conversion functions, as long as they behave in accordance with our axioms.}
+Suppose we are able to successfully assemble an assembly program using \texttt{assembly} and produce a code memory, \texttt{code\_memory}. The, fetching
+a pseudo-instruction from the pseudo-code memory at address \texttt{ppc}
+corresponds to fetching a sequence of instructions from the real code memory
+at address \texttt{sigma program pol ppc}. The fetched sequence is granted
+to be the expansion of the pseudo-instruction, according to the good policy
+\texttt{pol}.
+
+However, this property is \emph{not} strong enough to establish that the semantics of an assembly program has been preserved by the assembly process since it
+does not establish the correspondence between the semantics of a
+pseudo-instruction and that of its expansion. In particular, the two semantics
+differ on instructions that \emph{could} directly manipulate program
+addresses.
+
+\subsection{Total correctness for well-behaved assembly programs} 
+In any reasonable assembly language addresses in code memory are just data that
+can be manipulated in multiple ways by the program. An assembly program can
+forge constant addresses, compare addresses, move addresses around,
+shift existent addresses or apply logical and arithmetical operations
+to them. Every optimizing assembler is allowed to modify the code memory.
+Hence only the semantics of a few of the former operations is preserved by
+an optimizing compiler. Moreover, the problem of characterizing well behaved
+programs is clearly undecidable.
+
+To obtain a reasonable statement of correctness for our compiler, we need to
+trace the memory locations (and, potentially, registers) that contain memory
+addresses. This is necessary for two purposes. The first one is to detect
+(at run time) misbehaved programs that only manipulate addresses in well
+behaved ways, according to some safe approximation of well behavedness.
+The second one is to compute statuses that correspond to pseudo-statues:
+not only the content of the program counter, but also the content of all
+traced locations must be translated applying the \texttt{sigma} map; all
+the remaining memory cells are copied verbatim.
+
+For instance, after a function call, the two bytes that form the return
+pseudo-address are pushed on top of the stack, i.e. in internal RAM.
+This pseudo-internal RAM corresponds to an internal RAM where the stack
+holds the real addresses after optimization, and all the other values untouched.
+
+We use an \texttt{internal\_pseudo\_address\_map}
+to trace addresses of code memory addresses in internal RAM.
+The current code is parametric on the implementation of the map itself.
+\begin{lstlisting}
+axiom internal_pseudo_address_map: Type[0].
+\end{lstlisting}
+
+The \texttt{low\_internal\_ram\_of\_pseudo\_low\_internal\_ram} function
+converts the lower internal RAM of a \texttt{PseudoStatus} into the
+lower internal RAM of a \texttt{Status}. A similar one exists for higher
+internal RAM. Note that both RAM segments are index using addresses 7-bits
+long. The function is currently axiomatized and an associated
+set of axioms prescribe the behaviour of the function.
 \begin{lstlisting}
 axiom low_internal_ram_of_pseudo_low_internal_ram:
   internal_pseudo_address_map $\rightarrow$ BitVectorTrie Byte 7 $\rightarrow$ BitVectorTrie Byte 7.
 \end{lstlisting}
-A similar axiom exists for high internal RAM.
-
-Notice, the MCS-51's internal RAM is addressed with a 7-bit `byte'.
-% dpm: ugly English, fix
-The 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.
 
 Next, we are able to translate \texttt{PseudoStatus} records into \texttt{Status} records using \texttt{status\_of\_pseudo\_status}.
 Translating a \texttt{PseudoStatus}'s code memory requires we expand pseudoinstructions and then assemble to obtain a trie of bytes.
-This should never fail, providing that our policy is correct:
+This never fails, providing that our policy is correct:
 \begin{lstlisting}
 definition status_of_pseudo_status: internal_pseudo_address_map $\rightarrow$
@@ -488 +527 @@
 \end{lstlisting}
 
-After fetching an assembly instruction we must update any \texttt{internal\_pseudo\hyp{}\_address\_map}s that may be laying around.
-This is done with the following function:
+The \texttt{next\_internal\_pseudo\_address\_map} function is responsible for
+monitoring at run time the behaviour of pseudo-assembly programs to detect
+the well behaved ones. It returns the new map that traces memory addresses
+in internal RAM after execution of the next pseudo-instruction. It fails when
+the instruction tampers with memory addresses in unticipated (but potentially
+correct) ways. It thus decides membership to a correct but not complete
+subset of well behaved programs.
 \begin{lstlisting}
 definition next_internal_pseudo_address_map: internal_pseudo_address_map
@@ -507 +551 @@
 \begin{lstlisting}
 theorem main_thm:
-  ∀M,M',ps,s,s''.
-    next_internal_pseudo_address_map M ps = Some $\ldots$ M' $\rightarrow$
-      status_of_pseudo_status M ps = Some $\ldots$ s $\rightarrow$
-        status_of_pseudo_status M'
-          (execute_1_pseudo_instruction 
-            (ticks_of (code_memory $\ldots$ ps)) ps) = Some $\ldots$ s'' $\rightarrow$
-              $\exists$n. execute n s = s''.
-\end{lstlisting}
-The statement can be given an intuitive reading as follows.
-Suppose our \texttt{PseudoStatus}, \texttt{ps}, can be successfully converted into a \texttt{Status}, \texttt{s}.
-Suppose further that, after executing a single assembly instruction and converting the resulting \texttt{PseudoStatus} into a \texttt{Status}, making sure to map memory addresses at the pseudo assembly level to memory addresses at the machine level correctly, we obtain \texttt{s''}, being careful to track the number of ticks executed with \texttt{ticks\_of}.
-Then, there exists some number \texttt{n}, so that executing \texttt{n} machine code instructions in \texttt{Status} \texttt{s} gives us \texttt{Status} \texttt{s''}.
-
-Theorem \texttt{main\_thm} establishes the correctness of the assembly process.
+ ∀M,M':internal_pseudo_address_map.∀ps.∀pol: policy ps.
+  next_internal_pseudo_address_map M ps = Some $\ldots$ M' →
+   ∃n.
+      execute n (status_of_pseudo_status M ps pol)
+    = status_of_pseudo_status M'
+       (execute_1_pseudo_instruction (ticks_of (code_memory $\ldots$ ps) pol) ps)
+       [pol].
+\end{lstlisting}
+The statement is standard for forward simulation, but restricted to
+\texttt{PseudoStatuses} \texttt{ps} whose next instruction to be executed is
+well-behaved with respect to the \texttt{internal\_pseudo\_address\_map} \texttt{M}.
+
+Theorem \texttt{main\_thm} establishes the total correctness of the assembly process and can simply be lifted to the forward simulation of an arbitrary number
+of well behaved steps on the assembly program.
 
 % ---------------------------------------------------------------------------- %