- Timestamp:
- Jun 15, 2012, 3:25:21 PM (7 years ago)
- Location:
- src/ASM/CPP2012-policy
- Files:
-
- 4 edited
-
algorithm.tex (modified) (13 diffs)
-
conclusion.tex (modified) (4 diffs)
-
problem.tex (modified) (14 diffs)
-
proof.tex (modified) (20 diffs)
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/CPP2012-policy/algorithm.tex
r2091 r2096 4 4 5 5 Given the NP-completeness of the problem, to arrive at an optimal solution 6 within a short space of time (using, for example, a constraint solver) will 7 potentially take a great amountof time.6 (using, for example, a constraint solver) will potentially take a great amount 7 of time. 8 8 9 The SDCC compiler~\cite{SDCC2011}, which has the MCS-51 among its target10 instruction set s, simply encodes every branch instruction as a long jump9 The SDCC compiler~\cite{SDCC2011}, which has a backend targetting the MCS-51 10 instruction set, simply encodes every branch instruction as a long jump 11 11 without taking the distance into account. While certainly correct (the long 12 jump can reach any destination in memory) and rapid, it does result in a less13 than optimal solution.12 jump can reach any destination in memory) and a very fast solution to compute, 13 it results in a less than optimal solution. 14 14 15 The {\tt gcc} compiler suite~\cite{GCC2012}, while compiling C on the x86 16 architecture, uses a greatest fix point algorithm. In other words, it starts 17 off with all branch instructions encoded as the largest jumps available, and 18 then tries to reduce branch instructions as much as possible. 15 On the other hand, the {\tt gcc} compiler suite~\cite{GCC2012}, while compiling 16 C on the x86 architecture, uses a greatest fix point algorithm. In other words, 17 it starts with all branch instructions encoded as the largest jumps 18 available, and then tries to reduce the size of branch instructions as much as 19 possible. 19 20 20 21 Such an algorithm has the advantage that any intermediate result it returns … … 22 23 jump is always possible, and the algorithm only reduces those branch 23 24 instructions whose destination address is in range for a shorter jump. 24 The algorithm can thus be stopped after a determined amountof steps without25 losing correctness.25 The algorithm can thus be stopped after a determined number of steps without 26 sacrificing correctness. 26 27 27 The result, however, is not necessarily optimal , even if the algorithm is run28 until it terminates naturally :the fixed point reached is the {\em greatest}28 The result, however, is not necessarily optimal. Even if the algorithm is run 29 until it terminates naturally, the fixed point reached is the {\em greatest} 29 30 fixed point, not the least fixed point. Furthermore, {\tt gcc} (at least for 30 31 the x86 architecture) only uses short and long jumps. This makes the algorithm 31 more rapid, as shown in the previous section, but also results in a less32 more efficient, as shown in the previous section, but also results in a less 32 33 optimal solution. 33 34 … … 39 40 encoding can only switch from short to long, but never in the other direction. 40 41 When we add absolute jumps, however, it is theoretically possible for a branch 41 instruction to switch from absolute to long and back, as shown in the previous 42 section. 42 instruction to switch from absolute to long and back, as previously explained. 43 43 44 44 Proving termination then becomes difficult, because there is nothing that 45 precludes a branch instruction from switching back and forth between absolute46 and long indefinitely.45 precludes a branch instruction from oscillating back and forth between absolute 46 and long jumps indefinitely. 47 47 48 48 In order to keep the algorithm in the same complexity class and more easily … … 54 54 from absolute to long. 55 55 56 There is one complicating factor : suppose that a branch instruction is encoded56 There is one complicating factor. Suppose that a branch instruction is encoded 57 57 in step $n$ as an absolute jump, but in step $n+1$ it is determined that 58 58 (because of changes elsewhere) it can now be encoded as a short jump. Due to … … 61 61 $n+1$ as well. 62 62 63 This is not necessarily correct , however: abranch instruction that can be64 encoded as a short jump cannot always also be encoded as an absolute jump 65 (a short jump can bridge segments, whereas an absolute jump cannot). Therefore,66 in this situation we decide to encode the branch instruction as a long jump,67 which is always correct.63 This is not necessarily correct. A branch instruction that can be 64 encoded as a short jump cannot always also be encoded as an absolute jump, as a 65 short jump can bridge segments, whereas an absolute jump cannot. Therefore, 66 in this situation we have decided to encode the branch instruction as a long 67 jump, which is always correct. 68 68 69 69 The resulting algorithm, while not optimal, is at least as good as the ones … … 75 75 76 76 The branch displacement algorithm forms part of the translation from 77 pseudo -code to assembler. More specifically, it is used by the function that77 pseudocode to assembler. More specifically, it is used by the function that 78 78 translates pseudo-addresses (natural numbers indicating the position of the 79 79 instruction in the program) to actual addresses in memory. 80 80 81 Theoriginal intention was to have two different functions, one function81 Our original intention was to have two different functions, one function 82 82 $\mathtt{policy}: \mathbb{N} \rightarrow \{\mathtt{short\_jump}, 83 83 \mathtt{absolute\_jump}, \mathtt{long\_jump}\}$ to associate jumps to their 84 84 intended encoding, and a function $\sigma: \mathbb{N} \rightarrow 85 \mathtt{Word}$ to associate pseudo-addresses to actualaddresses. $\sigma$85 \mathtt{Word}$ to associate pseudo-addresses to machine addresses. $\sigma$ 86 86 would use $\mathtt{policy}$ to determine the size of jump instructions. 87 87 … … 91 91 From the algorithmic point of view, in order to create the $\mathtt{policy}$ 92 92 function, we must necessarily have a translation from pseudo-addresses 93 to actualaddresses (i.e. a $\sigma$ function): in order to judge the distance93 to machine addresses (i.e. a $\sigma$ function): in order to judge the distance 94 94 between a jump and its destination, we must know their memory locations. 95 95 Conversely, in order to create the $\sigma$ function, we need to have the … … 104 104 algorithms. We now have a function 105 105 $\sigma: \mathbb{N} \rightarrow \mathtt{Word} \times \mathtt{bool}$ which 106 associates a pseudo-address to a n actualaddress. The boolean denotes a forced106 associates a pseudo-address to a machine address. The boolean denotes a forced 107 107 long jump; as noted in the previous section, if during the fixed point 108 108 computation an absolute jump changes to be potentially re-encoded as a short … … 143 143 \end{figure} 144 144 145 The algorithm, shown in figure~\ref{f:jump_expansion_step}, works by folding the145 The algorithm, shown in Figure~\ref{f:jump_expansion_step}, works by folding the 146 146 function {\sc f} over the entire program, thus gradually constructing $sigma$. 147 147 This constitutes one step in the fixed point calculation; successive steps … … 162 162 163 163 The first two are parameters that remain the same through one iteration, the 164 lastthree are standard parameters for a fold function (including $ppc$,164 final three are standard parameters for a fold function (including $ppc$, 165 165 which is simply the number of instructions of the program already processed). 166 166 … … 169 169 $\sigma: \mathbb{N} \rightarrow \mathbb{N} \times \{\mathtt{short\_jump}, 170 170 \mathtt{absolute\_jump},\mathtt{long\_jump}\}$; a function that associates a 171 pseudo-address with a nmemory address and a jump length. We do this to be able172 to more eas ily compare thejump lengths between iterations. In the algorithm,171 pseudo-address with a memory address and a jump length. We do this to be able 172 to more ease the comparison of jump lengths between iterations. In the algorithm, 173 173 we use the notation $sigma_1(x)$ to denote the memory address corresponding to 174 174 $x$, and $sigma_2(x)$ to denote the jump length corresponding to $x$. … … 182 182 183 183 We cannot use $old\_sigma$ without change: it might be the case that we have 184 already increased the size some branch instructions before, making the program184 already increased the size of some branch instructions before, making the program 185 185 longer and moving every instruction forward. We must compensate for this by 186 186 adding the size increase of the program to the label's memory address according … … 189 189 Note also that we add the pc to $sigma$ at location $ppc+1$, whereas we add the 190 190 jump length at location $ppc$. We do this so that $sigma(ppc)$ will always 191 return a couplewith the start address of the instruction at $ppc$ and the191 return a pair with the start address of the instruction at $ppc$ and the 192 192 length of its branch instruction (if any); the end address of the program can 193 193 be found at $sigma(n+1)$, where $n$ is the number of instructions in the -
src/ASM/CPP2012-policy/conclusion.tex
r2093 r2096 1 1 \section{Conclusion} 2 2 3 In the previous sections ,we have discussed the branch displacement optimisation3 In the previous sections we have discussed the branch displacement optimisation 4 4 problem, presented an optimised solution, and discussed the proof of 5 5 termination and correctness for this algorithm, as formalised in Matita. … … 8 8 optimal solution would need techniques like constraint solvers. While outside 9 9 the scope of the present research, it would be interesting to see if enough 10 heuristics could be f ind to make such a solution practical for implementing11 in an exist entcompiler; this would be especially useful for embedded systems,12 where it is important to have a small solution as possible.10 heuristics could be found to make such a solution practical for implementing 11 in an existing compiler; this would be especially useful for embedded systems, 12 where it is important to have as small solution as possible. 13 13 14 This algorithm is part of a greater whole, the CerCo project, which aims at 15 the complete formalisation and verification of a compiler. More information 14 This algorithm is part of a greater whole, the CerCo project, which aims to 15 complete formalise and verify a concrete cost preserving compiler for a large 16 subset of the C programming language. More information 16 17 on the formalisation of the assembler, of which the present work is a part, 17 18 can be found in a companion publication~\cite{DC2012}. … … 22 23 displacement optimisation algorithm. 23 24 24 The CompCert project is another project aimed at formally verifying a compiler.25 Their backend~\cite{Leroy2009} generates assembly code for (amongst others) the25 The CompCert project is another verified compiler project. 26 Their backend~\cite{Leroy2009} generates assembly code for (amongst others) subsets of the 26 27 PowerPC and x86 (32-bit) architectures. At the assembly code stage, there is 27 28 no distinction between the span-dependent jump instructions, so a branch … … 30 31 An offshoot of the CompCert project is the CompCertTSO project, who add thread 31 32 concurrency and synchronisation to the CompCert compiler~\cite{TSO2011}. This 32 compiler also generate assembly code and therefore does not include a branch33 compiler also generates assembly code and therefore does not include a branch 33 34 displacement algorithm. 34 35 35 There is also Piton~\cite{Moore1996}, which not only includes the36 Finally, there is also the Piton stack~\cite{Moore1996}, which not only includes the 36 37 formal verification of a compiler, but also of the machine architecture 37 targeted by that compiler. However, this architecture does not have different 38 targeted by that compiler, a bespoke microprocessor called the FM9001. 39 However, this architecture does not have different 38 40 jump sizes (branching is simulated by assigning values to the program counter), 39 so the branch displacement problem does not occur.41 so the branch displacement problem is irrelevant. 40 42 41 43 \subsection{Formal development} -
src/ASM/CPP2012-policy/problem.tex
r2091 r2096 5 5 fact that in many architecture sets, the encoding (and therefore size) of some 6 6 instructions depends on the distance to their operand (the instruction 'span'). 7 The branch displacement optimisation problem consists inencoding these7 The branch displacement optimisation problem consists of encoding these 8 8 span-dependent instructions in such a way that the resulting program is as 9 9 small as possible. … … 11 11 This problem is the subject of the present paper. After introducing the problem 12 12 in more detail, we will discuss the solutions used by other compilers, present 13 the algorithm used by usin the CerCo assembler, and discuss its verification,14 that is the proofs of termination and correctness using the Matita theorem15 prover~\cite{Asperti2007}.13 the algorithm we use in the CerCo assembler, and discuss its verification, 14 that is the proofs of termination and correctness using the Matita proof 15 assistant~\cite{Asperti2007}. 16 16 17 17 The research presented in this paper has been executed within the CerCo project … … 19 19 target architecture for this project is the MCS-51, whose instruction set 20 20 contains span-dependent instructions. Furthermore, its maximum addressable 21 memory size is very small (6 5 Kbytes), which makes it important to generate21 memory size is very small (64 Kb), which makes it important to generate 22 22 programs that are as small as possible. 23 23 … … 31 31 In most modern instruction sets that have them, the only span-dependent 32 32 instructions are branch instructions. Taking the ubiquitous x86-64 instruction 33 set as an example, we find that it contains areeleven different forms of the33 set as an example, we find that it contains eleven different forms of the 34 34 unconditional branch instruction, all with different ranges, instruction sizes 35 35 and semantics (only six are valid in 64-bit mode, for example). Some examples 36 are shown in figure~\ref{f:x86jumps}.36 are shown in Figure~\ref{f:x86jumps}. 37 37 38 38 \begin{figure}[h] … … 55 55 The chosen target architecture of the CerCo project is the Intel MCS-51, which 56 56 features three types of branch instructions (or jump instructions; the two terms 57 are used interchangeably), as shown in figure~\ref{f:mcs51jumps}.57 are used interchangeably), as shown in Figure~\ref{f:mcs51jumps}. 58 58 59 59 \begin{figure}[h] … … 78 78 encoded using three branch instructions (for instructions whose logical 79 79 negation is available, it can be done with two branch instructions, but for 80 some instructions , this oppositeis not available); the call instruction is80 some instructions this is not available); the call instruction is 81 81 only available in absolute and long forms. 82 82 83 Note that even though the MCS-51 architecture is much less advanced and more84 simplethan the x86-64 architecture, the basic types of branch instruction83 Note that even though the MCS-51 architecture is much less advanced and simpler 84 than the x86-64 architecture, the basic types of branch instruction 85 85 remain the same: a short jump with a limited range, an intra-segment jump and a 86 86 jump that can reach the entire available memory. 87 87 88 Generally, in the code that is sentto the assembler as input, the only89 difference made between branch instructions is by semantics, not byspan. This88 Generally, in code fed to the assembler as input, the only 89 difference between branch instructions is semantics, not span. This 90 90 means that a distinction is made between an unconditional branch and the 91 91 several kinds of conditional branch, but not between their short, absolute or … … 94 94 The algorithm used by the assembler to encode these branch instructions into 95 95 the different machine instructions is known as the {\em branch displacement 96 algorithm}. The optimisation problem consists in using as small an encoding as96 algorithm}. The optimisation problem consists of finding as small an encoding as 97 97 possible, thus minimising program length and execution time. 98 98 … … 102 102 The canonical solution, as shown by Szymanski~\cite{Szymanski1978} or more 103 103 recently by Dickson~\cite{Dickson2008} for the x86 instruction set, is to use a 104 fixed point algorithm that starts outwith the shortest possible encoding (all105 branch instruction encoded as short jumps, which is very probably not a correct104 fixed point algorithm that starts with the shortest possible encoding (all 105 branch instruction encoded as short jumps, which is likely not a correct 106 106 solution) and then iterates over the program to re-encode those branch 107 107 instructions whose target is outside their range. … … 120 120 situation where the span of $j$ is so small that it can be encoded as a short 121 121 jump. This argument continues to hold throughout the subsequent iterations of 122 the algorithm: short jumps can change into long jumps, but not vice versa123 (spans only increase). Hence, the algorithm either terminateswhen a fixed122 the algorithm: short jumps can change into long jumps, but not \emph{vice versa}, 123 as spans only increase. Hence, the algorithm either terminates early when a fixed 124 124 point is reached or when all short jumps have been changed into long jumps. 125 125 … … 128 128 129 129 However, neither of these claims (termination nor optimality) hold when we add 130 the absolute jump. 131 132 The reason for this is that with absolute jumps, the encoding of a branch 130 the absolute jump, as with absolute jumps, the encoding of a branch 133 131 instruction no longer depends only on the distance between the branch 134 132 instruction and its target: in order for an absolute jump to be possible, they … … 139 137 long if this is not the case). 140 138 141 This invalidates the termination argument: a branch instruction, once encoded 139 \begin{figure}[ht] 140 \begin{alltt} 141 jmp X 142 \vdots 143 L\(\sb{0}\): 144 \vdots 145 jmp L\(\sb{0}\) 146 \end{alltt} 147 \caption{Example of a program where a long jump becomes absolute} 148 \label{f:term_example} 149 \end{figure} 150 151 This invalidates our earlier termination argument: a branch instruction, once encoded 142 152 as a long jump, can be re-encoded during a later iteration as an absolute jump. 143 Consider the program shown in figure~\ref{f:term_example}. At the start of the153 Consider the program shown in Figure~\ref{f:term_example}. At the start of the 144 154 first iteration, both the branch to {\tt X} and the branch to $\mathtt{L}_{0}$ 145 155 are encoded as small jumps. Let us assume that in this case, the placement of … … 156 166 Hence, in the third iteration, the branch to $\mathtt{L}_{0}$ can be encoded as 157 167 an absolute jump. At first glance, there is nothing that prevents us from 158 making a construction where two branch instructions interact in such a way as 159 to keep switching between long and absolute encodings for an indefinite amount 160 of iterations. 161 162 \begin{figure}[h] 163 \begin{alltt} 164 jmp X 165 \vdots 166 L\(\sb{0}\): 167 \vdots 168 jmp L\(\sb{0}\) 169 \end{alltt} 170 \caption{Example of a program where a long jump becomes absolute} 171 \label{f:term_example} 172 \end{figure} 173 174 In fact, this situation mirrors the explanation by 175 Szymanski~\cite{Szymanski1978} of why the branch displacement optimisation 176 problem is NP-complete. In this explanation, a condition for NP-completeness 177 is the fact that programs be allowed to contain {\em pathological} jumps. 178 These are branch instructions that can normally not be encoded as a short(er) 179 jump, but gain this property when some other branch instructions are encoded as 180 a long(er) jump. This is exactly what happens in figure~\ref{f:term_example}: 181 by encoding the first branch instruction as a long jump, another branch 182 instructions switches from long to absolute (which is shorter). 183 184 The optimality argument no longer holds either. Let us consider the program 185 shown in figure~\ref{f:opt_example}. Suppose that the distance between 168 constructing a configuration where two branch instructions interact in such a 169 way as to iterate indefinitely between long and absolute encodings. 170 171 This situation mirrors the explanation by Szymanski~\cite{Szymanski1978} of why 172 the branch displacement optimisation problem is NP-complete. In this explanation, 173 a condition for NP-completeness is the fact that programs be allowed to contain 174 {\em pathological} jumps. These are branch instructions that can normally not be 175 encoded as a short(er) jump, but gain this property when some other branch 176 instructions are encoded as a long(er) jump. This is exactly what happens in 177 Figure~\ref{f:term_example}. By encoding the first branch instruction as a long 178 jump, another branch instruction switches from long to absolute (which is 179 shorter). 180 181 In addition, our previous optimality argument no longer holds. Consider the program 182 shown in Figure~\ref{f:opt_example}. Suppose that the distance between 186 183 $\mathtt{L}_{0}$ and $\mathtt{L}_{1}$ is such that if {\tt jmp X} is encoded 187 184 as a short jump, there is a segment border just after $\mathtt{L}_{1}$. Let … … 189 186 segment, but far enough away from $\mathtt{L}_{1}$ that they cannot be encoded 190 187 as short jumps. 188 189 \begin{figure}[ht] 190 \begin{alltt} 191 L\(\sb{0}\): jmp X 192 X: 193 \vdots 194 L\(\sb{1}\): 195 \vdots 196 jmp L\(\sb{1}\) 197 \vdots 198 jmp L\(\sb{1}\) 199 \vdots 200 jmp L\(\sb{1}\) 201 \vdots 202 \end{alltt} 203 \caption{Example of a program where the fixed-point algorithm is not optimal} 204 \label{f:opt_example} 205 \end{figure} 191 206 192 207 Then, if {\tt jmp X} were to be encoded as a short jump, which is clearly … … 198 213 this solution might actually be smaller than the one reached by the smallest 199 214 fixed point algorithm. 200 201 \begin{figure}[h]202 \begin{alltt}203 L\(\sb{0}\): jmp X204 X:205 \vdots206 L\(\sb{1}\):207 \vdots208 jmp L\(\sb{1}\)209 \vdots210 jmp L\(\sb{1}\)211 \vdots212 jmp L\(\sb{1}\)213 \vdots214 \end{alltt}215 \caption{Example of a program where the fixed-point algorithm is not optimal}216 \label{f:opt_example}217 \end{figure} -
src/ASM/CPP2012-policy/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 pseudo-instruction 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 pseudo-address not yet treated cannot be91 foundin the lookup trie.92 93 \begin{lstlisting} 94 definition not_jump_default ≝84 This invariant states that any pseudo-address 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 MCS-51 architecture, which174 plus its size: this follows the behaviour of the MCS-51 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 MCS-51 can address).216 64 Kb, the maximum memory size the MCS-51 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.
