# Changeset 2091 for src/ASM/CPP2012-policy/proof.tex

Ignore:
Timestamp:
Jun 15, 2012, 1:35:46 PM (8 years ago)
Message:
• systematically changed 'jump' to 'branch'
File:
1 edited

### Legend:

Unmodified
 r2085 termination in order to prove correctness: if the algorithm is halted after a number of steps without reaching a fixed point, the solution is not guaranteed to be correct. More specifically, jumps might be encoded whose displacement is too great for the instruction chosen. Proof of termination rests on the fact that jumps can only increase, which means that we must reach a fixed point after at most $2n$ iterations, with $2n$ the number of jumps in the program. This worst case is reached if at every iteration, we change the encoding of exactly one jump; since a jump can change from short to absolute and from absolute to long, there can be at most $2n$ changes. guaranteed to be correct. More specifically, branch instructions might be encoded who do not coincide with the span between their location and their destination. Proof of termination rests on the fact that the encoding of branch instructions can only grow larger, which means that we must reach a fixed point after at most $2n$ iterations, with $n$ the number of branch instructions in the program. This worst case is reached if at every iteration, we change the encoding of exactly one branch instruction; since the encoding of any branch instructions can change first from short to absolute and then from absolute to long, there can be at most $2n$ changes. This proof has been executed in the Russell'' style from~\cite{Sozeau2006}. This invariant states that when we try to look up the jump length of a pseudo-address where there is no jump, we will get the default value, a short jump. pseudo-address where there is no branch instruction, we will get the default value, a short jump. \begin{lstlisting} ({\tt sigma\_policy\_specification}); its main difference with the final version is that it uses {\tt instruction\_size\_jmplen} to compute the instruction size. This function uses $j$ to compute the size of jumps (i.e. it uses the $\sigma$ function under construction), instead of looking at the distance between source and destination. This is because $\sigma$ is still under construction; later on we will prove that after the final iteration, {\tt sigma\_compact\_unsafe} is equivalent to the main compute the instruction size. This function uses $j$ to compute the span of branch instructions  (i.e. it uses the $\sigma$ function under construction), instead of looking at the distance between source and destination. This is because $\sigma$ is still under construction; later on we will prove that after the final iteration, {\tt sigma\_compact\_unsafe} is equivalent to the main property. \end{lstlisting} This is a more direct safety property: it states that jump instructions are encoded properly, and that no wrong jump instructions are chosen. This 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 is due to the behaviour of the MCS-51 architecture, which increases the program counter directly after fetching, and only then executes the jump. the branch instruction (by changing the program counter again). \begin{lstlisting} iteration does not change with respect to the current one. $added$ is the variable that keeps track of the number of bytes we have added to the program size by changing jumps; if this is 0, the program has not changed and vice versa. size by changing the encoding of branch instructions; if this is 0, the program has not changed and vice versa. We need to use two different formulations, because the fact that $added$ is 0 does not guarantee that no jumps have changed: it is possible that we have replaced a short jump with a absolute jump, which does not change the size. does not guarantee that no branch instructions have changed: it is possible that we have replaced a short jump with a absolute jump, which does not change the size of the branch instruction. Therefore {\tt policy\_pc\_equal} states that $old\_sigma_1(x) = sigma_1(x)$, This invariant is applied to $old\_sigma$; if our program becomes too large for memory, the previous iteration cannot have every jump encoded as a long jump. This is needed later on in the proof of termination. for memory, the previous iteration cannot have every branch instruction encoded as a long jump. This is needed later on in the proof of termination. If the iteration returns $\mathtt{Some}\ \sigma$, the invariants This is the same invariant as ${\tt sigma\_compact\_unsafe}$, but instead it computes the sizes of jump instructions by looking at the distance between computes the sizes of branch instructions by looking at the distance between position and destination using $\sigma$. been smaller than 65 Kbytes. Suppose that all the jumps in the previous iteration are long jumps. This means that all jumps in this iteration are long jumps as well, and therefore that both iterations are equal in jumps. Per the invariant, this means that Suppose that all the branch instructions in the previous iteration are encodes as long jumps. This means that all branch instructions in this iteration are long jumps as well, and therefore that both iterations are equal in the encoding of their branch instructions. Per the invariant, this means that $added = 0$, and therefore that all addresses in both iterations are equal. But if all addresses are equal, the program sizes must be equal too, which means that the program size in the current iteration must be smaller than 65 Kbytes. This contradicts the earlier hypothesis, hence not all jumps in the previous iteration are long jumps. 65 Kbytes. This contradicts the earlier hypothesis, hence not all branch instructions in the previous iteration are encoded as long jumps. The proof of {\tt sigma\_compact} follows from {\tt sigma\_compact\_unsafe} and These are the invariants that hold after $2n$ iterations, where $n$ is the program size. Here, we only need {\tt out\_of\_program\_none}, {\tt sigma\_compact} and the fact that $\sigma(0) = 0$. program size (we use the program size for convenience; we could also use the number of branch instructions, but this is more complicated). Here, we only need {\tt out\_of\_program\_none}, {\tt sigma\_compact} and the fact that $\sigma(0) = 0$. Termination can now be proven through the fact that there is a $k \leq 2n$, with property holds, or every iteration up to $2n$ is different. In the latter case, since the only changes between the iterations can be from shorter jumps to longer jumps, in iteration $2n$ every jump must be long. In this case, iteration $2n$ is equal to iteration $2n+1$ and the fixpoint is reached. 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.