Changeset 1012


Ignore:
Timestamp:
Jun 21, 2011, 12:33:55 AM (8 years ago)
Author:
mulligan
Message:

just a few things left to change

File:
1 edited

Legend:

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

    r1011 r1012  
    344344    pseudo_instruction $\rightarrow$ list instruction := $\ldots$
    345345\end{lstlisting}
     346
    346347
    347348\begin{lstlisting}
     
    366367\end{lstlisting}
    367368
    368 % dpm todo
     369Theorem \texttt{fetch\_assembly} establishes that the \texttt{fetch} and \texttt{assembly1} functions interact correctly.
     370The \texttt{fetch} function, as its name implies, fetches the instruction indexed by the program counter in the code memory, while \texttt{assembly1} maps a single instruction to its byte encoding:
    369371\begin{lstlisting}
    370372theorem fetch_assembly: $\forall$pc, i, cmem, assembled.
     
    379381       eq_bv $\ldots$ pc' (pc + len)) = true.
    380382\end{lstlisting}
     383In particular, we read \texttt{fetch\_assembly} as follows.
     384Given an instruction, \texttt{i}, we first assemble the instruction to obtain \texttt{assembled}, checking that the assembled instruction was stored in code memory correctly.
     385Fetching from code memory, we obtain \texttt{fetched}, a tuple consisting of the instruction, new program counter, and the number of ticks this instruction will take to execute.
     386Deconstructing these tuples, we finally check that the fetched instruction is the same instruction that we began with, and the number of ticks this instruction will take to execute is the same as the result returned by a lookup function, \texttt{ticks\_of\_instruction}, devoted to tracking this information.
     387Or, in plainer words, assembling and then immediately fetching again gets you back to where you started.
    381388
    382389Lemma \texttt{fetch\_assembly\_pseudo} establishes a basic relationship between \texttt{expand\_pseudo\_instruction} and \texttt{assembly\_1\_pseudoinstruction}:
     
    400407Further, suppose we expand the pseudoinstruction at \texttt{ppc} with the policy decision \texttt{jexp}, obtaining an (optional) list of machine code instructions \texttt{exp}.
    401408Suppose we also assemble the pseudoinstruction at \texttt{ppc} to obtain \texttt{ass}, a list of bytes.
    402 Then, under the assumption that neither the expansion of the pseudoinstruction to obtain \texttt{exp}, nor the assembly of the pseudoinstruction to obtain \texttt{ass}, failed, 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.
     409Then, 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.
    403410
    404411At first sight, Lemma \texttt{fetch\_assembly\_pseudo2} appears to nearly establish the correctness of the assembler:
     
    422429    $\exists$instrs. Some ? instrs = instructions' $\wedge$ fetched instrs.
    423430\end{lstlisting}
     431
    424432Intuitively, we may read \texttt{fetch\_assembly\_pseudo2} as follows.
    425433Suppose we are able to successfully assemble an assembly program using \texttt{assembly} and produce a code memory, \texttt{code\_memory}.
     
    429437In particular, \texttt{fetch\_assembly\_pseudo2} says nothing about how memory addresses evolve during assembly.
    430438Memory addresses in one memory space may be mapped to memory addresses in a completely different memory space during assembly.
    431 To handle this problem, we need some more machinery.
     439To 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.
    432440
    433441We use an \texttt{internal\_pseudo\_address\_map} for this purpose.
    434 An \texttt{internal\_pseudo\_address\_map} associates positions in the memory of a \texttt{PseudoStatus} with a physical memory address:
     442An \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:
    435443\begin{lstlisting}
    436444definition internal_pseudo_address_map := list (BitVector 8).
    437445\end{lstlisting}
    438 We 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}.
     446
     447We 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}.
    439448The 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.}
    440 
    441449\begin{lstlisting}
    442450axiom low_internal_ram_of_pseudo_low_internal_ram:
     
    451459Next, we are able to translate \texttt{PseudoStatus} records into \texttt{Status} records using \texttt{status\_of\_pseudo\_status}.
    452460Translating a \texttt{PseudoStatus}'s code memory requires we expand pseudoinstructions and then assemble to obtain a trie of bytes.
    453 This can fail, as mentioned, in a limited number of situations, related to improper use of labels in an assembly program.
    454 However, 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.
    455 \begin{lstlisting}
    456 definition status_of_pseudo_status:
    457  internal_pseudo_address_map → PseudoStatus → option Status
    458 \end{lstlisting}
     461This should never fail, providing that our policy is correct:
     462\begin{lstlisting}
     463definition status_of_pseudo_status: internal_pseudo_address_map $\rightarrow$
     464  $\forall$ps:PseudoStatus. policy (code_memory $\ldots$ ps) $\rightarrow$ Status
     465\end{lstlisting}
     466
    459467After fetching an assembly instruction we must update any \texttt{internal\_pseudo\hyp{}\_address\_map}s that may be laying around.
    460468This is done with the following function:
     
    463471  $\rightarrow$ PseudoStatus $\rightarrow$ option internal_pseudo_address_map
    464472\end{lstlisting}
     473
     474The function \texttt{ticks\_of} computes how long---in clock cycles---a pseudoinstruction will take to execute when expanded in accordance with a given policy.
     475The function returns a pair of natural numbers, needed for recording the execution times of each branch of a conditional jump.
     476\begin{lstlisting}
     477definition ticks_of:
     478  $\forall$p:pseudo_assembly_program. policy p $\rightarrow$ Word $\rightarrow$ nat $\times$ nat := $\ldots$
     479\end{lstlisting}
     480
    465481Finally, we are able to state and prove our main theorem.
    466 This relates the execution of a single assembly instruction and the execution of (possibly) many machine code instructions.
    467 That is, the assembly process preserves the semantics of an assembly program, as it is translated into machine code:
     482This relates the execution of a single assembly instruction and the execution of (possibly) many machine code instructions, as long .
     483That is, the assembly process preserves the semantics of an assembly program, as it is translated into machine code, as long as we are able to track memory addresses properly:
    468484\begin{lstlisting}
    469485theorem main_thm:
     
    478494The statement can be given an intuitive reading as follows.
    479495Suppose our \texttt{PseudoStatus}, \texttt{ps}, can be successfully converted into a \texttt{Status}, \texttt{s}.
    480 Suppose further that, after executing a single assembly instruction and converting the resulting \texttt{PseudoStatus} into a \texttt{Status}, we obtain \texttt{s''}, being careful to track the number of ticks executed.
     496Suppose 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}.
    481497Then, 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''}.
     498
    482499Theorem \texttt{main\_thm} establishes the correctness of the assembly process.
    483500
     
    555572The bulk of the proof described herein is contained in a single file, \texttt{AssemblyProof.ma}, consisting of approximately 3000 lines of Matita source.
    556573
     574We admit to using a number of axioms in our development.
     575We do not believe the use of these axioms has been particularly onerous---very few concern anything more interesting than, say, stating that converting from a natural number to a bitvector and back again is the identity---and what axioms remain are rapidly being closed as work continues.
     576
    557577\bibliography{cpp-2011.bib}
    558578
Note: See TracChangeset for help on using the changeset viewer.