Changeset 974


Ignore:
Timestamp:
Jun 16, 2011, 11:24:27 AM (8 years ago)
Author:
mulligan
Message:

more added

Location:
src/ASM/CPP2011
Files:
2 edited

Legend:

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

    r973 r974  
    224224To a degree of approximation, the assembler on an assembly program, consisting of $n$ pseudoinstructions $\mathtt{P_i}$ for $1 \leq i \leq n$, works as in the following diagram:
    225225\begin{displaymath}
    226 [\mathtt{P_1}, \ldots \mathtt{P_n}] \xrightarrow{\left(\mathtt{P_i} \xrightarrow{\mbox{\fontsize{7}{9}\selectfont$\mathtt{expand}$}} \mathtt{[I_1^i, \ldots I^q_i]} \xrightarrow{\mbox{\fontsize{7}{9}\selectfont$\mathtt{assembly1}^*$}} \mathtt{[0110]}\right)^{*}} \mathtt{[010101]}
     226[\mathtt{P_1}, \ldots \mathtt{P_n}] \xrightarrow{\mathtt{flatten}\left(\mathtt{P_i} \xrightarrow{\mbox{\fontsize{7}{9}\selectfont$\mathtt{expand}$}} \mathtt{[I_1^i, \ldots I^q_i]} \xrightarrow{\mbox{\fontsize{7}{9}\selectfont$\mathtt{assembly1}^*$}} \mathtt{[0110]}\right)^{*}} \mathtt{[010101]}
    227227\end{displaymath}
    228 
    229228Here $\mathtt{I^i_j}$ for $1 \leq j \leq q$ are the $q$ machine code instructions obtained by expanding, with \texttt{expand\_pseudo\_instruction}, a single pseudoinstruction.
    230229Each machine code instruction $\mathtt{I^i_j}$ is then assembled, using the \texttt{assembly1} function, into a list of bytes.
    231230This process is iterated for each pseudoinstruction, before the lists are flattened into a single bit list representation of the original assembly program.
     231
     232By inspecting the above diagram, it would appear that the best way to proceed with a proof that the assembly process does not change the semantics of an assembly program is via a decomposition of the problem into two subproblems.
     233Namely, we first expand any and all pseudoinstructions into lists of machine instructions, and provide a proof that this process does not change our program's semantics.
     234Finally, we assemble all machine code instructions into machine code---lists of bytes---and prove once more that this process does not have an adverse effect on a program's semantics.
     235By composition, we then have that the whole assembly process is semantics preserving.
     236
     237This is a tempting approach to the proof, but ultimately the wrong approach.
     238In particular, it is important that we track how the program counter indexing into the assembly program, and the machine's program counter evolve, so that we can relate them.
     239Expanding pseudoinstructions requires that the machine's program counter be incremented by $n$ steps, for $1 \leq n$, for every increment of the assembly program's program counter.
     240Keeping track of the correspondence between the two program counters quickly becomes unfeasible using a compositional approach, and hence the proof must be monolithic.
    232241
    233242% ---------------------------------------------------------------------------- %
     
    256265This function fails if and only if an internal call to \texttt{assembly\_1\_pseudoinstruction} fails:
    257266\begin{lstlisting}
    258 definition sigma0:
    259   pseudo_assembly_program $\rightarrow$ option (nat $\times$ (nat $\times$ (BitVectorTrie Word 16))) := $\ldots$
     267definition sigma0: pseudo_assembly_program
     268  $\rightarrow$ option (nat $\times$ (nat $\times$ (BitVectorTrie Word 16))) := $\ldots$
    260269\end{lstlisting}
    261270We eventually lift this to functions from program counters to program counters:
     
    273282definition sigma: pseudo_assembly_program $\rightarrow$ Word $\rightarrow$ Word := $\ldots$
    274283\end{lstlisting}
     284
     285% ---------------------------------------------------------------------------- %
     286% SECTION                                                                      %
     287% ---------------------------------------------------------------------------- %
     288\subsection{Total correctness of the assembler}
     289\label{subsect.total.correctness.of.the.assembler}
     290
     291CSC: no options using policy
     292\begin{lstlisting}
     293lemma fetch_assembly_pseudo2: $\forall$program, assembled, costs, labels.
     294  Some $\ldots$ $\langle$labels,costs$\rangle$ = build_maps program $\rightarrow$
     295  Some $\ldots$ $\langle$assembled,costs$\rangle$ = assembly program $\rightarrow$ $\forall$ppc.
     296  let code_memory := load_code_memory assembled in
     297  let preamble := $\pi_1$ program in
     298  let data_labels := construct_datalabels preamble in
     299  let lk_labels :=
     300    λx. sigma program (address_of_word_labels_code_mem ($\pi_2$ program) x) in
     301  let lk_dlabels := λx. lookup ? ? x data_labels (zero ?) in
     302  let expansion := jump_expansion ppc program in
     303  let $\langle$pi,newppc$\rangle$ := fetch_pseudo_instruction ($\pi_2$ program) ppc in
     304  let ppc' := sigma program ppc in
     305  let newppc' := sigma program newppc in
     306  let instructions' :=
     307    expand_pseudo_instruction lk_labels lk_dlabels ppc' expansion pi in
     308  let fetched := fetch_many code_memory newppc' ppc' instructions in
     309    $\exists$instructions. Some ? instructions = instructions' $\wedge$ fetched.
     310\end{lstlisting}
     311
     312\begin{lstlisting}
     313definition expand_pseudo_instruction:
     314  ∀lookup_labels, lookup_datalabels, pc, policy_decision.
     315    pseudo_instruciton $\rightarrow$ option list instruction := $\ldots$
     316\end{lstlisting}
     317
     318\begin{lstlisting}
     319axiom assembly_ok: ∀program,assembled,costs,labels.
     320  Some $\ldots$ $\langle$labels, costs$\rangle$ = build_maps program $\rightarrow$
     321  Some $\ldots$ $\langle$assembled, costs$\rangle$ = assembly program $\rightarrow$
     322  let code_memory := load_code_memory assembled in
     323  let preamble := $\pi_1$ program in
     324  let datalabels := construct_datalabels preamble in
     325  let lk_labels :=
     326    $\lambda$x. sigma program (address_of_word_labels_code_mem ($\pi_2$ program) x) in
     327  let lk_dlabels := $\lambda$x. lookup ? ? x datalabels (zero ?) in
     328   ∀ppc,len,assembledi.
     329    let $\langle$pi, newppc$\rangle$ := fetch_pseudo_instruction ($\pi_2$ program) ppc in
     330    let assembly' := assembly_1_pseudoinstruction program ppc
     331      (sigma program ppc) lk_labels lk_dlabels pi in
     332    let newpc := (sigma program ppc) + len in
     333    let echeck :=
     334      encoding_check code_memory (sigma program ppc) slen assembledi in
     335     Some $\ldots$ $\langle$len, assembledi$\rangle$ = assembly' $\rightarrow$
     336      echeck $\wedge$ sigma program newppc = newpc.
     337\end{lstlisting}
     338
     339\begin{lstlisting}
     340lemma fetch_assembly_pseudo: $\forall$program, ppc, lk_labels, lk_dlabels.
     341  $\forall$pi, code_memory, len, assembled, instructions, pc.
     342  let jexp := jump_expansion ppc program in
     343  let exp :=
     344    expand_pseudo_instruction lookup_labels lookup_datalabels pc jexp pi
     345  let ass :=
     346    assembly_1_pseudoinstruction program ppc pc lk_labels lk_dlabels pi in
     347  Some ? instructions = exp $\rightarrow$
     348    Some $\ldots$ $\langle$len, assembled$\rangle$ = ass $\rightarrow$
     349      encoding_check code_memory pc (pc + len) assembled $\rightarrow$
     350        fetch_many code_memory (pc + len) pc instructions.
     351\end{lstlisting}
     352
     353\begin{lstlisting}
     354theorem fetch_assembly: $\forall$pc, i, cmem, assembled.
     355  assembled = assembly1 i $\rightarrow$
     356  let len := length ... assembled in
     357    encoding_check cmem pc (pc + len) assembled $\rightarrow$
     358    let fetched := fetch code_memory (bitvector_of_nat $\ldots$ pc) in
     359    let $\langle$instr_pc, ticks$\rangle$ := fetched in
     360    let $\langle$instr,pc'$\rangle$ := instr_pc in
     361      (eq_instruction instr i $\wedge$
     362       eqb ticks (ticks_of_instruction instr) $\wedge$
     363       eq_bv $\ldots$ pc' (pc + len)) = true.
     364\end{lstlisting}
     365
    275366An \texttt{internal\_pseudo\_address\_map} positions in the memory of a \texttt{PseudoStatus} with a physical memory address.
    276367\begin{lstlisting}
     
    298389This is done with the following function:
    299390\begin{lstlisting}
    300 definition next_internal_pseudo_address_map:
    301  internal_pseudo_address_map $\rightarrow$ PseudoStatus $\rightarrow$ option internal_pseudo_address_map
    302 \end{lstlisting}
    303 Finally, we are able to state and prove our main theorem relating the execution of a single assembly instruction and the execution of (possibly) many machine code instructions:
    304 \begin{lstlisting}
    305 lemma main_thm:
     391definition next_internal_pseudo_address_map: internal_pseudo_address_map
     392  $\rightarrow$ PseudoStatus $\rightarrow$ option internal_pseudo_address_map
     393\end{lstlisting}
     394Finally, we are able to state and prove our main theorem.
     395This relates the execution of a single assembly instruction and the execution of (possibly) many machine code instructions.
     396That is, the assembly process preserves the semantics of an assembly program, as it is translated into machine code:
     397\begin{lstlisting}
     398theorem main_thm:
    306399  ∀M,M',ps,s,s''.
    307400    next_internal_pseudo_address_map M ps = Some ... M' $\rightarrow$
     
    316409Suppose further that, after executing a single assembly instruction and converting the resulting \texttt{PseudoStatus} into a \texttt{Status}, we obtain $s''$, being careful to track the number of ticks executed.
    317410Then, there exists some number $n$, so that executing $n$ machine code instructions in \texttt{Status} $s$ gives us \texttt{Status} $s''$.
    318 
    319 % ---------------------------------------------------------------------------- %
    320 % SECTION                                                                      %
    321 % ---------------------------------------------------------------------------- %
    322 \subsection{Proof of correctness}
    323 \label{subsect.proof.of.correctness}
    324 
    325 CSC: no options using policy
    326 \begin{lstlisting}
    327 lemma fetch_assembly_pseudo2:
    328  ∀program,assembled,costs,labels.
    329   Some ... LANGLElabels,costsRANGLE = build_maps program →
    330   Some ... LANGLEassembled,costsRANGLE = assembly program →
    331    ∀ppc.
    332     let code_memory ≝ load_code_memory assembled in
    333     let preamble ≝ \fst program in
    334     let data_labels ≝ construct_datalabels preamble in
    335     let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in
    336     let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
    337     let expansion ≝ jump_expansion ppc program in
    338     let LANGLEpi,newppcRANGLE ≝ fetch_pseudo_instruction (\snd program) ppc in
    339      ∃instructions.
    340       Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi ∧
    341        fetch_many code_memory (sigma program newppc) (sigma program ppc) instructions.
    342 \end{lstlisting}
    343 
    344 \begin{lstlisting}
    345  definition expand_pseudo_instruction:
    346   ∀lookup_labels.∀lookup_datalabels.∀pc.∀policy_decision. (sigma program ppc) expansion. pseudo_instruciton -> list instruction.
    347 \end{lstlisting}
    348 
    349 \begin{lstlisting}
    350 axiom assembly_ok:
    351  ∀program,assembled,costs,labels.
    352   Some ... LANGLElabels,costsRANGLE = build_maps program →
    353   Some ... LANGLEassembled,costsRANGLE = assembly program →
    354   let code_memory ≝ load_code_memory assembled in
    355   let preamble ≝ \fst program in
    356   let datalabels ≝ construct_datalabels preamble in
    357   let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in
    358   let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in
    359    ∀ppc,len,assembledi.
    360     let LANGLEpi,newppcRANGLE ≝ fetch_pseudo_instruction (\snd program) ppc in
    361      Some ... LANGLElen,assemblediRANGLE = assembly_1_pseudoinstruction program ppc (sigma program ppc) lookup_labels lookup_datalabels pi →
    362       encoding_check code_memory (sigma program ppc) (bitvector_of_nat ... (nat_of_bitvector ... (sigma program ppc) + len)) assembledi ∧
    363        sigma program newppc = bitvector_of_nat ... (nat_of_bitvector ... (sigma program ppc) + len).
    364 \end{lstlisting}
    365 
    366 \begin{lstlisting}
    367 lemma fetch_assembly_pseudo:
    368  ∀program,ppc,lookup_labels,lookup_datalabels.
    369   ∀pi,code_memory,len,assembled,instructions,pc.
    370    let expansion ≝ jump_expansion ppc program in
    371    Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (bitvector_of_nat ? pc) expansion pi →
    372     Some ... LANGLElen,assembledRANGLE = assembly_1_pseudoinstruction program ppc (bitvector_of_nat ? pc) lookup_labels lookup_datalabels pi →
    373      encoding_check code_memory (bitvector_of_nat ... pc) (bitvector_of_nat ... (pc + len)) assembled →
    374       fetch_many code_memory (bitvector_of_nat ... (pc + len)) (bitvector_of_nat ... pc) instructions.
    375 \end{lstlisting}
    376 
    377 \begin{lstlisting}
    378 theorem fetch_assembly:
    379   ∀pc,i,code_memory,assembled.
    380     assembled = assembly1 i →
    381       let len ≝ length ... assembled in
    382       encoding_check code_memory (bitvector_of_nat ... pc) (bitvector_of_nat ... (pc + len)) assembled →
    383       let fetched ≝ fetch code_memory (bitvector_of_nat ... pc) in
    384       let LANGLEinstr_pc, ticksRANGLE ≝ fetched in
    385       let LANGLEinstr,pc'RANGLE ≝ instr_pc in
    386        (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv ... pc' (bitvector_of_nat ... (pc + len))) = true.
    387 \end{lstlisting}
     411Theorem \texttt{main\_thm} establishes the correctness of the assembly process.
    388412
    389413% ---------------------------------------------------------------------------- %
  • src/ASM/CPP2011/lst-grafite.tex

    r960 r974  
    22mathescape=true,
    33texcl=false,
    4 keywords={include},
    5 morekeywords={record, with, match, let, rec, corec, inductive, definition, axiom,
     4keywords={record, with, match, let, rec, corec, inductive, definition, axiom,
    65        qed, intro, intros, symmetry, simplify, rewrite, apply, elim, assumption,
    76        left, cut, cases, auto, right, coercion, split, lemma, theorem, skip, constructor, copy, from, letin,
    87        by, done, we, conclude, assume, need, to, prove, unfold, return, and, check,
    98        notation, interpretation, lapply, repeat, try, as, clear, in, change, whd, exists},
     9morekeywords={[2]include},
    1010%emph={[1]Type, Prop, nat, real}, emphstyle={[1]\textit},
    1111literate=       
     
    142142        {...}{{$\ldots$}}1
    143143        ,
     144tabsize=1,
    144145comment=[s]{(*}{*)},
    145146showstringspaces=true,
     
    149150captionpos=b,
    150151mathescape=true,
     152keywordstyle=\bfseries,
     153keywordstyle=[2]\bfseries,
     154keywordstyle=[3]\bfseries,
    151155%backgroundcolor=\color{gray},
    152156frame=tblr,
Note: See TracChangeset for help on using the changeset viewer.