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

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