Changeset 3362 for src/ASM/CPP2012-policy/proof.tex

Ignore:
Timestamp:
Jun 17, 2013, 1:08:27 PM (6 years ago)
Message:
• added some bits as per Claudio's mail
• rewrote some small things
• general reread, spell check, grammar check
• 16 pages again now
File:
1 edited

Legend:

Unmodified
 r3361 In this section, we present the correctness proof for the algorithm in more detail.  The main correctness statement is shown, slightly simplified, in~Figure~\cite{statement}. detail.  The main correctness statement is shown, slightly simplified, in~Figure~\ref{statement}. \label{sigmapolspec} \begin{figure}[t] \begin{alignat*}{6} \subsection{Fold invariants} These are the invariants that hold during the fold of {\sc f} over the program, and that will later on be used to prove the properties of the iteration. In this section, we present the invariants that hold during the fold of {\sc f} over the program. These will be used later on to prove the properties of the iteration. Note that during the fixed point computation, the $\sigma$ function is implemented as a trie for ease of access; computing $\sigma(x)$ is achieved by looking up the value of $x$ in the trie. Actually, during the fold, the value we pass along is a pair $\mathbb{N} \times \mathtt{ppc\_pc\_map}$. The first component is the number of bytes added to the program so far with respect to implemented as a trie for ease of access; computing $\sigma(x)$ is achieved by looking up the value of $x$ in the trie. Actually, during the fold, the value we pass along is a pair $\mathbb{N} \times \mathtt{ppc\_pc\_map}$. The first component is the number of bytes added to the program so far with respect to the previous iteration, and the second component, {\tt ppc\_pc\_map}, is the acual $\sigma$ trie. actual $\sigma$ trie. \begin{alignat*}{2} \end{alignat*} This invariant states that any pseudo-address not yet examined is not The first invariant states that any pseudo-address not yet examined is not present in the lookup trie. increase. It is needed for proving termination. \begin{figure}[ht] \begin{alignat*}{6} \mathtt{sigma} & \omit\rlap{$\mathtt{\_compact\_unsafe} \equiv \lambda prefix.\lambda sigma.$}\notag\\ &&&&& \ \ \mathtt{instruction\_size\_jmplen}\ j\ (\mathtt{nth}\ n\ prefix) \end{alignat*} This is a temporary formulation of the main property\\ ({\tt sigma\_policy\_specification}); its main difference \caption{Temporary safety property} \label{sigmacompactunsafe} \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 property. \begin{figure}[ht] \begin{alignat*}{6} \mathtt{sigma} & \omit\rlap{$\mathtt{\_safe} \equiv \lambda prefix.\lambda labels.\lambda old\_sigma.\lambda sigma$}\notag\\ &&&&&\mathrm{long\_jump} \Rightarrow \mathrm{True} \end{alignat*} This is a more direct safety property: it states that branch instructions are encoded properly, and that no wrong branch instructions are chosen. \caption{Safety property} \label{sigmasafe} \end{figure} The lemma in figure~\ref{sigmasafe} is a more direct safety property. It states that branch instructions are encoded properly, and that no wrong branch instructions are chosen. Note that we compute the distance using the memory address of the instruction plus its size: this follows the behaviour of the MCS-51 microprocessor, which plus its size. This follows the behaviour of the MCS-51 microprocessor, which increases the program counter directly after fetching, and only then executes the branch instruction (by changing the program counter again). We now encode some final, simple, properties to make sure that our policy remains consistent, and to keep track of whether the fixed point has been reached. \begin{align*} The type of an iteration therefore becomes an option type: {\tt None} in case the program becomes larger than 64 Kb, or $\mathtt{Some}\ \sigma$ otherwise. We also no longer use a natural number to pass along the number of bytes added to the program size, but a boolean that indicates whether we have changed something during the iteration or not. otherwise. We also no longer pass along the number of bytes added to the program size, but a boolean that indicates whether we have changed something during the iteration or not. If an iteration returns {\tt None}, we have the following invariant: is only correct when we have reached the fixed point. There is another, trivial, invariant if the iteration returns $\mathtt{Some}\ \sigma$: $\mathtt{fst}\ sigma = 2^{16}$. There is another, trivial, invariant in case the iteration returns $\mathtt{Some}\ \sigma$: it must hold that $\mathtt{fst}\ sigma < 2^{16}$. 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 proof of {\tt nec\_plus\_ultra} works as follows: if we return {\tt None}, The proof of {\tt nec\_plus\_ultra} goes as follows: if we return {\tt None}, then the program size must be greater than 64 Kb. However, since the previous iteration did not return {\tt None} (because otherwise we would longer jumps, in iteration $2n$ every branch instruction must be encoded as a long jump. In this case, iteration $2n$ is equal to iteration $2n+1$ and the fixpoint is reached. fixed point is reached.