Changeset 3370 for src


Ignore:
Timestamp:
Jun 18, 2013, 2:36:31 AM (6 years ago)
Author:
sacerdot
Message:

Submitted.

Location:
src/ASM/CPP2013-policy
Files:
4 edited

Legend:

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

    r3363 r3370  
    180180$\sigma: \mathbb{N} \rightarrow \mathbb{N} \times \{\mathtt{short\_jump},
    181181\mathtt{absolute\_jump},\mathtt{long\_jump}\}$; a function that associates a
    182 pseudo-address with a memory address and a jump length. We do this to be able
    183 to ease the comparison of jump lengths between iterations. In the algorithm,
     182pseudo-address with a memory address and a jump length. We do this to
     183ease the comparison of jump lengths between iterations. In the algorithm,
    184184we use the notation $sigma_1(x)$ to denote the memory address corresponding to
    185 $x$, and $sigma_2(x)$ to denote the jump length corresponding to $x$.
     185$x$, and $sigma_2(x)$ for the jump length corresponding to $x$.
    186186
    187187Note that the $\sigma$ function used for label lookup varies depending on
  • src/ASM/CPP2013-policy/biblio.bib

    r3363 r3370  
    174174series={Lecture Notes in Computer Science},
    175175editor={Hawblitzel, Chris and Miller, Dale},
    176 doi={10.1007/978-3-642-35308-6_8},
    177 title={An Executable Semantics for CompCert C},
    178 url={http://dx.doi.org/10.1007/978-3-642-35308-6_8},
     176doi={10.1007/978-3-642-35308-6_7},
     177title={On the Correctness of an Optimising Assembler for the Intel MCS-51 Microprocessor},
     178url={http://dx.doi.org/10.1007/978-3-642-35308-6_7},
    179179publisher={Springer Berlin Heidelberg},
    180 author={Campbell, Brian},
    181 pages={60-75}
     180keywords={Verified software; CerCo (Certified Complexity); MCS-51 microcontroller; Matita proof assistant},
     181author={Mulligan, Dominic P. and Sacerdoti Coen, Claudio},
     182pages={43-59}
    182183}
    183184
  • src/ASM/CPP2013-policy/conclusion.tex

    r3364 r3370  
    3838only for those programs whose source code operations
    3939$(f\ ppc_1\ \ldots\ ppc_n)$ applied to code addresses $ppc_1 \ldots ppc_n$ are
    40 such that $(f\ (\sigma\ ppc_1)\ ...\ (\sigma\ ppc) = f\ ppc\ ppc_n))$. For
     40such that $(f\ (\sigma\ ppc_1)\ ...\ (\sigma\ ppc_n) = f\ ppc_1\ ppc_n))$. For
    4141example, an injective $\sigma$ preserves a binary equality test f for code
    4242addresses, but not pointer subtraction.
     
    5858would be to run an optimisation algorithm, and then verify the safety of the
    5959result using a verified validator. Such a validator would be easier to verify
    60 than the algorithm itself, but it would still leave the question of
    61 termination open. In the case of a least fixed point algorithm, at least, the
    62 solution is not necessarily safe until the algorithm terminates, so this
    63 effort would still have to be expended.
    64 
     60than the algorithm itself and it would also be efficient, requiring only a
     61linear pass over the source code to test the specification. However, it is
     62surely also interesting to formally prove that the assembler never rejects
     63programs that should be accepted, i.e. that the algorithm itself is correct.
     64This was the topic of the current paper.
    6565
    6666\subsection{Related work}
  • src/ASM/CPP2013-policy/proof.tex

    r3365 r3370  
    2020        &&&&& \mathbf{let}\ instruction' \equiv \mathtt{fetch\_pseudo\_instruction}\ instr\_list\ ppc'\ ppc\_ok'\ \mathbf{in} \notag\\
    2121        &&&&&\ \mathtt{instruction\_size}\ sigma\ policy\ ppc'\ instruction' = 0)\ \wedge \notag\\
    22         &&&&& pc + (\mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction = 2^{16}))
     22        &&&&& pc + \mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction = 2^{16})
    2323\end{alignat*}
    2424\caption{Main correctness statement\label{statement}}
Note: See TracChangeset for help on using the changeset viewer.