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

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2012-policy/proof.tex

    r2085 r2091  
    5050termination in order to prove correctness: if the algorithm is halted after
    5151a 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.
     52guaranteed to be correct. More specifically, branch instructions might be
     53encoded who do not coincide with the span between their location and their
     54destination.
     55
     56Proof of termination rests on the fact that the encoding of branch
     57instructions can only grow larger, which means that we must reach a fixed point
     58after at most $2n$ iterations, with $n$ the number of branch instructions in
     59the program. This worst case is reached if at every iteration, we change the
     60encoding of exactly one branch instruction; since the encoding of any branch
     61instructions can change first from short to absolute and then from absolute to
     62long, there can be at most $2n$ changes.
    6163
    6264This proof has been executed in the ``Russell'' style from~\cite{Sozeau2006}.
     
    99101
    100102This invariant states that when we try to look up the jump length of a
    101 pseudo-address where there is no jump, we will get the default value, a short
    102 jump.
     103pseudo-address where there is no branch instruction, we will get the default
     104value, a short jump.
    103105
    104106\begin{lstlisting}
     
    138140({\tt sigma\_policy\_specification}); its main difference
    139141with the final version is that it uses {\tt instruction\_size\_jmplen} to
    140 compute the instruction size. This function uses $j$ to compute the size
    141 of jumps (i.e. it uses the $\sigma$ function under construction), instead
    142 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 main
     142compute the instruction size. This function uses $j$ to compute the span
     143of branch instructions  (i.e. it uses the $\sigma$ function under construction),
     144instead of looking at the distance between source and destination. This is
     145because $\sigma$ is still under construction; later on we will prove that after
     146the final iteration, {\tt sigma\_compact\_unsafe} is equivalent to the main
    145147property.
    146148
     
    172174\end{lstlisting}
    173175
    174 This is a more direct safety property: it states that jump instructions are
    175 encoded properly, and that no wrong jump instructions are chosen.
     176This is a more direct safety property: it states that branch instructions are
     177encoded properly, and that no wrong branch instructions are chosen.
    176178
    177179Note that we compute the distance using the memory address of the instruction
    178180plus its size: this is due to the behaviour of the MCS-51 architecture, which
    179181increases the program counter directly after fetching, and only then executes
    180 the jump.
     182the branch instruction (by changing the program counter again).
    181183
    182184\begin{lstlisting}
     
    199201iteration does not change with respect to the current one. $added$ is the
    200202variable 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 vice
    202 versa.
     203size by changing the encoding of branch instructions; if this is 0, the program
     204has not changed and vice versa.
    203205
    204206We 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.
     207does not guarantee that no branch instructions have changed: it is possible
     208that we have replaced a short jump with a absolute jump, which does not change
     209the size of the branch instruction.
    207210
    208211Therefore {\tt policy\_pc\_equal} states that $old\_sigma_1(x) = sigma_1(x)$,
     
    237240
    238241This 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 long
    240 jump. This is needed later on in the proof of termination.
     242for memory, the previous iteration cannot have every branch instruction encoded
     243as a long jump. This is needed later on in the proof of termination.
    241244
    242245If the iteration returns $\mathtt{Some}\ \sigma$, the invariants
     
    270273
    271274This is the same invariant as ${\tt sigma\_compact\_unsafe}$, but instead it
    272 computes the sizes of jump instructions by looking at the distance between
     275computes the sizes of branch instructions by looking at the distance between
    273276position and destination using $\sigma$.
    274277
     
    294297been smaller than 65 Kbytes.
    295298
    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
     299Suppose that all the branch instructions in the previous iteration are
     300encodes as long jumps. This means that all branch instructions in this
     301iteration are long jumps as well, and therefore that both iterations are equal
     302in the encoding of their branch instructions. Per the invariant, this means that
    299303$added = 0$, and therefore that all addresses in both iterations are equal.
    300304But if all addresses are equal, the program sizes must be equal too, which
    301305means that the program size in the current iteration must be smaller than
    302 65 Kbytes. This contradicts the earlier hypothesis, hence not all jumps in
    303 the previous iteration are long jumps.
     30665 Kbytes. This contradicts the earlier hypothesis, hence not all branch
     307instructions in the previous iteration are encoded as long jumps.
    304308
    305309The proof of {\tt sigma\_compact} follows from {\tt sigma\_compact\_unsafe} and
     
    311315
    312316These 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$.
     317program size (we use the program size for convenience; we could also use the
     318number of branch instructions, but this is more complicated). Here, we only
     319need {\tt out\_of\_program\_none}, {\tt sigma\_compact} and the fact that
     320$\sigma(0) = 0$.
    315321
    316322Termination can now be proven through the fact that there is a $k \leq 2n$, with
     
    319325property holds, or every iteration up to $2n$ is different. In the latter case,
    320326since 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.
     327longer jumps, in iteration $2n$ every branch instruction must be encoded as
     328a long jump. In this case, iteration $2n$ is equal to iteration $2n+1$ and the
     329fixpoint is reached.
Note: See TracChangeset for help on using the changeset viewer.