Changeset 3364


Ignore:
Timestamp:
Jun 17, 2013, 3:16:25 PM (4 years ago)
Author:
boender
Message:
  • added bit to the introduction about contribution
Location:
src/ASM/CPP2013-policy
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2013-policy/conclusion.tex

    r3363 r3364  
    2424from instruction labels to addresses in the assembly code. In the
    2525second pass it iterates over the code, translating every pseudo jump
    26 at address src to a label l associated to the assembly instruction at
    27 address dst to a jump of the size dictated by $(\sigma\ src)$ to
     26at address $src$ to a label l associated to the assembly instruction at
     27address $dst$ to a jump of the size dictated by $(\sigma\ src)$ to
    2828$(\sigma\ dst)$. In case of conditional jumps, the translated jump may be
    2929implemented with a series of instructions.
     
    3131The proof of correctness abstracts over the algorithm used and only relies on
    3232{\tt sigma\_policy\_specification} (page~\ref{sigmapolspec}). It is a variation
    33 of a standard 1-to-many forward simulation proof~\cite{compcert:2011}. The
    34 relation R between states just maps every code address ppc stored in
     33of a standard 1-to-many forward simulation proof~\cite{Leroy2009}. The
     34relation R between states just maps every code address $ppc$ stored in
    3535registers or memory to $(\sigma\ ppc)$. To identify the code addresses,
    3636an additional data structure is always kept together with the source
    3737state and is updated by the semantics. The semantics is preserved
    3838only for those programs whose source code operations
    39 $(f\ ppc1\ \ldots\ ppcn)$ applied to code addresses $ppc1 \ldots ppcn$ are such
    40 that $(f\ (\sigma\ ppc1)\ ...\ (\sigma\ ppc) = f\ ppc\ ppcn))$. For example,
    41 an injective $\sigma$ preserves a binary equality test f for code addresses,
    42 but not pointer subtraction.
     39$(f\ ppc_1\ \ldots\ ppc_n)$ applied to code addresses $ppc_1 \ldots ppc_n$ are
     40such that $(f\ (\sigma\ ppc_1)\ ...\ (\sigma\ ppc) = f\ ppc\ ppc_n))$. For
     41example, an injective $\sigma$ preserves a binary equality test f for code
     42addresses, but not pointer subtraction.
    4343
    4444The main lemma (fetching simulation), which relies on\\
     
    5555see~\cite{lastyear}.
    5656
     57Instead of verifying the algorithm directly, another solution to the problem
     58would be to run an optimisation algorithm, and then verify the safety of the
     59result using a verified validator. Such a validator would be easier to verify
     60than the algorithm itself, but it would still leave the question of
     61termination open. In the case of a least fixed point algorithm, at least, the
     62solution is not necessarily safe until the algorithm terminates, so this
     63effort would still have to be expended.
     64
     65
    5766\subsection{Related work}
    5867
     
    6675displacement optimisation algorithm is not needed.
    6776
    68 An offshoot of the CompCert project is the CompCertTSO project, who add thread
    69 concurrency and synchronisation to the CompCert compiler~\cite{TSO2011}. This
    70 compiler also generates assembly code and therefore does not include a branch
    71 displacement algorithm.
     77An offshoot of the CompCert project is the CompCertTSO project, which adds
     78thread concurrency and synchronisation to the CompCert compiler~\cite{TSO2011}.
     79This compiler also generates assembly code and therefore does not include a
     80branch displacement algorithm.
    7281 
    7382Finally, there is also the Piton stack~\cite{Moore1996}, which not only includes the
    7483formal verification of a compiler, but also of the machine architecture
    75 targeted by that compiler, a bespoke microprocessor called the FM9001.
     84targeted by that compiler, a microprocessor called the FM9001.
    7685However, this architecture does not have different
    7786jump sizes (branching is simulated by assigning values to the program counter),
  • src/ASM/CPP2013-policy/problem.tex

    r3363 r3364  
    1414that is the proofs of termination and correctness using the Matita proof
    1515assistant~\cite{Asperti2007}.
    16  
     16
     17Formulating the final statement of correctness and finding the loop invariants
     18have been non-trivial tasks and are, indeed, the main contribution of this
     19paper. It has required considerable care and fine-tuning to formulate not
     20only the minimal statement required for the ulterior proof of correctness of
     21the assembler, but also the minimal set of invariants needed for the proof
     22of correctness of the algorithm.
     23
    1724The research presented in this paper has been executed within the CerCo project
    1825which aims at formally verifying a C compiler with cost annotations. The
  • src/ASM/CPP2013-policy/proof.tex

    r3363 r3364  
    22
    33In this section, we present the correctness proof for the algorithm in more
    4 detail.  The main correctness statement is shown, slightly simplified, in~Figure~\ref{statement}.
     4detail. The main correctness statement is shown, slightly simplified, in~Figure~\ref{statement}.
    55
    66\label{sigmapolspec}
     
    5151the program. This worst case is reached if at every iteration, we change the
    5252encoding of exactly one branch instruction; since the encoding of any branch
    53 instructions can change first from short to absolute and then from absolute to
    54 long, there can be at most $2n$ changes.
     53instructions can change first from short to absolute and then to long, there
     54can be at most $2n$ changes.
    5555
    5656The proof has been carried out using the ``Russell'' style from~\cite{Sozeau2006}.
     
    123123\end{figure}
    124124
    125 We can now proceed with the lemmas that are needed for algorithm safety.
    126 The lemma in Figure~\ref{sigmacompactunsafe} is a temporary formulation of
    127 the main property\\ ({\tt sigma\_policy\_specification}). Its main difference
    128 from the final version is that it uses {\tt instruction\_size\_jmplen} to
    129 compute the instruction size. This function uses $j$ to compute the span
    130 of branch instructions  (i.e. it uses the $\sigma$ function under construction),
    131 instead of looking at the distance between source and destination. This is
    132 because $\sigma$ is still under construction; later on we will prove that after
    133 the final iteration, {\tt sigma\_compact\_unsafe} is equivalent to the main
     125We now proceed with the safety lemmas. The lemma in
     126Figure~\ref{sigmacompactunsafe} is a temporary formulation of the main
     127property {\tt sigma\_policy\_specification}. Its main difference from the
     128final version is that it uses {\tt instruction\_size\_jmplen} to compute the
     129instruction size. This function uses $j$ to compute the span of branch
     130instructions  (i.e. it uses the $\sigma$ under construction), instead
     131of looking at the distance between source and destination. This is because
     132$\sigma$ is still under construction; we will prove below that after the
     133final iteration, {\tt sigma\_compact\_unsafe} is equivalent to the main
    134134property.
    135135
     
    161161\end{figure}
    162162
    163 The lemma in figure~\ref{sigmasafe} is a more direct safety property. It states
     163The lemma in figure~\ref{sigmasafe} is a safety property. It states
    164164that branch instructions are encoded properly, and that no wrong branch
    165165instructions are chosen.
     
    266266We need this invariant to make sure that addresses do not overflow.
    267267
    268 The invariants that are taken directly from the fold invariants are trivial to
    269 prove.
     268The invariants taken directly from the fold invariants are trivial to prove.
    270269
    271270The proof of {\tt nec\_plus\_ultra} goes as follows: if we return {\tt None},
Note: See TracChangeset for help on using the changeset viewer.