Changeset 3362 for src/ASM/CPP2012policy/proof.tex
 Timestamp:
 Jun 17, 2013, 1:08:27 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CPP2012policy/proof.tex
r3361 r3362 2 2 3 3 In this section, we present the correctness proof for the algorithm in more 4 detail. The main correctness statement is shown, slightly simplified, in~Figure~\cite{statement}. 5 4 detail. The main correctness statement is shown, slightly simplified, in~Figure~\ref{statement}. 5 6 \label{sigmapolspec} 6 7 \begin{figure}[t] 7 8 \begin{alignat*}{6} … … 61 62 \subsection{Fold invariants} 62 63 63 These are the invariants that hold during the fold of {\sc f} over the program, 64 and that will later on be used to prove the properties of the iteration. 64 In this section, we present the invariants that hold during the fold of {\sc f} 65 over the program. These will be used later on to prove the properties of the 66 iteration. 65 67 66 68 Note that during the fixed point computation, the $\sigma$ function is 67 implemented as a trie for ease of access; computing $\sigma(x)$ is achieved by looking68 up the value of $x$ in the trie. Actually, during the fold, the value we69 pass along is a pair $\mathbb{N} \times \mathtt{ppc\_pc\_map}$. The first component70 is the number of bytes added to the program so far with respect to69 implemented as a trie for ease of access; computing $\sigma(x)$ is achieved by 70 looking up the value of $x$ in the trie. Actually, during the fold, the value 71 we pass along is a pair $\mathbb{N} \times \mathtt{ppc\_pc\_map}$. The first 72 component is the number of bytes added to the program so far with respect to 71 73 the previous iteration, and the second component, {\tt ppc\_pc\_map}, is the 72 ac ual $\sigma$ trie.74 actual $\sigma$ trie. 73 75 74 76 \begin{alignat*}{2} … … 78 80 \end{alignat*} 79 81 80 Th isinvariant states that any pseudoaddress not yet examined is not82 The first invariant states that any pseudoaddress not yet examined is not 81 83 present in the lookup trie. 82 84 … … 104 106 increase. It is needed for proving termination. 105 107 108 \begin{figure}[ht] 106 109 \begin{alignat*}{6} 107 110 \mathtt{sigma} & \omit\rlap{$\mathtt{\_compact\_unsafe} \equiv \lambda prefix.\lambda sigma.$}\notag\\ … … 116 119 &&&&& \ \ \mathtt{instruction\_size\_jmplen}\ j\ (\mathtt{nth}\ n\ prefix) 117 120 \end{alignat*} 118 119 This is a temporary formulation of the main property\\ 120 ({\tt sigma\_policy\_specification}); its main difference 121 \caption{Temporary safety property} 122 \label{sigmacompactunsafe} 123 \end{figure} 124 125 We can now proceed with the lemmas that are needed for algorithm safety. 126 The lemma in Figure~\ref{sigmacompactunsafe} is a temporary formulation of 127 the main property\\ ({\tt sigma\_policy\_specification}). Its main difference 121 128 from the final version is that it uses {\tt instruction\_size\_jmplen} to 122 129 compute the instruction size. This function uses $j$ to compute the span … … 127 134 property. 128 135 136 \begin{figure}[ht] 129 137 \begin{alignat*}{6} 130 138 \mathtt{sigma} & \omit\rlap{$\mathtt{\_safe} \equiv \lambda prefix.\lambda labels.\lambda old\_sigma.\lambda sigma$}\notag\\ … … 149 157 &&&&&\mathrm{long\_jump} \Rightarrow \mathrm{True} 150 158 \end{alignat*} 151 152 This is a more direct safety property: it states that branch instructions are 153 encoded properly, and that no wrong branch instructions are chosen. 159 \caption{Safety property} 160 \label{sigmasafe} 161 \end{figure} 162 163 The lemma in figure~\ref{sigmasafe} is a more direct safety property. It states 164 that branch instructions are encoded properly, and that no wrong branch 165 instructions are chosen. 154 166 155 167 Note that we compute the distance using the memory address of the instruction 156 plus its size : this follows the behaviour of the MCS51 microprocessor, which168 plus its size. This follows the behaviour of the MCS51 microprocessor, which 157 169 increases the program counter directly after fetching, and only then executes 158 170 the branch instruction (by changing the program counter again). 171 172 We now encode some final, simple, properties to make sure that our policy 173 remains consistent, and to keep track of whether the fixed point has been 174 reached. 159 175 160 176 \begin{align*} … … 198 214 The type of an iteration therefore becomes an option type: {\tt None} in case 199 215 the program becomes larger than 64 Kb, or $\mathtt{Some}\ \sigma$ 200 otherwise. We also no longer use a natural number to pass along the number of201 bytes added to the program size, but a boolean that indicates whether we have 202 changed somethingduring the iteration or not.216 otherwise. We also no longer pass along the number of bytes added to the 217 program size, but a boolean that indicates whether we have changed something 218 during the iteration or not. 203 219 204 220 If an iteration returns {\tt None}, we have the following invariant: … … 246 262 is only correct when we have reached the fixed point. 247 263 248 There is another, trivial, invariant if the iteration returns 249 $\mathtt{Some}\ \sigma$: $\mathtt{fst}\ sigma = 2^{16}$. 264 There is another, trivial, invariant in case the iteration returns 265 $\mathtt{Some}\ \sigma$: it must hold that $\mathtt{fst}\ sigma < 2^{16}$. 266 We need this invariant to make sure that addresses do not overflow. 250 267 251 268 The invariants that are taken directly from the fold invariants are trivial to 252 269 prove. 253 270 254 The proof of {\tt nec\_plus\_ultra} works as follows: if we return {\tt None},271 The proof of {\tt nec\_plus\_ultra} goes as follows: if we return {\tt None}, 255 272 then the program size must be greater than 64 Kb. However, since the 256 273 previous iteration did not return {\tt None} (because otherwise we would … … 288 305 longer jumps, in iteration $2n$ every branch instruction must be encoded as 289 306 a long jump. In this case, iteration $2n$ is equal to iteration $2n+1$ and the 290 fix point is reached.307 fixed point is reached.
Note: See TracChangeset
for help on using the changeset viewer.