Changeset 2068


Ignore:
Timestamp:
Jun 13, 2012, 7:54:36 PM (5 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2012-asm/cpp-2012-asm.tex

    r2067 r2068  
    360360\label{subsect.total.correctness.of.the.assembler}
    361361
    362 Throughout the proof of correctness for assembly we assume that policies are bifurcated into two functions: \texttt{sigma} mapping \texttt{Word} to \texttt{Word} and \texttt{policy} mapping \texttt{Word} to \texttt{bool}.
    363 For our purposes, \texttt{sigma} is most interesting, as it maps pseudo program counters to program counters; \texttt{policy} is merely a technical device used in jump expansion.
    364 
    365362Using our policies, we now work toward proving the total correctness of the assembler.
    366 By `total correctness', we mean that the assembly process never fails when provided with a good policy and that the process does not change the semantics of a certain class of well behaved assembly programs.
    367 By `good policy' we mean
    368 We assume the correctness of the policies given to us using a function, \texttt{sigma\_policy\_specification} that we take in input, when needed.
    369 
    370 We expand pseudoinstructions using the function \texttt{expand\_pseudo\_instruction}.
    371 This takes an assembly program (consisting of a list of pseudoinstructions), a policy for the program, a map detailing the physical addresses of data labels from the pseudo program's preamble, and the pseudoinstruction to be expanded.
    372 It returns a list of instructions, corresponding to the expanded pseudoinstruction referenced by the pointer.
    373 Execution proceeds by case analysis on the pseudoinstruction given as input.
    374 The policy, \texttt{sigma}, is used to decide how to expand \texttt{Call}s, \texttt{Jmp}s and conditional jumps.
    375 \begin{lstlisting}
    376 definition expand_pseudo_instruction:
    377  $\forall$lookup_labels: Identifier $\rightarrow$ Word.
    378  $\forall$sigma: Word $\rightarrow$ Word.
    379  $\forall$policy: Word $\rightarrow$ bool.
    380   Word $\rightarrow$ (Identifier $\rightarrow$ Word) $\rightarrow$
    381    pseudo_instruction $\rightarrow$ list instruction := ...
    382 \end{lstlisting}
     363By `total correctness', we mean that the assembly process never fails when provided with a correct policy and that the process does not change the semantics of a certain class of well behaved assembly programs.
    383364
    384365We can express the following lemma, expressing the correctness of the assembly function (slightly simplified):
Note: See TracChangeset for help on using the changeset viewer.