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

Last change on this file since 3361 was 3361, checked in by sacerdot, 6 years ago

15 pages version

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