Changeset 3473 for Papers/sttt/proof.tex

Sep 22, 2014, 11:25:51 AM (5 years ago)

inlined section into main document, title change

1 edited


  • Papers/sttt/proof.tex

    r3470 r3473  
    1 \section{The proof}
    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~\ref{statement}.
    5 %
    6 \begin{figure}[t]
    7 \small
    8 \begin{alignat*}{6}
    9 \mathtt{sigma}&\omit\rlap{$\mathtt{\_policy\_specification} \equiv
    10 \lambda program.\lambda sigma.$} \notag\\
    11   & \omit\rlap{$sigma\ 0 = 0\ \wedge$} \notag\\
    12         & \mathbf{let}\ & & \omit\rlap{$instr\_list \equiv code\ program\ \mathbf{in}$} \notag\\
    13         &&& \omit\rlap{$\forall ppc.ppc < |instr\_list| \rightarrow$} \notag\\
    14         &&& \mathbf{let}\ && pc \equiv sigma\ ppc\ \mathbf{in} \notag\\
    15         &&& \mathbf{let}\ && instruction \equiv \mathtt{fetch\_pseudo\_instruction}\ instr\_list\ ppc\ \mathbf{in} \notag\\
    16         &&& \mathbf{let}\ && next\_pc \equiv sigma\ (ppc+1)\ \mathbf{in}\notag\\
    17         &&&&& next\_pc = pc + \mathtt{instruction\_size}\ sigma\ ppc\ instruction\ \wedge\notag\\
    18   &&&&& (pc + \mathtt{instruction\_size}\ sigma\ ppc\ instruction < 2^{16}\ \vee\notag\\
    19   &&&&& (\forall ppc'.ppc' < |instr\_list| \rightarrow ppc < ppc' \rightarrow \notag\\
    20         &&&&& \mathbf{let}\ instruction' \equiv \mathtt{fetch\_pseudo\_instruction}\ instr\_list\ ppc'\ \mathbf{in} \notag\\
    21         &&&&&\ \mathtt{instruction\_size}\ sigma\ ppc'\ instruction' = 0)\ \wedge \notag\\
    22         &&&&& pc + \mathtt{instruction\_size}\ sigma\ ppc\ instruction = 2^{16})
    23 \end{alignat*}
    24 \caption{Main correctness statement\label{statement}}
    25 \label{sigmapolspec}
    26 \end{figure}
    27 %
    28 Informally, this means that when fetching a pseudo-instruction at $ppc$, the
    29 translation by $\sigma$ of $ppc+1$ is the same as $\sigma(ppc)$ plus the size
    30 of the instruction at $ppc$.  That is, an instruction is placed consecutively
    31 after the previous one, and there are no overlaps. The rest of the statement deals with memory size: either the next instruction fits within memory ($next\_pc < 2^{16}$) or it ends exactly at the limit memory,
    32 in which case it must be the last translated instruction in the program (enforced by specfiying that the size of all subsequent instructions is 0: there may be comments or cost annotations that are not translated).
    34 Finally, we enforce that the program starts at address 0, i.e. $\sigma(0) = 0$. It may seem strange that we do not explicitly include a safety property stating that every jump instruction is of the right type with respect to its target (akin to the lemma from Figure~\ref{sigmasafe}), but this is not necessary. The distance is recalculated according to the instruction addresses from $\sigma$, which implicitly expresses safety.
    36 Since our computation is a least fixed point computation, we must prove
    37 termination in order to prove correctness: if the algorithm is halted after
    38 a number of steps without reaching a fixed point, the solution is not
    39 guaranteed to be correct. More specifically, branch instructions might be
    40 encoded which do not coincide with the span between their location and their
    41 destination.
    43 Proof of termination rests on the fact that the encoding of branch
    44 instructions can only grow larger, which means that we must reach a fixed point
    45 after at most $2n$ iterations, with $n$ the number of branch instructions in
    46 the program. This worst case is reached if at every iteration, we change the
    47 encoding of exactly one branch instruction; since the encoding of any branch
    48 instruction can change first from short to absolute, and then to long, there
    49 can be at most $2n$ changes.
    51 %The proof has been carried out using the ``Russell'' style from~\cite{Sozeau2006}.
    52 %We have proven some invariants of the {\sc f} function from the previous
    53 %section; these invariants are then used to prove properties that hold for every
    54 %iteration of the fixed point computation; and finally, we can prove some
    55 %properties of the fixed point.
    57 \subsection{Fold invariants}
    59 In this section, we present the invariants that hold during the fold of {\sc f}
    60 over the program. These will be used later on to prove the properties of the
    61 iteration. During the fixed point computation, the $\sigma$ function is
    62 implemented as a trie for ease of access; computing $\sigma(x)$ is achieved by
    63 looking up the value of $x$ in the trie. Actually, during the fold, the value
    64 we pass along is a pair $\mathbb{N} \times \mathtt{ppc\_pc\_map}$. The first
    65 component is the number of bytes added to the program so far with respect to
    66 the previous iteration, and the second component, {\tt ppc\_pc\_map}, is the
    67 actual $\sigma$ trie (which we'll call $strie$ to avoid confusion).
    68 %
    69 {\small
    70 \begin{alignat*}{2}
    71 \mathtt{out} & \mathtt{\_of\_program\_none} \equiv \lambda prefix.\lambda strie. \notag\\
    72 & \forall i.i < 2^{16} \rightarrow (i > |prefix| \leftrightarrow
    73  \mathtt{lookup\_opt}\ i\ (\mathtt{snd}\ strie) = \mathtt{None})
    74 \end{alignat*}}
    75 %
    76 The first invariant states that any pseudo-address not yet examined is not
    77 present in the lookup trie.
    78 %
    79 {\small
    80 \begin{alignat*}{2}
    81 \mathtt{not} & \mathtt{\_jump\_default} \equiv \lambda prefix.\lambda strie.\forall i.i < |prefix| \rightarrow\notag\\
    82 & \neg\mathtt{is\_jump}\ (\mathtt{nth}\ i\ prefix) \rightarrow \mathtt{lookup}\ i\ (\mathtt{snd}\ strie) = \mathtt{short\_jump}
    83 \end{alignat*}}
    84 %
    85 This invariant states that when we try to look up the jump length of a
    86 pseudo-address where there is no branch instruction, we will get the default
    87 value, a short jump.
    88 %
    89 {\small
    90 \begin{alignat*}{4}
    91 \mathtt{jump} & \mathtt{\_increase} \equiv \lambda pc.\lambda op.\lambda p.\forall i.i < |prefix| \rightarrow \notag\\ 
    92 &       \mathbf{let}\  oj \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ op)\ \mathbf{in} \notag\\
    93 &       \mathbf{let}\ j \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ p)\ \mathbf{in}\ \mathtt{jmpleq}\ oj\ j
    94 \end{alignat*}}
    95 %
    96 This invariant states that between iterations (with $op$ being the previous
    97 iteration, and $p$ the current one), jump lengths either remain equal or
    98 increase. It is needed for proving termination.
    99 %
    100 \begin{figure}[h]
    101 \small
    102 \begin{alignat*}{6}
    103 \mathtt{sigma} & \omit\rlap{$\mathtt{\_compact\_unsafe} \equiv \lambda prefix.\lambda strie.\forall n.n < |prefix| \rightarrow$}\notag\\
    104 & \mathbf{match}\ && \omit\rlap{$\mathtt{lookup\_opt}\ n\ (\mathtt{snd}\ strie)\ \mathbf{with}$}\notag\\
    105 &&& \omit\rlap{$\mathtt{None} \Rightarrow \mathrm{False}$} \notag\\
    106 &&& \omit\rlap{$\mathtt{Some}\ \langle pc, j \rangle \Rightarrow$} \notag\\
    107 &&& \mathbf{match}\ && \mathtt{lookup\_opt}\ (n+1)\ (\mathtt{snd}\ strie)\ \mathbf{with}\notag\\
    108 &&&&& \mathtt{None} \Rightarrow \mathrm{False} \notag\\
    109 &&&&& \mathtt{Some}\ \langle pc_1, j_1 \rangle \Rightarrow
    110                 pc_1 = pc + \notag\\
    111 &&&&& \ \ \mathtt{instruction\_size\_jmplen}\ j\ (\mathtt{nth}\ n\ prefix)
    112 \end{alignat*}
    113 \caption{Temporary safety property}
    114 \label{sigmacompactunsafe}
    115 \end{figure}
    116 %
    117 We now proceed with the safety lemmas. The lemma in
    118 Figure~\ref{sigmacompactunsafe} is a temporary formulation of the main
    119 property {\tt sigma\_policy\_specification}. Its main difference from the
    120 final version is that it uses {\tt instruction\_size\_jmplen} to compute the
    121 instruction size. This function uses $j$ to compute the span of branch
    122 instructions  (i.e. it uses the $\sigma$ under construction), instead
    123 of looking at the distance between source and destination. This is because
    124 $\sigma$ is still under construction; we will prove below that after the
    125 final iteration, {\tt sigma\_compact\_unsafe} is equivalent to the main
    126 property in Figure~\ref{sigmasafe} which holds at the end of the computation.
    127 %
    128 \begin{figure}[h]
    129 \small
    130 \begin{alignat*}{6}
    131 \mathtt{sigma} & \omit\rlap{$\mathtt{\_safe} \equiv \lambda prefix.\lambda labels.\lambda old\_strie.\lambda strie.\forall i.i < |prefix| \rightarrow$} \notag\\
    132 & \omit\rlap{$\forall dest\_label.\mathtt{is\_jump\_to\ (\mathtt{nth}\ i\ prefix})\ dest\_label \rightarrow$} \notag\\
    133 & \mathbf{let} && \omit\rlap{$\ paddr \equiv \mathtt{lookup}\ labels\ dest\_label\ \mathbf{in}$} \notag\\
    134 & \mathbf{let} && \omit\rlap{$\ \langle j, src, dest \rangle \equiv \mathbf{if} \ paddr\ \leq\ i\ \mathbf{then}$}\notag\\
    135 &&&&& \mathbf{let}\ \langle \_, j \rangle \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ strie)\ \mathbf{in} \notag\\
    136 &&&&& \mathbf{let}\ \langle pc\_plus\_jl, \_ \rangle \equiv \mathtt{lookup}\ (i+1)\ (\mathtt{snd}\ strie)\ \mathbf{in}\notag\\
    137 &&&&& \mathbf{let}\ \langle addr, \_ \rangle \equiv \mathtt{lookup}\ paddr\ (\mathtt{snd}\ strie)\ \mathbf{in}\notag\\
    138 &&&&&   \langle j, pc\_plus\_jl, addr \rangle\notag\\
    139 &&&\mathbf{else} \notag\\
    140 &&&&&\mathbf{let}\ \langle \_, j \rangle \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ strie)\ \mathbf{in} \notag\\
    141 &&&&&\mathbf{let}\ \langle pc\_plus\_jl, \_ \rangle \equiv \mathtt{lookup}\ (i+1)\ (\mathtt{snd}\ old\_strie)\ \mathbf{in}\notag\\
    142 &&&&&\mathbf{let}\ \langle addr, \_ \rangle \equiv \mathtt{lookup}\ paddr\ (\mathtt{snd}\ old\_strie)\ \mathbf{in}\notag\\
    143 &&&&&\langle j, pc\_plus\_jl, addr \rangle \mathbf{in}\ \notag\\
    144 &&&\mathbf{match} && \ j\ \mathbf{with} \notag\\
    145 &&&&&\mathrm{short\_jump} \Rightarrow \mathtt{short\_jump\_valid}\ src\ dest\notag\\
    146 &&&&&\mathrm{absolute\_jump} \Rightarrow \mathtt{absolute\_jump\_valid}\ src\ dest\notag\\
    147 &&&&&\mathrm{long\_jump} \Rightarrow \mathrm{True}
    148 \end{alignat*}
    149 \caption{Safety property}
    150 \label{sigmasafe}
    151 \end{figure}
    152 %
    153 We compute the distance using the memory address of the instruction
    154 plus its size. This follows the behaviour of the MCS-51 microprocessor, which
    155 increases the program counter directly after fetching, and only then executes
    156 the branch instruction (by changing the program counter again).
    158 There are also some simple, properties to make sure that our policy
    159 remains consistent, and to keep track of whether the fixed point has been
    160 reached. We do not include them here in detail. Two of these properties give the values of $\sigma$ for the start and end of the program; $\sigma(0) = 0$ and $\sigma(n)$, where $n$ is the number of instructions up until now, is equal to the maximum memory address so far. There are also two properties that deal with what happens when the previous
    161 iteration does not change with respect to the current one. $added$ is a
    162 variable that keeps track of the number of bytes we have added to the program
    163 size by changing the encoding of branch instructions. If $added$ is 0, the program
    164 has not changed and vice versa.
    166 %{\small
    167 %\begin{align*}
    168 %& \mathtt{lookup}\ 0\ (\mathtt{snd}\ strie) = 0 \notag\\
    169 %& \mathtt{lookup}\ |prefix|\ (\mathtt{snd}\ strie) = \mathtt{fst}\ strie
    170 %\end{align*}}
    173 %{\small
    174 %\begin{align*}
    175 %& added = 0\ \rightarrow\ \mathtt{policy\_pc\_equal}\ prefix\ old\_strie\ strie \notag\\
    176 %& \mathtt{policy\_jump\_equal}\ prefix\ old\_strie\ strie\ \rightarrow\ added = 0
    177 %\end{align*}}
    179 We need to use two different formulations, because the fact that $added$ is 0
    180 does not guarantee that no branch instructions have changed.  For instance,
    181 it is possible that we have replaced a short jump with an absolute jump, which
    182 does not change the size of the branch instruction. Therefore {\tt policy\_pc\_equal} states that $old\_sigma_1(x) = sigma_1(x)$, whereas {\tt policy\_jump\_equal} states that $old\_sigma_2(x) = sigma_2(x)$. This formulation is sufficient to prove termination and compactness. 
    184 Proving these invariants is simple, usually by induction on the prefix length.
    186 \subsection{Iteration invariants}
    188 These are invariants that hold after the completion of an iteration. The main
    189 difference between these invariants and the fold invariants is that after the
    190 completion of the fold, we check whether the program size does not supersede
    191 64 Kb, the maximum memory size the MCS-51 can address. The type of an iteration therefore becomes an option type: {\tt None} in case
    192 the program becomes larger than 64 Kb, or $\mathtt{Some}\ \sigma$
    193 otherwise. We also no longer pass along the number of bytes added to the
    194 program size, but a boolean that indicates whether we have changed something
    195 during the iteration or not.
    197 If the iteration returns {\tt None}, which means that it has become too large for memory, there is an invariant that states that the previous iteration cannot
    198 have every branch instruction encoded as a long jump. This is needed later in the proof of termination. If the iteration returns $\mathtt{Some}\ \sigma$, the fold invariants are retained without change.
    200 Instead of using {\tt sigma\_compact\_unsafe}, we can now use the proper
    201 invariant:
    202 %
    203 {\small
    204 \begin{alignat*}{6}
    205 \mathtt{sigma} & \omit\rlap{$\mathtt{\_compact} \equiv \lambda program.\lambda sigma.$} \notag\\
    206 & \omit\rlap{$\forall n.n < |program|\ \rightarrow$} \notag\\
    207 & \mathbf{match}\ && \omit\rlap{$\mathtt{lookup\_opt}\ n\ (\mathtt{snd}\ sigma)\ \mathbf{with}$}\notag\\
    208 &&& \omit\rlap{$\mathrm{None}\ \Rightarrow\ \mathrm{False}$}\notag\\
    209 &&& \omit\rlap{$\mathrm{Some}\ \langle pc, j \rangle \Rightarrow$}\notag\\
    210 &&& \mathbf{match}\ && \mathtt{lookup\_opt}\ (n+1)\ (\mathtt{snd}\ sigma)\ \mathbf{with}\notag\\
    211 &&&&&   \mathrm{None}\ \Rightarrow\ \mathrm{False}\notag\\
    212 &&&&& \mathrm{Some} \langle pc1, j1 \rangle \Rightarrow\notag\\
    213 &&&&& \ \ pc1 = pc + \mathtt{instruction\_size}\ n\ (\mathtt{nth}\ n\ program)
    214 \end{alignat*}}
    215 %
    216 This is almost the same invariant as ${\tt sigma\_compact\_unsafe}$, but differs in that it
    217 computes the sizes of branch instructions by looking at the distance between
    218 position and destination using $\sigma$. In actual use, the invariant is qualified: $\sigma$ is compact if there have
    219 been no changes (i.e. the boolean passed along is {\tt true}). This is to
    220 reflect the fact that we are doing a least fixed point computation: the result
    221 is only correct when we have reached the fixed point.
    223 There is another, trivial, invariant in case the iteration returns
    224 $\mathtt{Some}\ \sigma$: it must hold that $\mathtt{fst}\ sigma < 2^{16}$.
    225 We need this invariant to make sure that addresses do not overflow.
    227 The proof of {\tt nec\_plus\_ultra} goes as follows: if we return {\tt None},
    228 then the program size must be greater than 64 Kb. However, since the
    229 previous iteration did not return {\tt None} (because otherwise we would
    230 terminate immediately), the program size in the previous iteration must have
    231 been smaller than 64 Kb.
    233 Suppose that all the branch instructions in the previous iteration are
    234 encoded as long jumps. This means that all branch instructions in this
    235 iteration are long jumps as well, and therefore that both iterations are equal
    236 in the encoding of their branch instructions. Per the invariant, this means that
    237 $added = 0$, and therefore that all addresses in both iterations are equal.
    238 But if all addresses are equal, the program sizes must be equal too, which
    239 means that the program size in the current iteration must be smaller than
    240 64 Kb. This contradicts the earlier hypothesis, hence not all branch
    241 instructions in the previous iteration are encoded as long jumps.
    243 The proof of {\tt sigma\_compact} follows from {\tt sigma\_compact\_unsafe} and
    244 the fact that we have reached a fixed point, i.e. the previous iteration and
    245 the current iteration are the same. This means that the results of
    246 {\tt instruction\_size\_jmplen} and {\tt instruction\_size} are the same.
    248 \subsection{Final properties}
    250 These are the invariants that hold after $2n$ iterations, where $n$ is the
    251 program size (we use the program size for convenience; we could also use the
    252 number of branch instructions, but this is more complex). Here, we only
    253 need {\tt out\_of\_program\_none}, {\tt sigma\_compact} and the fact that
    254 $\sigma(0) = 0$.
    256 Termination can now be proved using the fact that there is a $k \leq 2n$, with
    257 $n$ the length of the program, such that iteration $k$ is equal to iteration
    258 $k+1$. There are two possibilities: either there is a $k < 2n$ such that this
    259 property holds, or every iteration up to $2n$ is different. In the latter case,
    260 since the only changes between the iterations can be from shorter jumps to
    261 longer jumps, in iteration $2n$ every branch instruction must be encoded as
    262 a long jump. In this case, iteration $2n$ is equal to iteration $2n+1$ and the
    263 fixed point is reached.
Note: See TracChangeset for help on using the changeset viewer.