Changeset 3370 for src/ASM/CPP2013-policy

Timestamp:

Jun 18, 2013, 2:36:31 AM (8 years ago)

Author:

sacerdot

Message:

Submitted.

Location:

src/ASM/CPP2013-policy

Files:

• algorithm.tex (modified) (1 diff)
• biblio.bib (modified) (1 diff)
• conclusion.tex (modified) (2 diffs)
• proof.tex (modified) (1 diff)

src/ASM/CPP2013-policy/algorithm.tex

@@ -180 +180 @@
 $\sigma: \mathbb{N} \rightarrow \mathbb{N} \times \{\mathtt{short\_jump},
 \mathtt{absolute\_jump},\mathtt{long\_jump}\}$; a function that associates a
-pseudo-address with a memory address and a jump length. We do this to be able
-to ease the comparison of jump lengths between iterations. In the algorithm,
+pseudo-address with a memory address and a jump length. We do this to
+ease the comparison of jump lengths between iterations. In the algorithm,
 we use the notation $sigma_1(x)$ to denote the memory address corresponding to
-$x$, and $sigma_2(x)$ to denote the jump length corresponding to $x$.
+$x$, and $sigma_2(x)$ for the jump length corresponding to $x$.
 
 Note that the $\sigma$ function used for label lookup varies depending on

src/ASM/CPP2013-policy/biblio.bib

@@ -174 +174 @@
 series={Lecture Notes in Computer Science},
 editor={Hawblitzel, Chris and Miller, Dale},
-doi={10.1007/978-3-642-35308-6_8},
-title={An Executable Semantics for CompCert C},
-url={http://dx.doi.org/10.1007/978-3-642-35308-6_8},
+doi={10.1007/978-3-642-35308-6_7},
+title={On the Correctness of an Optimising Assembler for the Intel MCS-51 Microprocessor},
+url={http://dx.doi.org/10.1007/978-3-642-35308-6_7},
 publisher={Springer Berlin Heidelberg},
-author={Campbell, Brian},
-pages={60-75}
+keywords={Verified software; CerCo (Certified Complexity); MCS-51 microcontroller; Matita proof assistant},
+author={Mulligan, Dominic P. and Sacerdoti Coen, Claudio},
+pages={43-59}
 }
 

src/ASM/CPP2013-policy/conclusion.tex

@@ -38 +38 @@
 only for those programs whose source code operations
 $(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
+such that $(f\ (\sigma\ ppc_1)\ ...\ (\sigma\ ppc_n) = f\ ppc_1\ ppc_n))$. For
 example, an injective $\sigma$ preserves a binary equality test f for code
 addresses, but not pointer subtraction.
@@ -58 +58 @@
 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.
-
+than the algorithm itself and it would also be efficient, requiring only a
+linear pass over the source code to test the specification. However, it is
+surely also interesting to formally prove that the assembler never rejects
+programs that should be accepted, i.e. that the algorithm itself is correct.
+This was the topic of the current paper.
 
 \subsection{Related work}

src/ASM/CPP2013-policy/proof.tex

@@ -20 +20 @@
         &&&&& \mathbf{let}\ instruction' \equiv \mathtt{fetch\_pseudo\_instruction}\ instr\_list\ ppc'\ ppc\_ok'\ \mathbf{in} \notag\\
         &&&&&\ \mathtt{instruction\_size}\ sigma\ policy\ ppc'\ instruction' = 0)\ \wedge \notag\\
-        &&&&& pc + (\mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction = 2^{16}))
+        &&&&& pc + \mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction = 2^{16})
 \end{alignat*}
 \caption{Main correctness statement\label{statement}}