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

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