Changeset 2091
 Timestamp:
 Jun 15, 2012, 1:35:46 PM (7 years ago)
 Location:
 src/ASM/CPP2012policy
 Files:

 5 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CPP2012policy/algorithm.tex
r2086 r2091 8 8 9 9 The SDCC compiler~\cite{SDCC2011}, which has the MCS51 among its target 10 instruction sets, simply encodes every jump as a long jump without taking the11 distance into account. While certainly correct (the long jump can reach any 12 destination in memory) and rapid, it does result in a less than optimal 13 solution.10 instruction sets, simply encodes every branch instruction as a long jump 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 less 13 than optimal solution. 14 14 15 15 The {\tt gcc} compiler suite~\cite{GCC2012}, while compiling C on the x86 16 16 architecture, uses a greatest fix point algorithm. In other words, it starts 17 off with all jumps encoded as the largest jumps available, and then tries to18 reduce jumps as much as possible.17 off with all branch instructions encoded as the largest jumps available, and 18 then tries to reduce branch instructions as much as possible. 19 19 20 Such an algorithm has the advantage that any intermediate result sit returns21 are correct: the solution where every jump is encoded as a large jump is 22 always possible, and the algorithm only reduces those jumps where the 23 destination address is in range for a shorter jump instruction. The algorithm 24 can thus be stopped after a determined amount of steps without losing 25 correctness.20 Such an algorithm has the advantage that any intermediate result it returns 21 is correct: the solution where every branch instruction is encoded as a large 22 jump is always possible, and the algorithm only reduces those branch 23 instructions whose destination address is in range for a shorter jump. 24 The algorithm can thus be stopped after a determined amount of steps without 25 losing correctness. 26 26 27 27 The result, however, is not necessarily optimal, even if the algorithm is run … … 38 38 previous section: if we only take short and long jumps into account, the jump 39 39 encoding can only switch from short to long, but never in the other direction. 40 When we add absolute jumps, however, it is theoretically possible for a jump to 41 switch from absolute to long and back, as explained in the previous section. 40 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 43 43 44 Proving termination then becomes difficult, because there is nothing that 44 precludes a jump from switching back and forth between absolute and long45 indefinitely.45 precludes a branch instruction from switching back and forth between absolute 46 and long indefinitely. 46 47 47 48 In order to keep the algorithm in the same complexity class and more easily 48 prove termination, we decided to explicitly enforce the `jumps must always 49 increase' requirement: if a jump is encoded as a long jump in one step, it will 50 also be encoded as a long jump in all the following steps. This means that any 51 jump can change at most two times: once from short to absolute (or long), and 52 once from absolute to long. 49 prove termination, we decided to explicitly enforce the `branch instructions 50 must always grow longer' requirement: if a branch instruction is encoded as a 51 long jump in one iteration, it will also be encoded as a long jump in all the 52 following iterations. This means that the encoding of any branch instruction 53 can change at most two times: once from short to absolute (or long), and once 54 from absolute to long. 53 55 54 There is one complicating factor: suppose that a jump is encoded in step $n$ 55 as an absolute jump, but in step $n+1$ it is determined that (because of changes 56 elsewhere) it can now be encoded as a short jump. Due to the requirement that 57 jumps must always increase, this means that the jump will be encoded as an 58 absolute jump in step $n+1$ as well. 56 There is one complicating factor: suppose that a branch instruction is encoded 57 in step $n$ as an absolute jump, but in step $n+1$ it is determined that 58 (because of changes elsewhere) it can now be encoded as a short jump. Due to 59 the requirement that the branch instructions must always grow longer, this 60 means that the branch encoding will be encoded as an absolute jump in step 61 $n+1$ as well. 59 62 60 This is not necessarily correct, however: it is not the case that any short 61 jump can correctly be encoded as an absolute jump (a short jump can bridge 62 segments, whereas an absolute jump cannot). Therefore, in this situation 63 we decide to encode the jump as a long jump, which is always correct. 63 This is not necessarily correct, however: a branch instruction that can be 64 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. 64 68 65 69 The resulting algorithm, while not optimal, is at least as good as the ones 66 70 from SDCC and {\tt gcc}, and potentially better. Its complexity remains 67 the same (there are at most $2n$ iterations, where $n$ is the number of jumps68 in the program).71 the same (there are at most $2n$ iterations, where $n$ is the number of branch 72 instructions in the program). 69 73 70 74 \subsection{The algorithm in detail} … … 172 176 Note that the $\sigma$ function used for label lookup varies depending on 173 177 whether the label is behind our current position or ahead of it. For 174 backward jumps, where the label is behind our current position, we can use178 backward branches, where the label is behind our current position, we can use 175 179 $sigma$ for lookup, since its memory address is already known. However, for 176 forward jumps, the memory address of the address of the label is not yet180 forward branches, the memory address of the address of the label is not yet 177 181 known, so we must use $old\_sigma$. 178 182 179 183 We cannot use $old\_sigma$ without change: it might be the case that we have 180 already changed some jumps before, making the program longer. We must therefore181 compensate for this by adding the size increase of the program to the label's 182 memory address according to $old\_sigma$, so that jump distances do not get 183 compromised.184 already increased the size some branch instructions before, making the program 185 longer and moving every instruction forward. We must compensate for this by 186 adding the size increase of the program to the label's memory address according 187 to $old\_sigma$, so that branch instruction spans do not get compromised. 184 188 185 189 Note also that we add the pc to $sigma$ at location $ppc+1$, whereas we add the 186 190 jump length at location $ppc$. We do this so that $sigma(ppc)$ will always 187 191 return a couple with the start address of the instruction at $ppc$ and the 188 length of its jump; the end address of the program can be found at $sigma(n+1)$, 189 where $n$ is the number of instructions in the program. 192 length of its branch instruction (if any); the end address of the program can 193 be found at $sigma(n+1)$, where $n$ is the number of instructions in the 194 program. 
src/ASM/CPP2012policy/biblio.bib
r2085 r2091 59 59 title = {Small Device {C} Compiler 3.1.0}, 60 60 howpublished = {\url{http://sdcc.sourceforge.net/}}, 61 year = {2011} 61 year = {2011}, 62 key = {SDCC2011} 62 63 } 63 64 … … 65 66 title = {GNU Compiler Collection 4.7.0}, 66 67 howpublished = {\url{http://gcc.gnu.org/}}, 67 year = {2012} 68 year = {2012}, 69 key = {GCC2012} 68 70 } 69 71 … … 94 96 } 95 97 98 @misc {Hyde2006, 99 title = {Branch displacement optimisation}, 100 author = {Randall Hyde}, 101 howpublished = {\url{http://groups.google.com/group/alt.lang.asm/msg/d31192d442accad3}}, 102 year = {2006}, 103 } 104 105 @misc{DC2012, 106 title={On the correctness of an optimising assembler for the Intel MCS51 microprocessor}, 107 author = {Dominic P. Mulligan and Claudio {Sacerdoti Coen}}, 108 year = {2012}, 109 booktitle = {Certified Proofs and Programs {(CPP)}}, 110 note = {Submitted} 111 } 112 113 @article{Asperti2007, 114 author = {Andrea Asperti and Claudio {Sacerdoti Coen} and Enrico Tassi and Stefano Zacchiroli}, 115 title = {User interaction with the {Matita} proof assistant}, 116 journal = {Automated Reasoning}, 117 pages = {109139}, 118 volume = {39}, 119 issue = {2}, 120 year = {2007} 121 } 
src/ASM/CPP2012policy/conclusion.tex
r2085 r2091 15 15 the complete formalisation and verification of a compiler. More information 16 16 on the formalisation of the assembler, of which the present work is a part, 17 can be found in a companion publication .17 can be found in a companion publication~\cite{DC2012}. 18 18 19 19 \subsection{Related work} 
src/ASM/CPP2012policy/problem.tex
r2086 r2091 2 2 3 3 The problem of branch displacement optimisation, also known as jump encoding, is 4 a wellknown problem in assembler design. It is caused by the fact that in 5 many architecture sets, the encoding (and therefore size) of some instructions 6 depends on the distance to their operand (the instruction 'span'). The branch 7 displacement optimisation problem consists in encoding these spandependent 8 instructions in such a way that the resulting program is as small as possible. 4 a wellknown problem in assembler design~\cite{Hyde2006}. It is caused by the 5 fact that in many architecture sets, the encoding (and therefore size) of some 6 instructions depends on the distance to their operand (the instruction 'span'). 7 The branch displacement optimisation problem consists in encoding these 8 spandependent instructions in such a way that the resulting program is as 9 small as possible. 9 10 10 11 This problem is the subject of the present paper. After introducing the problem 11 12 in more detail, we will discuss the solutions used by other compilers, present 12 13 the algorithm used by us in the CerCo assembler, and discuss its verification, 13 that is the proofs of termination and correctness. 14 that is the proofs of termination and correctness using the Matita theorem 15 prover~\cite{Asperti2007}. 14 16 15 17 The research presented in this paper has been executed within the CerCo project … … 21 23 22 24 With this optimisation, however, comes increased complexity and hence 23 increased possibility for error. We must make sure that the jumps are encoded 24 correctly, otherwise the assembled program will behave unpredictably. 25 increased possibility for error. We must make sure that the branch instructions 26 are encoded correctly, otherwise the assembled program will behave 27 unpredictably. 25 28 26 29 \section{The branch displacement optimisation problem} 27 30 28 In most modern instruction sets , the only spandependent instructions are29 branch instructions. Taking the ubiquitous x8664 instruction set as an30 example, we find that it contains are eleven different forms of the31 unconditional jumpinstruction, all with different ranges, instruction sizes31 In most modern instruction sets that have them, the only spandependent 32 instructions are branch instructions. Taking the ubiquitous x8664 instruction 33 set as an example, we find that it contains are eleven different forms of the 34 unconditional branch instruction, all with different ranges, instruction sizes 32 35 and semantics (only six are valid in 64bit mode, for example). Some examples 33 36 are shown in figure~\ref{f:x86jumps}. … … 46 49 \end{tabular} 47 50 \end{center} 48 \caption{List of x86 jumpinstructions}51 \caption{List of x86 branch instructions} 49 52 \label{f:x86jumps} 50 53 \end{figure} … … 67 70 \end{tabular} 68 71 \end{center} 69 \caption{List of MCS51 jumpinstructions}72 \caption{List of MCS51 branch instructions} 70 73 \label{f:mcs51jumps} 71 74 \end{figure} 72 75 73 The conditional jump instruction is only available in short form, which 74 means that a conditional jump outside the short address range has to be 75 encoded using two jumps; the call instruction is only available in 76 absolute and long forms. 76 Conditional branch instructions are only available in short form, which 77 means that a conditional branch outside the short address range has to be 78 encoded using three branch instructions (for instructions whose logical 79 negation is available, it can be done with two branch instructions, but for 80 some instructions, this opposite is not available); the call instruction is 81 only available in absolute and long forms. 77 82 78 83 Note that even though the MCS51 architecture is much less advanced and more 79 simple than the x8664 architecture, the basic types of jump remain the same:80 a short jump with a limited range, an intrasegment jump and a jump that can 81 reach the entire available memory.84 simple than the x8664 architecture, the basic types of branch instruction 85 remain the same: a short jump with a limited range, an intrasegment jump and a 86 jump that can reach the entire available memory. 82 87 83 88 Generally, in the code that is sent to the assembler as input, the only 84 difference made between jumpinstructions is by semantics, not by span. This85 means that a distinction is made between the unconditional jump and the several86 kinds of conditional jump, but not between their short, absolute or long 87 variants.88 89 The algorithm used by the assembler to encode these jumps into the different90 machine instructions is known as the {\tt branch displacement algorithm}. The 91 optimisation problem consists in using as small an encoding as possible, thus92 minimising program length and execution time.89 difference made between branch instructions is by semantics, not by span. This 90 means that a distinction is made between an unconditional branch and the 91 several kinds of conditional branch, but not between their short, absolute or 92 long variants. 93 94 The algorithm used by the assembler to encode these branch instructions into 95 the different machine instructions is known as the {\em branch displacement 96 algorithm}. The optimisation problem consists in using as small an encoding as 97 possible, thus minimising program length and execution time. 93 98 94 99 This problem is known to be NPcomplete~\cite{Robertson1979,Szymanski1978}, … … 98 103 recently by Dickson~\cite{Dickson2008} for the x86 instruction set, is to use a 99 104 fixed point algorithm that starts out with the shortest possible encoding (all 100 jumps encoded as short jumps, which is very probably not a correct solution) 101 and then iterates over the program to reencode those jumps whose target is 102 outside their range.105 branch instruction encoded as short jumps, which is very probably not a correct 106 solution) and then iterates over the program to reencode those branch 107 instructions whose target is outside their range. 103 108 104 109 \subsection*{Adding absolute jumps} … … 109 114 110 115 Here, termination of the smallest fixed point algorithm is easy to prove. All 111 jumps start out encoded as short jumps, which means that the distance between 112 any jump and its target is as short as possible. If, in this situation, there 113 is a jump $j$ whose span is not within the range for a short jump, we can be 114 sure that we can never reach a situation where the span of $j$ is so small that 115 it can be encoded as a short jump. This reasoning holds throughout the 116 subsequent iterations of the algorithm: short jumps can change into long jumps, 117 but not vice versa (spans only increase). Hence, the algorithm either 118 terminates when a fixed point is reached or when all short jumps have been 119 changed into long jumps.116 branch instructions start out encoded as short jumps, which means that the 117 distance between any branch instruction and its target is as short as possible. 118 If, in this situation, there is a branch instruction $b$ whose span is not 119 within the range for a short jump, we can be sure that we can never reach a 120 situation where the span of $j$ is so small that it can be encoded as a short 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 versa 123 (spans only increase). Hence, the algorithm either terminates when a fixed 124 point is reached or when all short jumps have been changed into long jumps. 120 125 121 126 Also, we can be certain that we have reached an optimal solution: a short jump … … 125 130 the absolute jump. 126 131 127 The reason for this is that with absolute jumps, the encoding of a jump no 128 longer depends only on the distance between the jump and its target: in order 129 for an absolute jump to be possible, they need to be in the same segment (for 130 the MCS51, this means that the first 5 bytes of their addresses have to be 131 equal). It is therefore entirely possible for two jumps with the same span to 132 be encoded in different ways (absolute if the jump and its target are in the 133 same segment, long if this is not the case). 134 135 This invalidates the termination argument: a jump, once encoded as a long jump, 136 can be reencoded during a later iteration as an absolute jump. Consider the 137 program shown in figure~\ref{f:term_example}. At the start of the first 138 iteration, both the jump to {\tt X} and the jump to $\mathtt{L}_{0}$ are 139 encoded as small jumps. Let us assume that in this case, the placement of 140 $\mathtt{L}_{0}$ and the jump to it are such that $\mathtt{L}_{0}$ is just 141 outside the segment that contains this jump. Let us also assume that the 142 distance between $\mathtt{L}_{0}$ and the jump to it are too large for the jump 143 to be encoded as a short jump. 144 145 All this means that in the second iteration, the jump to $\mathtt{L}_{0}$ will 146 be encoded as a long jump. If we assume that the jump to {\tt X} is encoded as 147 a long jump as well, the size of the jump will increase and $\mathtt{L}_{0}$ 148 will be `propelled' into the same segment as its jump. Hence, in the third 149 iteration, it can be encoded as an absolute jump. At first glance, there is 150 nothing that prevents us from making a construction where two jumps interact 151 in such a way as to keep switching between long and absolute encodings for 152 an indefinite amount of iterations. 132 The reason for this is that with absolute jumps, the encoding of a branch 133 instruction no longer depends only on the distance between the branch 134 instruction and its target: in order for an absolute jump to be possible, they 135 need to be in the same segment (for the MCS51, this means that the first 5 136 bytes of their addresses have to be equal). It is therefore entirely possible 137 for two branch instructions with the same span to be encoded in different ways 138 (absolute if the branch instruction and its target are in the same segment, 139 long if this is not the case). 140 141 This invalidates the termination argument: a branch instruction, once encoded 142 as a long jump, can be reencoded during a later iteration as an absolute jump. 143 Consider the program shown in figure~\ref{f:term_example}. At the start of the 144 first iteration, both the branch to {\tt X} and the branch to $\mathtt{L}_{0}$ 145 are encoded as small jumps. Let us assume that in this case, the placement of 146 $\mathtt{L}_{0}$ and the branch to it are such that $\mathtt{L}_{0}$ is just 147 outside the segment that contains this branch. Let us also assume that the 148 distance between $\mathtt{L}_{0}$ and the branch to it are too large for the 149 branch instruction to be encoded as a short jump. 150 151 All this means that in the second iteration, the branch to $\mathtt{L}_{0}$ will 152 be encoded as a long jump. If we assume that the branch to {\tt X} is encoded as 153 a long jump as well, the size of the branch instruction will increase and 154 $\mathtt{L}_{0}$ will be `propelled' into the same segment as its branch 155 instruction, because every subsequent instruction will move one byte forward. 156 Hence, in the third iteration, the branch to $\mathtt{L}_{0}$ can be encoded as 157 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. 153 161 154 162 \begin{figure}[h] … … 168 176 problem is NPcomplete. In this explanation, a condition for NPcompleteness 169 177 is the fact that programs be allowed to contain {\em pathological} jumps. 170 These are jumps that can normally not be encoded as a short(er) jump, but gain171 this property when some other jumps are encoded as a long(er) jump. This is172 exactly what happens in figure~\ref{f:term_example}: by encoding the first 173 jump as a long jump, another jump switches from long to absolute 174 (which is shorter).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). 175 183 176 184 The optimality argument no longer holds either. Let us consider the program … … 178 186 $\mathtt{L}_{0}$ and $\mathtt{L}_{1}$ is such that if {\tt jmp X} is encoded 179 187 as a short jump, there is a segment border just after $\mathtt{L}_{1}$. Let 180 us also assume that the three jumps to $\mathtt{L}_{1}$ are all in the same188 us also assume that the three branches to $\mathtt{L}_{1}$ are all in the same 181 189 segment, but far enough away from $\mathtt{L}_{1}$ that they cannot be encoded 182 190 as short jumps. 183 191 184 192 Then, if {\tt jmp X} were to be encoded as a short jump, which is clearly 185 possible, all of the jumps to $\mathtt{L}_{1}$ would have to be encoded as193 possible, all of the branches to $\mathtt{L}_{1}$ would have to be encoded as 186 194 long jumps. However, if {\tt jmp X} were to be encoded as a long jump, and 187 195 therefore increase in size, $\mathtt{L}_{1}$ would be `propelled' across the 188 segment border, so that the three jumps to $\mathtt{L}_{1}$ could be encoded196 segment border, so that the three branches to $\mathtt{L}_{1}$ could be encoded 189 197 as absolute jumps. Depending on the relative sizes of long and absolute jumps, 190 198 this solution might actually be smaller than the one reached by the smallest 
src/ASM/CPP2012policy/proof.tex
r2085 r2091 50 50 termination in order to prove correctness: if the algorithm is halted after 51 51 a number of steps without reaching a fixed point, the solution is not 52 guaranteed to be correct. More specifically, jumps might be encoded whose 53 displacement is too great for the instruction chosen. 54 55 Proof of termination rests on the fact that jumps can only increase, which 56 means that we must reach a fixed point after at most $2n$ iterations, with 57 $2n$ the number of jumps in the program. This worst case is reached if at every 58 iteration, we change the encoding of exactly one jump; since a jump can change 59 from short to absolute and from absolute to long, there can be at most $2n$ 60 changes. 52 guaranteed to be correct. More specifically, branch instructions might be 53 encoded who do not coincide with the span between their location and their 54 destination. 55 56 Proof of termination rests on the fact that the encoding of branch 57 instructions can only grow larger, which means that we must reach a fixed point 58 after at most $2n$ iterations, with $n$ the number of branch instructions in 59 the program. This worst case is reached if at every iteration, we change the 60 encoding of exactly one branch instruction; since the encoding of any branch 61 instructions can change first from short to absolute and then from absolute to 62 long, there can be at most $2n$ changes. 61 63 62 64 This proof has been executed in the ``Russell'' style from~\cite{Sozeau2006}. … … 99 101 100 102 This invariant states that when we try to look up the jump length of a 101 pseudoaddress where there is no jump, we will get the default value, a short102 jump.103 pseudoaddress where there is no branch instruction, we will get the default 104 value, a short jump. 103 105 104 106 \begin{lstlisting} … … 138 140 ({\tt sigma\_policy\_specification}); its main difference 139 141 with the final version is that it uses {\tt instruction\_size\_jmplen} to 140 compute the instruction size. This function uses $j$ to compute the s ize141 of jumps (i.e. it uses the $\sigma$ function under construction), instead142 of looking at the distance between source and destination. This is because 143 $\sigma$ is still under construction; later on we will prove that after the 144 final iteration, {\tt sigma\_compact\_unsafe} is equivalent to the main142 compute the instruction size. This function uses $j$ to compute the span 143 of branch instructions (i.e. it uses the $\sigma$ function under construction), 144 instead of looking at the distance between source and destination. This is 145 because $\sigma$ is still under construction; later on we will prove that after 146 the final iteration, {\tt sigma\_compact\_unsafe} is equivalent to the main 145 147 property. 146 148 … … 172 174 \end{lstlisting} 173 175 174 This is a more direct safety property: it states that jumpinstructions are175 encoded properly, and that no wrong jumpinstructions are chosen.176 This is a more direct safety property: it states that branch instructions are 177 encoded properly, and that no wrong branch instructions are chosen. 176 178 177 179 Note that we compute the distance using the memory address of the instruction 178 180 plus its size: this is due to the behaviour of the MCS51 architecture, which 179 181 increases the program counter directly after fetching, and only then executes 180 the jump.182 the branch instruction (by changing the program counter again). 181 183 182 184 \begin{lstlisting} … … 199 201 iteration does not change with respect to the current one. $added$ is the 200 202 variable that keeps track of the number of bytes we have added to the program 201 size by changing jumps; if this is 0, the program has not changed and vice202 versa.203 size by changing the encoding of branch instructions; if this is 0, the program 204 has not changed and vice versa. 203 205 204 206 We need to use two different formulations, because the fact that $added$ is 0 205 does not guarantee that no jumps have changed: it is possible that we have 206 replaced a short jump with a absolute jump, which does not change the size. 207 does not guarantee that no branch instructions have changed: it is possible 208 that we have replaced a short jump with a absolute jump, which does not change 209 the size of the branch instruction. 207 210 208 211 Therefore {\tt policy\_pc\_equal} states that $old\_sigma_1(x) = sigma_1(x)$, … … 237 240 238 241 This invariant is applied to $old\_sigma$; if our program becomes too large 239 for memory, the previous iteration cannot have every jump encoded as a long240 jump. This is needed later on in the proof of termination.242 for memory, the previous iteration cannot have every branch instruction encoded 243 as a long jump. This is needed later on in the proof of termination. 241 244 242 245 If the iteration returns $\mathtt{Some}\ \sigma$, the invariants … … 270 273 271 274 This is the same invariant as ${\tt sigma\_compact\_unsafe}$, but instead it 272 computes the sizes of jumpinstructions by looking at the distance between275 computes the sizes of branch instructions by looking at the distance between 273 276 position and destination using $\sigma$. 274 277 … … 294 297 been smaller than 65 Kbytes. 295 298 296 Suppose that all the jumps in the previous iteration are long jumps. This means 297 that all jumps in this iteration are long jumps as well, and therefore that 298 both iterations are equal in jumps. Per the invariant, this means that 299 Suppose that all the branch instructions in the previous iteration are 300 encodes as long jumps. This means that all branch instructions in this 301 iteration are long jumps as well, and therefore that both iterations are equal 302 in the encoding of their branch instructions. Per the invariant, this means that 299 303 $added = 0$, and therefore that all addresses in both iterations are equal. 300 304 But if all addresses are equal, the program sizes must be equal too, which 301 305 means that the program size in the current iteration must be smaller than 302 65 Kbytes. This contradicts the earlier hypothesis, hence not all jumps in303 the previous iteration arelong jumps.306 65 Kbytes. This contradicts the earlier hypothesis, hence not all branch 307 instructions in the previous iteration are encoded as long jumps. 304 308 305 309 The proof of {\tt sigma\_compact} follows from {\tt sigma\_compact\_unsafe} and … … 311 315 312 316 These are the invariants that hold after $2n$ iterations, where $n$ is the 313 program size. Here, we only need {\tt out\_of\_program\_none}, 314 {\tt sigma\_compact} and the fact that $\sigma(0) = 0$. 317 program size (we use the program size for convenience; we could also use the 318 number of branch instructions, but this is more complicated). Here, we only 319 need {\tt out\_of\_program\_none}, {\tt sigma\_compact} and the fact that 320 $\sigma(0) = 0$. 315 321 316 322 Termination can now be proven through the fact that there is a $k \leq 2n$, with … … 319 325 property holds, or every iteration up to $2n$ is different. In the latter case, 320 326 since the only changes between the iterations can be from shorter jumps to 321 longer jumps, in iteration $2n$ every jump must be long. In this case, 322 iteration $2n$ is equal to iteration $2n+1$ and the fixpoint is reached. 327 longer jumps, in iteration $2n$ every branch instruction must be encoded as 328 a long jump. In this case, iteration $2n$ is equal to iteration $2n+1$ and the 329 fixpoint is reached.
Note: See TracChangeset
for help on using the changeset viewer.