Changeset 3364 for src

Timestamp:

Jun 17, 2013, 3:16:25 PM (7 years ago)

Author:

boender

Message:

• added bit to the introduction about contribution

Location:

src/ASM/CPP2013-policy

Files:

• conclusion.tex (modified) (4 diffs)
• problem.tex (modified) (1 diff)
• proof.tex (modified) (5 diffs)

src/ASM/CPP2013-policy/conclusion.tex

@@ -24 +24 @@
 from instruction labels to addresses in the assembly code. In the 
 second pass it iterates over the code, translating every pseudo jump
-at address src to a label l associated to the assembly instruction at
-address dst to a jump of the size dictated by $(\sigma\ src)$ to
+at address $src$ to a label l associated to the assembly instruction at
+address $dst$ to a jump of the size dictated by $(\sigma\ src)$ to
 $(\sigma\ dst)$. In case of conditional jumps, the translated jump may be 
 implemented with a series of instructions.
@@ -31 +31 @@
 The proof of correctness abstracts over the algorithm used and only relies on
 {\tt sigma\_policy\_specification} (page~\ref{sigmapolspec}). It is a variation
-of a standard 1-to-many forward simulation proof~\cite{compcert:2011}. The
-relation R between states just maps every code address ppc stored in 
+of a standard 1-to-many forward simulation proof~\cite{Leroy2009}. The
+relation R between states just maps every code address $ppc$ stored in 
 registers or memory to $(\sigma\ ppc)$. To identify the code addresses,
 an additional data structure is always kept together with the source
 state and is updated by the semantics. The semantics is preserved
 only for those programs whose source code operations
-$(f\ ppc1\ \ldots\ ppcn)$ applied to code addresses $ppc1 \ldots ppcn$ are such
-that $(f\ (\sigma\ ppc1)\ ...\ (\sigma\ ppc) = f\ ppc\ ppcn))$. For example,
-an injective $\sigma$ preserves a binary equality test f for code addresses,
-but not pointer subtraction.
+$(f\ ppc_1\ \ldots\ ppc_n)$ applied to code addresses $ppc_1 \ldots ppc_n$ are
+such that $(f\ (\sigma\ ppc_1)\ ...\ (\sigma\ ppc) = f\ ppc\ ppc_n))$. For
+example, an injective $\sigma$ preserves a binary equality test f for code
+addresses, but not pointer subtraction.
 
 The main lemma (fetching simulation), which relies on\\
@@ -55 +55 @@
 see~\cite{lastyear}.
 
+Instead of verifying the algorithm directly, another solution to the problem
+would be to run an optimisation algorithm, and then verify the safety of the
+result using a verified validator. Such a validator would be easier to verify
+than the algorithm itself, but it would still leave the question of
+termination open. In the case of a least fixed point algorithm, at least, the
+solution is not necessarily safe until the algorithm terminates, so this
+effort would still have to be expended.
+
+
 \subsection{Related work}
 
@@ -66 +75 @@
 displacement optimisation algorithm is not needed.
 
-An offshoot of the CompCert project is the CompCertTSO project, who add thread
-concurrency and synchronisation to the CompCert compiler~\cite{TSO2011}. This
-compiler also generates assembly code and therefore does not include a branch
-displacement algorithm.
+An offshoot of the CompCert project is the CompCertTSO project, which adds
+thread concurrency and synchronisation to the CompCert compiler~\cite{TSO2011}.
+This compiler also generates assembly code and therefore does not include a
+branch displacement algorithm.
  
 Finally, there is also the Piton stack~\cite{Moore1996}, which not only includes the
 formal verification of a compiler, but also of the machine architecture
-targeted by that compiler, a bespoke microprocessor called the FM9001.
+targeted by that compiler, a microprocessor called the FM9001.
 However, this architecture does not have different
 jump sizes (branching is simulated by assigning values to the program counter),

src/ASM/CPP2013-policy/problem.tex

@@ -14 +14 @@
 that is the proofs of termination and correctness using the Matita proof
 assistant~\cite{Asperti2007}.
- 
+
+Formulating the final statement of correctness and finding the loop invariants
+have been non-trivial tasks and are, indeed, the main contribution of this
+paper. It has required considerable care and fine-tuning to formulate not
+only the minimal statement required for the ulterior proof of correctness of
+the assembler, but also the minimal set of invariants needed for the proof
+of correctness of the algorithm.
+
 The research presented in this paper has been executed within the CerCo project
 which aims at formally verifying a C compiler with cost annotations. The

src/ASM/CPP2013-policy/proof.tex

@@ -2 +2 @@
 
 In this section, we present the correctness proof for the algorithm in more
-detail.  The main correctness statement is shown, slightly simplified, in~Figure~\ref{statement}.
+detail. The main correctness statement is shown, slightly simplified, in~Figure~\ref{statement}.
 
 \label{sigmapolspec}
@@ -51 +51 @@
 the program. This worst case is reached if at every iteration, we change the
 encoding of exactly one branch instruction; since the encoding of any branch
-instructions can change first from short to absolute and then from absolute to
-long, there can be at most $2n$ changes.
+instructions can change first from short to absolute and then to long, there
+can be at most $2n$ changes.
 
 The proof has been carried out using the ``Russell'' style from~\cite{Sozeau2006}.
@@ -123 +123 @@
 \end{figure}
 
-We can now proceed with the lemmas that are needed for algorithm safety.
-The lemma in Figure~\ref{sigmacompactunsafe} is a temporary formulation of
-the main property\\ ({\tt sigma\_policy\_specification}). Its main difference
-from the final version is that it uses {\tt instruction\_size\_jmplen} to
-compute the instruction size. This function uses $j$ to compute the span
-of branch instructions  (i.e. it uses the $\sigma$ function under construction),
-instead of looking at the distance between source and destination. This is
-because $\sigma$ is still under construction; later on we will prove that after
-the final iteration, {\tt sigma\_compact\_unsafe} is equivalent to the main
+We now proceed with the safety lemmas. The lemma in
+Figure~\ref{sigmacompactunsafe} is a temporary formulation of the main
+property {\tt sigma\_policy\_specification}. Its main difference from the
+final version is that it uses {\tt instruction\_size\_jmplen} to compute the
+instruction size. This function uses $j$ to compute the span of branch
+instructions  (i.e. it uses the $\sigma$ under construction), instead
+of looking at the distance between source and destination. This is because
+$\sigma$ is still under construction; we will prove below that after the
+final iteration, {\tt sigma\_compact\_unsafe} is equivalent to the main
 property.
 
@@ -161 +161 @@
 \end{figure}
 
-The lemma in figure~\ref{sigmasafe} is a more direct safety property. It states
+The lemma in figure~\ref{sigmasafe} is a safety property. It states
 that branch instructions are encoded properly, and that no wrong branch
 instructions are chosen.
@@ -266 +266 @@
 We need this invariant to make sure that addresses do not overflow.
 
-The invariants that are taken directly from the fold invariants are trivial to
-prove.
+The invariants taken directly from the fold invariants are trivial to prove.
 
 The proof of {\tt nec\_plus\_ultra} goes as follows: if we return {\tt None},