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

Last change on this file since 2080 was 2080, checked in by boender, 8 years ago
• added references to SDCC and gcc (thanks, Dominic)
• updated sigma policy specification
• changed description of SDCC algorithm to actual SDCC behaviour
File size: 5.7 KB
Line
1\section{The proof}
2
3In this section, we will present the correctness proof of the algorithm in more
4detail.
5
6Since our computation is a least fixed point computation, we must prove
7termination in order to prove correctness: if the algorithm is halted after
8a number of steps without reaching a fixed point, the solution is not
9guaranteed to be correct. More specifically, jumps might be encoded whose
10displacement is too great for the instruction chosen.
11
12Proof of termination rests on the fact that jumps can only increase, which
13means that we must reach a fixed point after at most $2n$ iterations, with
14$2n$ the number of jumps in the program. This worst case is reached if at every
15iteration, we change the encoding of exactly one jump; since a jump can change
16from {\tt short} to {\tt medium} and from {\tt medium} to {\tt long}, there
17can be at most $2n$ changes.
18
19This proof has been executed in the Russell'' style from~\cite{Sozeau2006}.
20We have proven some invariants of the {\sc f} function from the previous
21section; these invariants are then used to prove properties that hold for every
22iteration of the fixed point computation; and finally, we can prove some
23properties of the fixed point.
24
25The invariants for the fold function. Note that during the fixed point
26computation, the $sigma$ functions are implemented as tries, so in order to
27compute $sigma(i)$, we lookup the value for $i$ in the corresponding trie.
28
29\begin{lstlisting}
30(out_of_program_none prefix policy) $\wedge$
31(jump_not_in_policy prefix policy) $\wedge$
32(policy_increase prefix old_sigma policy) $\wedge$
33(policy_compact_unsafe prefix labels policy) $\wedge$
34(policy_safe prefix labels added old_sigma policy) $\wedge$
35(\fst (bvt_lookup $\ldots$
36  (bitvector_of_nat ? 0) (\snd policy) $\langle$0,short_jump$\rangle$) = 0) $\wedge$
37(\fst policy = \fst (bvt_lookup $\ldots$
38  (bitvector_of_nat ? (|prefix|)) (\snd policy) $\langle$0,short_jump$\rangle$)) $\wedge$
39(added = 0 → policy_pc_equal prefix old_sigma policy) $\wedge$
40(policy_jump_equal prefix old_sigma policy → added = 0)
41\end{lstlisting}
42
43These invariants have the following meanings:
44
45\begin{itemize}
46        \item {\tt out\_of\_program\_none} shows that if we try to lookup a value
47beyond the program, we will get an empty result;
48        \item {\tt jump\_not\_in\_policy} shows that an instruction that is not a jump
49will have a {\tt short\_jump} as its associated jump length;
50        \item {\tt policy\_increase} shows that between iterations, jumps either increase (i.e. from {\tt short\_jump} to {\tt medium\_jump} or from {\tt medium\_jump} to {\tt long\_jump}) or remain equal;
51        \item {\tt policy\_compact\_unsafe} shows that the policy is compact (instrucftions directly follow each other and do not overlap);
52        \item {\tt policy\_safe} shows that jumps selected are appropriate for the
53distance between their position and their target, and the jumps selected are
54the smallest possible;
55        \item Then there are two properties that fix the values of $\sigma(0)$ and
56$\sigma(n)$ (with $n$ the size of the program);
57        \item And finally two predicates that link the value of $added$ to reaching
58of a fixed point.
59\end{itemize}
60
61\begin{lstlisting}
62($\Sigma$x:bool × (option ppc_pc_map).
63 let $\langle$no_ch,y$\rangle$ := x in
64 match y with
65 [ None ⇒ nec_plus_ultra program old_policy
66 | Some p ⇒ (out_of_program_none program p) $\wedge$
67    (jump_not_in_policy program p) $\wedge$
68    (policy_increase program old_policy p) $\wedge$
69    (no_ch = true → policy_compact program labels p) $\wedge$
70    (\fst (bvt_lookup $\ldots$
71      (bitvector_of_nat ? 0) (\snd p) $\langle$0,short_jump$\rangle$) = 0) $\wedge$
72    (\fst p = \fst (bvt_lookup $\ldots$
73      (bitvector_of_nat ? (|program|)) (\snd p) $\langle$0,short_jump$\rangle$)) $\wedge$
74    (no_ch = true $\rightarrow$ policy_pc_equal program old_policy p) $\wedge$
75    (policy_jump_equal program old_policy p $\rightarrow$ no_ch = true) $\wedge$
76    (\fst p < 2^16)
77 ])
78\end{lstlisting}
79
80The main correctness statement, then, is as follows:
81
82\begin{lstlisting}
83definition sigma_policy_specification :=:
84$\lambda$program: pseudo_assembly_program.
85$\lambda$sigma: Word → Word.
86$\lambda$policy: Word → bool.
87 sigma (zero $\ldots$) = zero $\ldots$ $\wedge$
88 $\forall$ppc: Word.$\forall$ppc_ok.
89 let instr_list := \snd program in
90 let pc ≝ sigma ppc in
91 let labels := \fst (create_label_cost_map (\snd program)) in
92 let lookup_labels :=
93  $\lambda$x.bitvector_of_nat ? (lookup_def ?? labels x 0) in
94 let instruction :=
95  \fst (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in
96 let next_pc := \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in
97  (nat_of_bitvector $\ldots$ ppc ≤ |instr_list| →
98   next_pc = add 16 pc (bitvector_of_nat $\ldots$
99   (instruction_size lookup_labels sigma policy ppc instruction)))
100  $\wedge$
101  ((nat_of_bitvector $\ldots$ ppc < |instr_list| →
102   nat_of_bitvector $\ldots$ pc < nat_of_bitvector $\ldots$ next_pc)
103  $\vee$ (nat_of_bitvector $\ldots$ ppc = |instr_list| → next_pc = (zero $\ldots$))).
104\end{lstlisting}
105
106Informally, this means that when fetching a pseudo-instruction at $ppc$, the
107translation by $\sigma$ of $ppc+1$ is the same as $\sigma(ppc)$ plus the size
108of the instruction at $ppc$; i.e. an instruction is placed immediately
109after the previous one, and there are no overlaps.
110
111The other condition enforced is the fact that instructions are stocked in
112order: the memory address of the instruction at $ppc$ should be smaller than
113the memory address of the instruction at $ppc+1$. There is one exeception to
114this rule: the instruction at the very end of the program, whose successor
115address can be zero (this is the case where the program size is exactly equal
116to the amount of memory).
117
118And finally, we enforce that the program starts at address 0, i.e.
119$\sigma(0) = 0$.
Note: See TracBrowser for help on using the repository browser.