Changeset 2091 for src/ASM/CPP2012policy/proof.tex
 Timestamp:
 Jun 15, 2012, 1:35:46 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CPP2012policy/proof.tex
r2085 r2091 50 50 termination in order to prove correctness: if the algorithm is halted after 51 51 a number of steps without reaching a fixed point, the solution is not 52 guaranteed to be correct. More specifically, jumps might be encoded whose 53 displacement is too great for the instruction chosen. 54 55 Proof of termination rests on the fact that jumps can only increase, which 56 means that we must reach a fixed point after at most $2n$ iterations, with 57 $2n$ the number of jumps in the program. This worst case is reached if at every 58 iteration, we change the encoding of exactly one jump; since a jump can change 59 from short to absolute and from absolute to long, there can be at most $2n$ 60 changes. 52 guaranteed to be correct. More specifically, branch instructions might be 53 encoded who do not coincide with the span between their location and their 54 destination. 55 56 Proof of termination rests on the fact that the encoding of branch 57 instructions can only grow larger, which means that we must reach a fixed point 58 after at most $2n$ iterations, with $n$ the number of branch instructions in 59 the program. This worst case is reached if at every iteration, we change the 60 encoding of exactly one branch instruction; since the encoding of any branch 61 instructions can change first from short to absolute and then from absolute to 62 long, there can be at most $2n$ changes. 61 63 62 64 This proof has been executed in the ``Russell'' style from~\cite{Sozeau2006}. … … 99 101 100 102 This invariant states that when we try to look up the jump length of a 101 pseudoaddress where there is no jump, we will get the default value, a short102 jump.103 pseudoaddress where there is no branch instruction, we will get the default 104 value, a short jump. 103 105 104 106 \begin{lstlisting} … … 138 140 ({\tt sigma\_policy\_specification}); its main difference 139 141 with the final version is that it uses {\tt instruction\_size\_jmplen} to 140 compute the instruction size. This function uses $j$ to compute the s ize141 of jumps (i.e. it uses the $\sigma$ function under construction), instead142 of looking at the distance between source and destination. This is because 143 $\sigma$ is still under construction; later on we will prove that after the 144 final iteration, {\tt sigma\_compact\_unsafe} is equivalent to the main142 compute the instruction size. This function uses $j$ to compute the span 143 of branch instructions (i.e. it uses the $\sigma$ function under construction), 144 instead of looking at the distance between source and destination. This is 145 because $\sigma$ is still under construction; later on we will prove that after 146 the final iteration, {\tt sigma\_compact\_unsafe} is equivalent to the main 145 147 property. 146 148 … … 172 174 \end{lstlisting} 173 175 174 This is a more direct safety property: it states that jumpinstructions are175 encoded properly, and that no wrong jumpinstructions are chosen.176 This is a more direct safety property: it states that branch instructions are 177 encoded properly, and that no wrong branch instructions are chosen. 176 178 177 179 Note that we compute the distance using the memory address of the instruction 178 180 plus its size: this is due to the behaviour of the MCS51 architecture, which 179 181 increases the program counter directly after fetching, and only then executes 180 the jump.182 the branch instruction (by changing the program counter again). 181 183 182 184 \begin{lstlisting} … … 199 201 iteration does not change with respect to the current one. $added$ is the 200 202 variable that keeps track of the number of bytes we have added to the program 201 size by changing jumps; if this is 0, the program has not changed and vice202 versa.203 size by changing the encoding of branch instructions; if this is 0, the program 204 has not changed and vice versa. 203 205 204 206 We need to use two different formulations, because the fact that $added$ is 0 205 does not guarantee that no jumps have changed: it is possible that we have 206 replaced a short jump with a absolute jump, which does not change the size. 207 does not guarantee that no branch instructions have changed: it is possible 208 that we have replaced a short jump with a absolute jump, which does not change 209 the size of the branch instruction. 207 210 208 211 Therefore {\tt policy\_pc\_equal} states that $old\_sigma_1(x) = sigma_1(x)$, … … 237 240 238 241 This invariant is applied to $old\_sigma$; if our program becomes too large 239 for memory, the previous iteration cannot have every jump encoded as a long240 jump. This is needed later on in the proof of termination.242 for memory, the previous iteration cannot have every branch instruction encoded 243 as a long jump. This is needed later on in the proof of termination. 241 244 242 245 If the iteration returns $\mathtt{Some}\ \sigma$, the invariants … … 270 273 271 274 This is the same invariant as ${\tt sigma\_compact\_unsafe}$, but instead it 272 computes the sizes of jumpinstructions by looking at the distance between275 computes the sizes of branch instructions by looking at the distance between 273 276 position and destination using $\sigma$. 274 277 … … 294 297 been smaller than 65 Kbytes. 295 298 296 Suppose that all the jumps in the previous iteration are long jumps. This means 297 that all jumps in this iteration are long jumps as well, and therefore that 298 both iterations are equal in jumps. Per the invariant, this means that 299 Suppose that all the branch instructions in the previous iteration are 300 encodes as long jumps. This means that all branch instructions in this 301 iteration are long jumps as well, and therefore that both iterations are equal 302 in the encoding of their branch instructions. Per the invariant, this means that 299 303 $added = 0$, and therefore that all addresses in both iterations are equal. 300 304 But if all addresses are equal, the program sizes must be equal too, which 301 305 means that the program size in the current iteration must be smaller than 302 65 Kbytes. This contradicts the earlier hypothesis, hence not all jumps in303 the previous iteration arelong jumps.306 65 Kbytes. This contradicts the earlier hypothesis, hence not all branch 307 instructions in the previous iteration are encoded as long jumps. 304 308 305 309 The proof of {\tt sigma\_compact} follows from {\tt sigma\_compact\_unsafe} and … … 311 315 312 316 These are the invariants that hold after $2n$ iterations, where $n$ is the 313 program size. Here, we only need {\tt out\_of\_program\_none}, 314 {\tt sigma\_compact} and the fact that $\sigma(0) = 0$. 317 program size (we use the program size for convenience; we could also use the 318 number of branch instructions, but this is more complicated). Here, we only 319 need {\tt out\_of\_program\_none}, {\tt sigma\_compact} and the fact that 320 $\sigma(0) = 0$. 315 321 316 322 Termination can now be proven through the fact that there is a $k \leq 2n$, with … … 319 325 property holds, or every iteration up to $2n$ is different. In the latter case, 320 326 since the only changes between the iterations can be from shorter jumps to 321 longer jumps, in iteration $2n$ every jump must be long. In this case, 322 iteration $2n$ is equal to iteration $2n+1$ and the fixpoint is reached. 327 longer jumps, in iteration $2n$ every branch instruction must be encoded as 328 a long jump. In this case, iteration $2n$ is equal to iteration $2n+1$ and the 329 fixpoint is reached.
Note: See TracChangeset
for help on using the changeset viewer.