Changeset 2096 for src/ASM/CPP2012policy/proof.tex
 Timestamp:
 Jun 15, 2012, 3:25:21 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CPP2012policy/proof.tex
r2091 r2096 1 1 \section{The proof} 2 2 3 In this section, we will present the correctness proof of the algorithm in more 4 detail. 5 6 The main correctness statement is as follows: 3 In this section, we present the correctness proof for the algorithm in more 4 detail. The main correctness statement is as follows (slightly simplified, here): 7 5 8 6 \clearpage 9 7 10 8 \begin{lstlisting} 11 definition 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$))). 9 definition sigma_policy_specification := 10 $\lambda$program: pseudo_assembly_program. 11 $\lambda$sigma: Word $\rightarrow$ Word. 12 $\lambda$policy: Word $\rightarrow$ bool. 13 sigma (zero $\ldots$) = zero $\ldots$ $\wedge$ 14 $\forall$ppc: Word.$\forall$ppc_ok. 15 let $\langle$preamble, instr_list$\rangle$ := program in 16 let pc := sigma ppc in 17 let instruction := 18 \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) in 19 let next_pc := \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in 20 (nat_of_bitvector $\ldots$ ppc $\leq$ instr_list $\rightarrow$ 21 next_pc = add ? pc (bitvector_of_nat $\ldots$ 22 (instruction_size $\ldots$ sigma policy ppc instruction))) 23 $\wedge$ 24 ((nat_of_bitvector $\ldots$ ppc < instr_list $\rightarrow$ 25 nat_of_bitvector $\ldots$ pc < nat_of_bitvector $\ldots$ next_pc) 26 $\vee$ (nat_of_bitvector $\ldots$ ppc = instr_list $\rightarrow$ next_pc = (zero $\ldots$))). 32 27 \end{lstlisting} 33 28 34 29 Informally, this means that when fetching a pseudoinstruction at $ppc$, the 35 30 translation by $\sigma$ of $ppc+1$ is the same as $\sigma(ppc)$ plus the size 36 of the instruction at $ppc$ ; i.e. an instruction is placed immediately31 of the instruction at $ppc$. That is, an instruction is placed consecutively 37 32 after the previous one, and there are no overlaps. 38 33 39 The other condition enforced is the fact that instructions arestocked in34 Instructions are also stocked in 40 35 order: the memory address of the instruction at $ppc$ should be smaller than 41 36 the memory address of the instruction at $ppc+1$. There is one exeception to … … 44 39 to the amount of memory). 45 40 46 And finally, we enforce that the program starts at address 0, i.e. 47 $\sigma(0) = 0$. 41 Finally, we enforce that the program starts at address 0, i.e. $\sigma(0) = 0$. 48 42 49 43 Since our computation is a least fixed point computation, we must prove … … 51 45 a number of steps without reaching a fixed point, the solution is not 52 46 guaranteed to be correct. More specifically, branch instructions might be 53 encoded wh odo not coincide with the span between their location and their47 encoded which do not coincide with the span between their location and their 54 48 destination. 55 49 … … 62 56 long, there can be at most $2n$ changes. 63 57 64 Th is proof has been executed inthe ``Russell'' style from~\cite{Sozeau2006}.58 The proof has been carried out using the ``Russell'' style from~\cite{Sozeau2006}. 65 59 We have proven some invariants of the {\sc f} function from the previous 66 60 section; these invariants are then used to prove properties that hold for every … … 74 68 75 69 Note that during the fixed point computation, the $\sigma$ function is 76 implemented as a trie for ease access; computing $\sigma(x)$ is doneby looking70 implemented as a trie for ease of access; computing $\sigma(x)$ is achieved by looking 77 71 up the value of $x$ in the trie. Actually, during the fold, the value we 78 pass along is a couple $\mathbb{N} \times \mathtt{ppc_pc_map}$. The natural79 numberis the number of bytes added to the program so far with respect to80 the previous iteration, and {\tt ppc\_pc\_map} is a couple of the current81 size of the program and our $\sigma$ function.72 pass along is a pair $\mathbb{N} \times \mathtt{ppc_pc_map}$. The first component 73 is the number of bytes added to the program so far with respect to 74 the previous iteration, and the second component, {\tt ppc\_pc\_map}, is a pair 75 consisting of the current size of the program and our $\sigma$ function. 82 76 83 77 \begin{lstlisting} 84 78 definition out_of_program_none := 85 79 $\lambda$prefix:list labelled_instruction.$\lambda$sigma:ppc_pc_map. 86 $\forall$i.i < 2^16 →(i > prefix $\leftrightarrow$80 $\forall$i.i < 2^16 $\rightarrow$ (i > prefix $\leftrightarrow$ 87 81 bvt_lookup_opt $\ldots$ (bitvector_of_nat ? i) (\snd sigma) = None ?). 88 82 \end{lstlisting} 89 83 90 This invariant states that every pseudoaddress not yet treated cannot be91 foundin the lookup trie.92 93 \begin{lstlisting} 94 definition not_jump_default ≝84 This invariant states that any pseudoaddress not yet examined is not 85 present in the lookup trie. 86 87 \begin{lstlisting} 88 definition not_jump_default := 95 89 $\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$)) →90 $\forall$i.i < prefix $\rightarrow$ 91 ¬is_jump (\snd (nth i ? prefix $\langle$None ?, Comment []$\rangle$)) $\rightarrow$ 98 92 \snd (bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd sigma) 99 93 $\langle$0,short_jump$\rangle$) = short_jump. … … 106 100 \begin{lstlisting} 107 101 definition jump_increase := 108 λprefix:list labelled_instruction.λop:ppc_pc_map.λp:ppc_pc_map.109 ∀i.i ≤ prefix →102 $\lambda$prefix:list labelled_instruction.$\lambda$op:ppc_pc_map.$\lambda$p:ppc_pc_map. 103 $\forall$i.i $\leq$ prefix $\rightarrow$ 110 104 let $\langle$opc,oj$\rangle$ := 111 105 bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd op) $\langle$0,short_jump$\rangle$ in … … 115 109 \end{lstlisting} 116 110 117 This invariant states that between iterations ( $op$ being the previous111 This invariant states that between iterations (with $op$ being the previous 118 112 iteration, and $p$ the current one), jump lengths either remain equal or 119 113 increase. It is needed for proving termination. … … 123 117 \begin{lstlisting} 124 118 definition sigma_compact_unsafe := 125 λprogram:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map.126 ∀n.n < program →119 $\lambda$program:list labelled_instruction.$\lambda$labels:label_map.$\lambda$sigma:ppc_pc_map. 120 $\forall$n.n < program $\rightarrow$ 127 121 match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? n) (\snd sigma) with 128 [ None ⇒False129  Some x ⇒let $\langle$pc,j$\rangle$ := x in122 [ None $\Rightarrow$ False 123  Some x $\Rightarrow$ let $\langle$pc,j$\rangle$ := x in 130 124 match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? (S n)) (\snd sigma) with 131 [ None ⇒False132  Some x1 ⇒ let $\langle$pc1,j1$\rangle$ ≝x1 in125 [ None $\Rightarrow$ False 126  Some x1 $\Rightarrow$ let $\langle$pc1,j1$\rangle$ := x1 in 133 127 pc1 = pc + instruction_size_jmplen j 134 128 (\snd (nth n ? program $\langle$None ?, Comment []$\rangle$))) … … 139 133 This is a temporary formulation of the main property 140 134 ({\tt sigma\_policy\_specification}); its main difference 141 withthe final version is that it uses {\tt instruction\_size\_jmplen} to135 from the final version is that it uses {\tt instruction\_size\_jmplen} to 142 136 compute the instruction size. This function uses $j$ to compute the span 143 137 of branch instructions (i.e. it uses the $\sigma$ function under construction), … … 149 143 \begin{lstlisting} 150 144 definition 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$ :=145 $\lambda$prefix:list labelled_instruction.$\lambda$labels:label_map.$\lambda$added:$\mathbb{N}$. 146 $\lambda$old_sigma:ppc_pc_map.$\lambda$sigma:ppc_pc_map. 147 $\forall$i.i < prefix $\rightarrow$ let $\langle$pc,j$\rangle$ := 154 148 bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd sigma) $\langle$0,short_jump$\rangle$ in 155 149 let pc_plus_jmp_length := bitvector_of_nat ? (\fst (bvt_lookup $\ldots$ … … 178 172 179 173 Note that we compute the distance using the memory address of the instruction 180 plus its size: this is due to the behaviour of the MCS51 architecture, which174 plus its size: this follows the behaviour of the MCS51 microprocessor, which 181 175 increases the program counter directly after fetching, and only then executes 182 176 the branch instruction (by changing the program counter again). … … 194 188 195 189 \begin{lstlisting} 196 (added = 0 →policy_pc_equal prefix old_sigma policy))197 (policy_jump_equal prefix old_sigma policy →added = 0))190 (added = 0 $\rightarrow$ policy_pc_equal prefix old_sigma policy)) 191 (policy_jump_equal prefix old_sigma policy $\rightarrow$ added = 0)) 198 192 \end{lstlisting} 199 193 200 194 And finally, two properties that deal with what happens when the previous 201 iteration does not change with respect to the current one. $added$ is the195 iteration does not change with respect to the current one. $added$ is a 202 196 variable that keeps track of the number of bytes we have added to the program 203 size by changing the encoding of branch instructions ; if thisis 0, the program197 size by changing the encoding of branch instructions. If $added$ is 0, the program 204 198 has not changed and vice versa. 205 199 206 200 We need to use two different formulations, because the fact that $added$ is 0 207 does not guarantee that no branch instructions have changed : it is possible208 that we have replaced a short jump with a absolute jump, which does not change 209 the size of the branch instruction.201 does not guarantee that no branch instructions have changed. For instance, 202 it is possible that we have replaced a short jump with a absolute jump, which 203 does not change the size of the branch instruction. 210 204 211 205 Therefore {\tt policy\_pc\_equal} states that $old\_sigma_1(x) = sigma_1(x)$, … … 220 214 difference between these invariants and the fold invariants is that after the 221 215 completion of the fold, we check whether the program size does not supersede 222 6 5 Kbytes (the maximum memory size the MCS51 can address).216 64 Kb, the maximum memory size the MCS51 can address. 223 217 224 218 The type of an iteration therefore becomes an option type: {\tt None} in case 225 the program becomes larger than 6 5 KBytes, or $\mathtt{Some}\ \sigma$219 the program becomes larger than 64 Kb, or $\mathtt{Some}\ \sigma$ 226 220 otherwise. We also no longer use a natural number to pass along the number of 227 221 bytes added to the program size, but a boolean that indicates whether we have … … 232 226 \begin{lstlisting} 233 227 definition 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$)) →228 $\lambda$program:list labelled_instruction.$\lambda$p:ppc_pc_map. 229 ¬($\forall$i.i < program $\rightarrow$ 230 is_jump (\snd (nth i ? program $\langle$None ?, Comment []$\rangle$)) $\rightarrow$ 237 231 \snd (bvt_lookup $\ldots$ (bitvector_of_nat 16 i) (\snd p) $\langle$0,short_jump$\rangle$) = 238 232 long_jump). … … 241 235 This invariant is applied to $old\_sigma$; if our program becomes too large 242 236 for memory, the previous iteration cannot have every branch instruction encoded 243 as a long jump. This is needed later onin the proof of termination.237 as a long jump. This is needed later in the proof of termination. 244 238 245 239 If the iteration returns $\mathtt{Some}\ \sigma$, the invariants … … 253 247 \begin{lstlisting} 254 248 definition sigma_compact := 255 λprogram:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map.256 ∀n.n < program →249 $\lambda$program:list labelled_instruction.$\lambda$labels:label_map.$\lambda$sigma:ppc_pc_map. 250 $\forall$n.n < program $\rightarrow$ 257 251 match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? n) (\snd sigma) with 258 [ None ⇒False259  Some x ⇒let $\langle$pc,j$\rangle$ := x in252 [ None $\Rightarrow$ False 253  Some x $\Rightarrow$ let $\langle$pc,j$\rangle$ := x in 260 254 match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? (S n)) (\snd sigma) with 261 [ None ⇒False262  Some x1 ⇒let $\langle$pc1,j1$\rangle$ := x1 in255 [ None $\Rightarrow$ False 256  Some x1 $\Rightarrow$ let $\langle$pc1,j1$\rangle$ := x1 in 263 257 pc1 = pc + instruction_size 264 ( λid.bitvector_of_nat ? (lookup_def ?? labels id 0))265 ( λppc.bitvector_of_nat ?258 ($\lambda$id.bitvector_of_nat ? (lookup_def ?? labels id 0)) 259 ($\lambda$ppc.bitvector_of_nat ? 266 260 (\fst (bvt_lookup $\ldots$ ppc (\snd sigma) $\langle$0,short_jump$\rangle$))) 267 ( λppc.jmpeqb long_jump (\snd (bvt_lookup $\ldots$ ppc261 ($\lambda$ppc.jmpeqb long_jump (\snd (bvt_lookup $\ldots$ ppc 268 262 (\snd sigma) $\langle$0,short_jump$\rangle$))) (bitvector_of_nat ? n) 269 263 (\snd (nth n ? program $\langle$None ?, Comment []$\rangle$)) … … 272 266 \end{lstlisting} 273 267 274 This is the same invariant as ${\tt sigma\_compact\_unsafe}$, but insteadit268 This is almost the same invariant as ${\tt sigma\_compact\_unsafe}$, but differs in that it 275 269 computes the sizes of branch instructions by looking at the distance between 276 270 position and destination using $\sigma$. … … 292 286 293 287 The proof of {\tt nec\_plus\_ultra} works as follows: if we return {\tt None}, 294 then the program size must be greater than 6 5 Kbytes. However, since the288 then the program size must be greater than 64 Kb. However, since the 295 289 previous iteration did not return {\tt None} (because otherwise we would 296 290 terminate immediately), the program size in the previous iteration must have 297 been smaller than 6 5 Kbytes.291 been smaller than 64 Kb. 298 292 299 293 Suppose that all the branch instructions in the previous iteration are 300 encode sas long jumps. This means that all branch instructions in this294 encoded as long jumps. This means that all branch instructions in this 301 295 iteration are long jumps as well, and therefore that both iterations are equal 302 296 in the encoding of their branch instructions. Per the invariant, this means that … … 304 298 But if all addresses are equal, the program sizes must be equal too, which 305 299 means that the program size in the current iteration must be smaller than 306 6 5 Kbytes. This contradicts the earlier hypothesis, hence not all branch300 64 Kb. This contradicts the earlier hypothesis, hence not all branch 307 301 instructions in the previous iteration are encoded as long jumps. 308 302 … … 316 310 These are the invariants that hold after $2n$ iterations, where $n$ is the 317 311 program size (we use the program size for convenience; we could also use the 318 number of branch instructions, but this is more compl icated). Here, we only312 number of branch instructions, but this is more complex). Here, we only 319 313 need {\tt out\_of\_program\_none}, {\tt sigma\_compact} and the fact that 320 314 $\sigma(0) = 0$. 321 315 322 Termination can now be prove n throughthe fact that there is a $k \leq 2n$, with316 Termination can now be proved using the fact that there is a $k \leq 2n$, with 323 317 $n$ the length of the program, such that iteration $k$ is equal to iteration 324 318 $k+1$. There are two possibilities: either there is a $k < 2n$ such that this
Note: See TracChangeset
for help on using the changeset viewer.