source: src/ASM/CPP2012-policy/proof.tex @ 3352

Last change on this file since 3352 was 3352, checked in by boender, 7 years ago
  • nicified formulas
File size: 15.4 KB
1\section{The proof}
3In this section, we present the correctness proof for the algorithm in more
4detail.  The main correctness statement is as follows (slightly simplified, here):
7\mathtt{sigma}&\omit\rlap{$\mathtt{\_policy\_specification} \equiv
8\lambda program.\lambda sigma.\lambda policy.$} \notag\\
9  & \omit\rlap{$sigma\ 0 = 0\ \wedge$} \notag\\
10        & \mathbf{let}\ & & \omit\rlap{$instr\_list \equiv code\ program\ \mathbf{in}$} \notag\\
11        &&& \omit\rlap{$\forall ppc.ppc < |instr\_list| \rightarrow$} \notag\\
12        &&& \mathbf{let}\ && pc \equiv sigma\ ppc\ \mathbf{in} \notag\\
13        &&& \mathbf{let}\ && instruction \equiv \mathtt{fetch\_pseudo\_instruction}\ instr\_list\ ppc\ \mathbf{in} \notag\\
14        &&& \mathbf{let}\ && next\_pc \equiv sigma\ (ppc+1)\ \mathbf{in}\notag\\
15        &&&&& next\_pc = pc + \mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction\ \wedge\notag\\
16  &&&&& (pc + \mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction < 2^{16}\ \vee\notag\\
17  &&&&& (\forall ppc'.ppc' < |instr\_list| \rightarrow ppc < ppc' \rightarrow \notag\\
18        &&&&& \mathbf{let}\ instruction' \equiv \mathtt{fetch\_pseudo\_instruction}\ instr\_list\ ppc'\ ppc\_ok'\ \mathbf{in} \notag\\
19        &&&&&\ \mathtt{instruction\_size}\ sigma\ policy\ ppc'\ instruction' = 0)\ \wedge \notag\\
20        &&&&& pc + (\mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction = 2^{16}))
23Informally, this means that when fetching a pseudo-instruction at $ppc$, the
24translation by $\sigma$ of $ppc+1$ is the same as $\sigma(ppc)$ plus the size
25of the instruction at $ppc$.  That is, an instruction is placed consecutively
26after the previous one, and there are no overlaps.
28Instructions are also stocked in
29order: the memory address of the instruction at $ppc$ should be smaller than
30the memory address of the instruction at $ppc+1$. There is one exeception to
31this rule: the instruction at the very end of the program, whose successor
32address can be zero (this is the case where the program size is exactly equal
33to the amount of memory).
35Finally, we enforce that the program starts at address 0, i.e. $\sigma(0) = 0$.
37Since our computation is a least fixed point computation, we must prove
38termination in order to prove correctness: if the algorithm is halted after
39a number of steps without reaching a fixed point, the solution is not
40guaranteed to be correct. More specifically, branch instructions might be
41encoded which do not coincide with the span between their location and their
44Proof of termination rests on the fact that the encoding of branch
45instructions can only grow larger, which means that we must reach a fixed point
46after at most $2n$ iterations, with $n$ the number of branch instructions in
47the program. This worst case is reached if at every iteration, we change the
48encoding of exactly one branch instruction; since the encoding of any branch
49instructions can change first from short to absolute and then from absolute to
50long, there can be at most $2n$ changes.
52The proof has been carried out using the ``Russell'' style from~\cite{Sozeau2006}.
53We have proven some invariants of the {\sc f} function from the previous
54section; these invariants are then used to prove properties that hold for every
55iteration of the fixed point computation; and finally, we can prove some
56properties of the fixed point.
58\subsection{Fold invariants}
60These are the invariants that hold during the fold of {\sc f} over the program,
61and that will later on be used to prove the properties of the iteration.
63Note that during the fixed point computation, the $\sigma$ function is
64implemented as a trie for ease of access; computing $\sigma(x)$ is achieved by looking
65up the value of $x$ in the trie. Actually, during the fold, the value we
66pass along is a pair $\mathbb{N} \times \mathtt{ppc\_pc\_map}$. The first component
67is the number of bytes added to the program so far with respect to
68the previous iteration, and the second component, {\tt ppc\_pc\_map}, is the
69acual $\sigma$ trie.
72\mathtt{out} & \mathtt{\_of\_program\_none} \equiv \lambda prefix.\lambda sigma. \notag\\
73& \forall i.i < 2^{16} \rightarrow (i > |prefix| \leftrightarrow
74 \mathtt{lookup\_opt}\ i\ (\mathtt{snd}\ sigma) = \mathtt{None})
77This invariant states that any pseudo-address not yet examined is not
78present in the lookup trie.
81\mathtt{not} & \mathtt{\_jump\_default} \equiv \lambda prefix.\lambda sigma.\notag\\
82& \forall i.i < |prefix| \rightarrow\notag\\
83& \neg\mathtt{is\_jump}\ (\mathtt{nth}\ i\ prefix) \rightarrow\notag\\
84& \mathtt{lookup}\ i\ (\mathtt{snd}\ sigma) = \mathtt{short\_jump}
87This invariant states that when we try to look up the jump length of a
88pseudo-address where there is no branch instruction, we will get the default
89value, a short jump.
92\mathtt{jump} & \omit\rlap{$\mathtt{\_increase} \equiv \lambda pc.\lambda op.\lambda p.$} \notag\\
93        & \omit\rlap{$\forall i.i < |prefix| \rightarrow$} \notag\\     
94&       \mathbf{let}\  && oj \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ op)\ \mathbf{in} \notag\\
95&       \mathbf{let}\ && j \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ p)\ \mathbf{in} \notag\\
96&&&     \mathtt{jmpleq}\ oj\ j
99This invariant states that between iterations (with $op$ being the previous
100iteration, and $p$ the current one), jump lengths either remain equal or
101increase. It is needed for proving termination.
104\mathtt{sigma} & \omit\rlap{$\mathtt{\_compact\_unsafe} \equiv \lambda prefix.\lambda sigma.$}\notag\\
105& \omit\rlap{$\forall n.n < |prefix| \rightarrow$}\notag\\
106& \mathbf{match}\ && \omit\rlap{$\mathtt{lookup\_opt}\ n\ (\mathtt{snd}\ sigma)\ \mathbf{with}$}\notag\\
107&&& \omit\rlap{$\mathtt{None} \Rightarrow \mathrm{False}$} \notag\\
108&&& \omit\rlap{$\mathtt{Some}\ \langle pc, j \rangle \Rightarrow$} \notag\\
109&&& \mathbf{match}\ && \mathtt{lookup\_opt}\ (n+1)\ (\mathtt{snd}\ sigma)\ \mathbf{with}\notag\\
110&&&&& \mathtt{None} \Rightarrow \mathrm{False} \notag\\
111&&&&& \mathtt{Some}\ \langle pc_1, j_1 \rangle \Rightarrow
112                pc_1 = pc + \notag\\
113&&&&& \ \ \mathtt{instruction\_size\_jmplen}\ j\ (\mathtt{nth}\ n\ prefix)
116This is a temporary formulation of the main property\\
117({\tt sigma\_policy\_specification}); its main difference
118from the final version is that it uses {\tt instruction\_size\_jmplen} to
119compute the instruction size. This function uses $j$ to compute the span
120of branch instructions  (i.e. it uses the $\sigma$ function under construction),
121instead of looking at the distance between source and destination. This is
122because $\sigma$ is still under construction; later on we will prove that after
123the final iteration, {\tt sigma\_compact\_unsafe} is equivalent to the main
127\mathtt{sigma} & \omit\rlap{$\mathtt{\_safe} \equiv \lambda prefix.\lambda labels.\lambda old\_sigma.\lambda sigma$}\notag\\
128& \omit\rlap{$\forall i.i < |prefix| \rightarrow$} \notag\\
129& \omit\rlap{$\forall dest\_label.\mathtt{is\_jump\_to\ (\mathtt{nth}\ i\ prefix})\ dest\_label \rightarrow$} \notag\\
130& \mathbf{let} && \omit\rlap{$\ paddr \equiv \mathtt{lookup}\ labels\ dest\_label\ \mathbf{in}$} \notag\\
131& \mathbf{let} && \omit\rlap{$\ \langle j, src, dest \rangle \equiv$}\notag\\
132&&& \omit\rlap{$\mathbf{if} \ paddr\ \leq\ i\ \mathbf{then}$}\notag\\
133&&&&& \mathbf{let}\ \langle \_, j \rangle \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ sigma)\ \mathbf{in} \notag\\
134&&&&& \mathbf{let}\ \langle pc\_plus\_jl, \_ \rangle \equiv \mathtt{lookup}\ (i+1)\ (\mathtt{snd}\ sigma)\ \mathbf{in}\notag\\
135&&&&& \mathbf{let}\ \langle addr, \_ \rangle \equiv \mathtt{lookup}\ paddr\ (\mathtt{snd}\ sigma)\ \mathbf{in}\notag\\
136&&&&&   \langle j, pc\_plus\_jl, addr \rangle\notag\\
137&&&\mathbf{else} \notag\\
138&&&&&\mathbf{let}\ \langle \_, j \rangle \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ sigma)\ \mathbf{in} \notag\\
139&&&&&\mathbf{let}\ \langle pc\_plus\_jl, \_ \rangle \equiv \mathtt{lookup}\ (i+1)\ (\mathtt{snd}\ old\_sigma)\ \mathbf{in}\notag\\
140&&&&&\mathbf{let}\ \langle addr, \_ \rangle \equiv \mathtt{lookup}\ paddr\ (\mathtt{snd}\ old\_sigma)\ \mathbf{in}\notag\\
141&&&&&\langle j, pc\_plus\_jl, addr \rangle\notag\\
143&&&\mathbf{match} && \ j\ \mathbf{with} \notag\\
144&&&&&\mathrm{short\_jump} \Rightarrow \mathtt{short\_jump\_valid}\ src\ dest\notag\\
145&&&&&\mathrm{absolute\_jump} \Rightarrow \mathtt{absolute\_jump\_valid}\ src\ dest\notag\\
146&&&&&\mathrm{long\_jump} \Rightarrow \mathrm{True}
149This is a more direct safety property: it states that branch instructions are
150encoded properly, and that no wrong branch instructions are chosen.
152Note that we compute the distance using the memory address of the instruction
153plus its size: this follows the behaviour of the MCS-51 microprocessor, which
154increases the program counter directly after fetching, and only then executes
155the branch instruction (by changing the program counter again).
158& \mathtt{lookup}\ 0\ (\mathtt{snd}\ policy) = 0 \notag\\
159& \mathtt{lookup}\ |prefix|\ (\mathtt{snd}\ policy) = \mathtt{fst}\ policy
162These two properties give the values of $\sigma$ for the start and end of the
163program; $\sigma(0) = 0$ and $\sigma(n)$, where $n$ is the number of
164instructions up until now, is equal to the maximum memory address so far.
167& added = 0\ \rightarrow\ \mathtt{policy\_pc\_equal}\ prefix\ old\_sigma\ policy \notag\\
168& \mathtt{policy\_jump\_equal}\ prefix\ old\_sigma\ policy\ \rightarrow\ added = 0
171And finally, two properties that deal with what happens when the previous
172iteration does not change with respect to the current one. $added$ is a
173variable that keeps track of the number of bytes we have added to the program
174size by changing the encoding of branch instructions. If $added$ is 0, the program
175has not changed and vice versa.
177We need to use two different formulations, because the fact that $added$ is 0
178does not guarantee that no branch instructions have changed.  For instance,
179it is possible that we have replaced a short jump with an absolute jump, which
180does not change the size of the branch instruction.
182Therefore {\tt policy\_pc\_equal} states that $old\_sigma_1(x) = sigma_1(x)$,
183whereas {\tt policy\_jump\_equal} states that $old\_sigma_2(x) = sigma_2(x)$.
184This formulation is sufficient to prove termination and compactness.
186Proving these invariants is simple, usually by induction on the prefix length.
188\subsection{Iteration invariants}
190These are invariants that hold after the completion of an iteration. The main
191difference between these invariants and the fold invariants is that after the
192completion of the fold, we check whether the program size does not supersede
19364 Kb, the maximum memory size the MCS-51 can address.
195The type of an iteration therefore becomes an option type: {\tt None} in case
196the program becomes larger than 64 Kb, or $\mathtt{Some}\ \sigma$
197otherwise. We also no longer use a natural number to pass along the number of
198bytes added to the program size, but a boolean that indicates whether we have
199changed something during the iteration or not.
201If an iteration returns {\tt None}, we have the following invariant:
204\mathtt{nec} & \mathtt{\_plus\_ultra} \equiv \lambda program.\lambda p. \notag\\
205&\neg(\forall i.i < |program|\ \rightarrow \notag\\
206& \mathtt{is\_jump}\ (\mathtt{nth}\ i\ program)\ \rightarrow \notag\\
207& \mathtt{lookup}\ i\ (\mathtt{snd}\ p) = \mathrm{long\_jump}).
210This invariant is applied to $old\_sigma$; if our program becomes too large
211for memory, the previous iteration cannot have every branch instruction encoded
212as a long jump. This is needed later in the proof of termination.
214If the iteration returns $\mathtt{Some}\ \sigma$, the invariants
215{\tt out\_of\_program\_none},\\
216{\tt not\_jump\_default}, {\tt jump\_increase},
217and the two invariants that deal with $\sigma(0)$ and $\sigma(n)$ are
218retained without change.
220Instead of using {\tt sigma\_compact\_unsafe}, we can now use the proper
224\mathtt{sigma} & \omit\rlap{$\mathtt{\_compact} \equiv \lambda program.\lambda sigma.$} \notag\\
225& \omit\rlap{$\forall n.n < |program|\ \rightarrow$} \notag\\
226& \mathbf{match}\ && \omit\rlap{$\mathtt{lookup\_opt}\ n\ (\mathtt{snd}\ sigma)\ \mathbf{with}$}\notag\\
227&&& \omit\rlap{$\mathrm{None}\ \Rightarrow\ \mathrm{False}$}\notag\\
228&&& \omit\rlap{$\mathrm{Some}\ \langle pc, j \rangle \Rightarrow$}\notag\\
229&&& \mathbf{match}\ && \mathtt{lookup\_opt}\ (n+1)\ (\mathtt{snd}\ sigma)\ \mathbf{with}\notag\\
230&&&&&   \mathrm{None}\ \Rightarrow\ \mathrm{False}\notag\\
231&&&&& \mathrm{Some} \langle pc1, j1 \rangle \Rightarrow\notag\\
232&&&&& \ \ pc1 = pc + \mathtt{instruction\_size}\ n\ (\mathtt{nth}\ n\ program)
236This is almost the same invariant as ${\tt sigma\_compact\_unsafe}$, but differs in that it
237computes the sizes of branch instructions by looking at the distance between
238position and destination using $\sigma$.
240In actual use, the invariant is qualified: $\sigma$ is compact if there have
241been no changes (i.e. the boolean passed along is {\tt true}). This is to
242reflect the fact that we are doing a least fixed point computation: the result
243is only correct when we have reached the fixed point.
245There is another, trivial, invariant if the iteration returns
246$\mathtt{Some}\ \sigma$: $\mathtt{fst}\ sigma = 2^{16}$.
248The invariants that are taken directly from the fold invariants are trivial to
251The proof of {\tt nec\_plus\_ultra} works as follows: if we return {\tt None},
252then the program size must be greater than 64 Kb. However, since the
253previous iteration did not return {\tt None} (because otherwise we would
254terminate immediately), the program size in the previous iteration must have
255been smaller than 64 Kb.
257Suppose that all the branch instructions in the previous iteration are
258encoded as long jumps. This means that all branch instructions in this
259iteration are long jumps as well, and therefore that both iterations are equal
260in the encoding of their branch instructions. Per the invariant, this means that
261$added = 0$, and therefore that all addresses in both iterations are equal.
262But if all addresses are equal, the program sizes must be equal too, which
263means that the program size in the current iteration must be smaller than
26464 Kb. This contradicts the earlier hypothesis, hence not all branch
265instructions in the previous iteration are encoded as long jumps.
267The proof of {\tt sigma\_compact} follows from {\tt sigma\_compact\_unsafe} and
268the fact that we have reached a fixed point, i.e. the previous iteration and
269the current iteration are the same. This means that the results of
270{\tt instruction\_size\_jmplen} and {\tt instruction\_size} are the same.
272\subsection{Final properties}
274These are the invariants that hold after $2n$ iterations, where $n$ is the
275program size (we use the program size for convenience; we could also use the
276number of branch instructions, but this is more complex). Here, we only
277need {\tt out\_of\_program\_none}, {\tt sigma\_compact} and the fact that
278$\sigma(0) = 0$.
280Termination can now be proved using the fact that there is a $k \leq 2n$, with
281$n$ the length of the program, such that iteration $k$ is equal to iteration
282$k+1$. There are two possibilities: either there is a $k < 2n$ such that this
283property holds, or every iteration up to $2n$ is different. In the latter case,
284since the only changes between the iterations can be from shorter jumps to
285longer jumps, in iteration $2n$ every branch instruction must be encoded as
286a long jump. In this case, iteration $2n$ is equal to iteration $2n+1$ and the
287fixpoint is reached.
Note: See TracBrowser for help on using the repository browser.