# Changeset 3370

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

Submitted.

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

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

 r3363 $\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

 r3363 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

 r3364 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. 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

 r3365 &&&&& \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}}
Note: See TracChangeset for help on using the changeset viewer.