Changeset 3393 for src


Ignore:
Timestamp:
Oct 11, 2013, 4:39:32 PM (7 years ago)
Author:
boender
Message:
  • TACAS stuff
Location:
src/ASM/TACAS2013-policy
Files:
5 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/TACAS2013-policy/algorithm.tex

    r3370 r3393  
    1313execution time.
    1414
    15 On the other hand, the {\tt gcc} compiler suite~\cite{GCC2012}, while compiling
     15On the other hand, the {\tt gcc} compiler suite, while compiling
    1616C on the x86 architecture, uses a greatest fix point algorithm. In other words,
    1717it starts with all branch instructions encoded as the largest jumps
    … …  
    4141When we add absolute jumps, however, it is theoretically possible for a branch
    4242instruction to switch from absolute to long and back, as previously explained.
    43 
    4443Proving termination then becomes difficult, because there is nothing that
    4544precludes a branch instruction from oscillating back and forth between absolute
    … …  
    7271return a smaller or equal solution.
    7372
     73Experiments on the gcc 2.3.3 test suite of C programs have shown that on
     74average, about 25 percent of jumps are encoded as short or absolute jumps by the algorithm. As not all instructions are jumps, this does not make for a large reduction in size, but it can make for a reduction in execution time: if jumps
     75are executed multiple times, for example in loops, the fact that short jumps take less cycles to execute than long jumps can have great effect.
     76
    7477As for complexity, there are at most $2n$ iterations, with $n$ the number of
    7578branch instructions. Practical tests within the CerCo project on small to
    7679medium pieces of code have shown that in almost all cases, a fixed point is
    77 reached in 3 passes. Only in one case did the algorithm need 4.
    78 
    79 This is not surprising: after all, the difference between short/absolute and
     80reached in 3 passes. Only in one case did the algorithm need 4. This is not surprising: after all, the difference between short/absolute and
    8081long jumps is only one byte (three for conditional jumps). For a change from
    8182short/absolute to long to have an effect on other jumps is therefore relatively
    … …  
    8788pseudocode to assembler. More specifically, it is used by the function that
    8889translates pseudo-addresses (natural numbers indicating the position of the
    89 instruction in the program) to actual addresses in memory.
     90instruction in the program) to actual addresses in memory. Note that in pseudocode, all instructions are of size 1.
    9091
    9192Our original intention was to have two different functions, one function
    … …  
    9495intended encoding, and a function $\sigma: \mathbb{N} \rightarrow
    9596\mathtt{Word}$ to associate pseudo-addresses to machine addresses. $\sigma$
    96 would use $\mathtt{policy}$ to determine the size of jump instructions.
    97 
    98 This turned out to be suboptimal from the algorithmic point of view and
     97would use $\mathtt{policy}$ to determine the size of jump instructions. This turned out to be suboptimal from the algorithmic point of view and
    9998impossible to prove correct.
    10099
    … …  
    129128
    130129\begin{figure}[t]
     130\small
    131131\begin{algorithmic}
    132132\Function{f}{$labels$,$old\_sigma$,$instr$,$ppc$,$acc$}
    … …  
    136136        \ElsIf {$instr$ is a forward jump to $j$}
    137137                \State $length \gets \mathrm{jump\_size}(pc,old\_sigma_1(labels(j))+added)$
    138         \Else
    139                 \State $length \gets \mathtt{short\_jump}$
    140138        \EndIf
    141139        \State $old\_length \gets \mathrm{old\_sigma_1}(ppc)$
    … …  
    157155function {\sc f} over the entire program, thus gradually constructing $sigma$.
    158156This constitutes one step in the fixed point calculation; successive steps
    159 repeat the fold until a fixed point is reached.
     157repeat the fold until a fixed point is reached. We have abstracted away the case where an instruction is not a jump, since the size of these instructions is constant.
    160158
    161159Parameters of the function {\sc f} are:
    … …  
    171169                $\sigma$ function under construction.
    172170\end{itemize}
    173 
    174171The first two are parameters that remain the same through one iteration, the
    175172final three are standard parameters for a fold function (including $ppc$,
    … …  
    193190
    194191We cannot use $old\_sigma$ without change: it might be the case that we have
    195 already increased the size of some branch instructions before, making the program
    196 longer and moving every instruction forward. We must compensate for this by
    197 adding the size increase of the program to the label's memory address according
    198 to $old\_sigma$, so that branch instruction spans do not get compromised.
    199 
    200 Note also that we add the pc to $sigma$ at location $ppc+1$, whereas we add the
    201 jump length at location $ppc$. We do this so that $sigma(ppc)$ will always
    202 return a pair with the start address of the instruction at $ppc$ and the
    203 length of its branch instruction (if any); the end address of the program can
    204 be found at $sigma(n+1)$, where $n$ is the number of instructions in the
    205 program.
     192already increased the size of some branch instructions before, making the
     193program longer and moving every instruction forward. We must compensate for this
     194by adding the size increase of the program to the label's memory address
     195according to $old\_sigma$, so that branch instruction spans do not get
     196compromised.
     197
     198%Note also that we add the pc to $sigma$ at location $ppc+1$, whereas we add the
     199%jump length at location $ppc$. We do this so that $sigma(ppc)$ will always
     200%return a pair with the start address of the instruction at $ppc$ and the
     201%length of its branch instruction (if any); the end address of the program can
     202%be found at $sigma(n+1)$, where $n$ is the number of instructions in the
     203%program.

  • src/ASM/TACAS2013-policy/biblio.bib

    r3370 r3393  
    6161  year = {2011},
    6262        key = {SDCC2011}
    63 }
    64 
    65 @misc{GCC2012,
    66         title = {GNU Compiler Collection 4.7.0},
    67         howpublished = {\url{http://gcc.gnu.org/}},
    68         year = {2012},
    69         key = {GCC2012}
    7063}
    7164

  • src/ASM/TACAS2013-policy/conclusion.tex

    r3370 r3393  
    6262surely also interesting to formally prove that the assembler never rejects
    6363programs that should be accepted, i.e. that the algorithm itself is correct.
    64 This was the topic of the current paper.
     64This is the topic of the current paper.
    6565
    6666\subsection{Related work}
    … …  
    7575displacement optimisation algorithm is not needed.
    7676
    77 An offshoot of the CompCert project is the CompCertTSO project, which adds
    78 thread concurrency and synchronisation to the CompCert compiler~\cite{TSO2011}.
    79 This compiler also generates assembly code and therefore does not include a
    80 branch displacement algorithm.
     77%An offshoot of the CompCert project is the CompCertTSO project, which adds
     78%thread concurrency and synchronisation to the CompCert compiler~\cite{TSO2011}.
     79%This compiler also generates assembly code and therefore does not include a
     80%branch displacement algorithm.
    8181 
    82 Finally, there is also the Piton stack~\cite{Moore1996}, which not only includes the
    83 formal verification of a compiler, but also of the machine architecture
    84 targeted by that compiler, a microprocessor called the FM9001.
    85 However, this architecture does not have different
    86 jump sizes (branching is simulated by assigning values to the program counter),
    87 so the branch displacement problem is irrelevant.
     82%Finally, there is also the Piton stack~\cite{Moore1996}, which not only includes the
     83%formal verification of a compiler, but also of the machine architecture
     84%targeted by that compiler, a microprocessor called the FM9001.
     85%However, this architecture does not have different
     86%jump sizes (branching is simulated by assigning values to the program counter),
     87%so the branch displacement problem is irrelevant.
    8888 
    89 \subsection{Formal development}
    90 
    91 All Matita files related to this development can be found on the CerCo
    92 website, \url{http://cerco.cs.unibo.it}. The specific part that contains the
    93 branch displacement algorithm is in the {\tt ASM} subdirectory, in the files
    94 {\tt PolicyFront.ma}, {\tt PolicyStep.ma} and {\tt Policy.ma}.

  • src/ASM/TACAS2013-policy/problem.tex

    r3364 r3393  
    2727contains span-dependent instructions. Furthermore, its maximum addressable
    2828memory size is very small (64 Kb), which makes it important to generate
    29 programs that are as small as possible.
    30 
    31 With this optimisation, however, comes increased complexity and hence
    32 increased possibility for error. We must make sure that the branch instructions
    33 are encoded correctly, otherwise the assembled program will behave
    34 unpredictably.
     29programs that are as small as possible. With this optimisation, however, comes increased complexity and hence increased possibility for error. We must make sure that the branch instructions are encoded correctly, otherwise the assembled program will behave unpredictably.
     30
     31All Matita files related to this development can be found on the CerCo
     32website, \url{http://cerco.cs.unibo.it}. The specific part that contains the
     33branch displacement algorithm is in the {\tt ASM} subdirectory, in the files
     34{\tt PolicyFront.ma}, {\tt PolicyStep.ma} and {\tt Policy.ma}.
    3535
    3636\section{The branch displacement optimisation problem}
    … …  
    123123Here, termination of the smallest fixed point algorithm is easy to prove. All
    124124branch instructions start out encoded as short jumps, which means that the
    125 distance between any branch instruction and its target is as short as possible.
     125distance between any branch instruction and its target is as short as possible
     126(all the intervening jumps are short).
    126127If, in this situation, there is a branch instruction $b$ whose span is not
    127128within the range for a short jump, we can be sure that we can never reach a
    … …  
    147148\begin{figure}[t]
    148149\begin{subfigure}[b]{.45\linewidth}
     150\small
    149151\begin{alltt}
    150152    jmp X
    … …  
    161163\hfill
    162164\begin{subfigure}[b]{.45\linewidth}
     165\small
    163166\begin{alltt}
    164167L\(\sb{0}\): jmp X

  • src/ASM/TACAS2013-policy/proof.tex

    r3370 r3393  
    33In this section, we present the correctness proof for the algorithm in more
    44detail. The main correctness statement is shown, slightly simplified, in~Figure~\ref{statement}.
    5 
    6 \label{sigmapolspec}
     5%
    76\begin{figure}[t]
     7\small
    88\begin{alignat*}{6}
    99\mathtt{sigma}&\omit\rlap{$\mathtt{\_policy\_specification} \equiv
    10 \lambda program.\lambda sigma.\lambda policy.$} \notag\\
     10\lambda program.\lambda sigma.$} \notag\\
    1111  & \omit\rlap{$sigma\ 0 = 0\ \wedge$} \notag\\
    1212        & \mathbf{let}\ & & \omit\rlap{$instr\_list \equiv code\ program\ \mathbf{in}$} \notag\\
    … …  
    1515        &&& \mathbf{let}\ && instruction \equiv \mathtt{fetch\_pseudo\_instruction}\ instr\_list\ ppc\ \mathbf{in} \notag\\
    1616        &&& \mathbf{let}\ && next\_pc \equiv sigma\ (ppc+1)\ \mathbf{in}\notag\\
    17         &&&&& next\_pc = pc + \mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction\ \wedge\notag\\
    18   &&&&& (pc + \mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction < 2^{16}\ \vee\notag\\
     17        &&&&& next\_pc = pc + \mathtt{instruction\_size}\ sigma\ ppc\ instruction\ \wedge\notag\\
     18  &&&&& (pc + \mathtt{instruction\_size}\ sigma\ ppc\ instruction < 2^{16}\ \vee\notag\\
    1919  &&&&& (\forall ppc'.ppc' < |instr\_list| \rightarrow ppc < ppc' \rightarrow \notag\\
    2020        &&&&& \mathbf{let}\ instruction' \equiv \mathtt{fetch\_pseudo\_instruction}\ instr\_list\ ppc'\ ppc\_ok'\ \mathbf{in} \notag\\
    21         &&&&&\ \mathtt{instruction\_size}\ sigma\ policy\ ppc'\ instruction' = 0)\ \wedge \notag\\
    22         &&&&& pc + \mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction = 2^{16})
     21        &&&&&\ \mathtt{instruction\_size}\ sigma\ ppc'\ instruction' = 0)\ \wedge \notag\\
     22        &&&&& pc + \mathtt{instruction\_size}\ sigma\ ppc\ instruction = 2^{16})
    2323\end{alignat*}
    2424\caption{Main correctness statement\label{statement}}
     25\label{sigmapolspec}
    2526\end{figure}
    26 
     27%
    2728Informally, this means that when fetching a pseudo-instruction at $ppc$, the
    2829translation by $\sigma$ of $ppc+1$ is the same as $\sigma(ppc)$ plus the size
    2930of the instruction at $ppc$.  That is, an instruction is placed consecutively
    30 after the previous one, and there are no overlaps.
    31 
    32 Instructions are also stocked in
    33 order: the memory address of the instruction at $ppc$ should be smaller than
    34 the memory address of the instruction at $ppc+1$. There is one exception to
    35 this rule: the instruction at the very end of the program, whose successor
    36 address can be zero (this is the case where the program size is exactly equal
    37 to the amount of memory).
    38 
    39 Finally, we enforce that the program starts at address 0, i.e. $\sigma(0) = 0$.
     31after the previous one, and there are no overlaps. The rest of the statement deals with memory size: either the next instruction fits within memory ($next\_pc < 2^{16}$) or it ends exactly at the limit memory,
     32in which case it must be the last translated instruction in the program (enforced by specfiying that the size of all subsequent instructions is 0: there may be comments or cost annotations that are not translated).
     33
     34Finally, we enforce that the program starts at address 0, i.e. $\sigma(0) = 0$. It may seem strange that we do not explicitly include a safety property stating that every jump instruction is of the right type with respect to its target (akin to the lemma from Figure~\ref{sigmasafe}), but this is not necessary. The distance is recalculated according to the instruction addresses from $\sigma$, which implicitly expresses safety.
    4035
    4136Since our computation is a least fixed point computation, we must prove
    … …  
    5449can be at most $2n$ changes.
    5550
    56 The proof has been carried out using the ``Russell'' style from~\cite{Sozeau2006}.
    57 We have proven some invariants of the {\sc f} function from the previous
    58 section; these invariants are then used to prove properties that hold for every
    59 iteration of the fixed point computation; and finally, we can prove some
    60 properties of the fixed point.
     51%The proof has been carried out using the ``Russell'' style from~\cite{Sozeau2006}.
     52%We have proven some invariants of the {\sc f} function from the previous
     53%section; these invariants are then used to prove properties that hold for every
     54%iteration of the fixed point computation; and finally, we can prove some
     55%properties of the fixed point.
    6156
    6257\subsection{Fold invariants}
    … …  
    6459In this section, we present the invariants that hold during the fold of {\sc f}
    6560over the program. These will be used later on to prove the properties of the
    66 iteration.
    67 
    68 Note that during the fixed point computation, the $\sigma$ function is
     61iteration. During the fixed point computation, the $\sigma$ function is
    6962implemented as a trie for ease of access; computing $\sigma(x)$ is achieved by
    7063looking up the value of $x$ in the trie. Actually, during the fold, the value
    … …  
    7265component is the number of bytes added to the program so far with respect to
    7366the previous iteration, and the second component, {\tt ppc\_pc\_map}, is the
    74 actual $\sigma$ trie.
    75 
     67actual $\sigma$ trie (which we'll call $strie$ to avoid confusion).
     68%
     69{\small
    7670\begin{alignat*}{2}
    77 \mathtt{out} & \mathtt{\_of\_program\_none} \equiv \lambda prefix.\lambda sigma. \notag\\
     71\mathtt{out} & \mathtt{\_of\_program\_none} \equiv \lambda prefix.\lambda strie. \notag\\
    7872& \forall i.i < 2^{16} \rightarrow (i > |prefix| \leftrightarrow
    79  \mathtt{lookup\_opt}\ i\ (\mathtt{snd}\ sigma) = \mathtt{None})
    80 \end{alignat*}
    81 
     73 \mathtt{lookup\_opt}\ i\ (\mathtt{snd}\ strie) = \mathtt{None})
     74\end{alignat*}}
     75%
    8276The first invariant states that any pseudo-address not yet examined is not
    8377present in the lookup trie.
    84 
     78%
     79{\small
    8580\begin{alignat*}{2}
    86 \mathtt{not} & \mathtt{\_jump\_default} \equiv \lambda prefix.\lambda sigma.\notag\\
    87 & \forall i.i < |prefix| \rightarrow\notag\\
    88 & \neg\mathtt{is\_jump}\ (\mathtt{nth}\ i\ prefix) \rightarrow\notag\\
    89 & \mathtt{lookup}\ i\ (\mathtt{snd}\ sigma) = \mathtt{short\_jump}
    90 \end{alignat*}
    91 
     81\mathtt{not} & \mathtt{\_jump\_default} \equiv \lambda prefix.\lambda strie.\forall i.i < |prefix| \rightarrow\notag\\
     82& \neg\mathtt{is\_jump}\ (\mathtt{nth}\ i\ prefix) \rightarrow \mathtt{lookup}\ i\ (\mathtt{snd}\ strie) = \mathtt{short\_jump}
     83\end{alignat*}}
     84%
    9285This invariant states that when we try to look up the jump length of a
    9386pseudo-address where there is no branch instruction, we will get the default
    9487value, a short jump.
    95 
     88%
     89{\small
    9690\begin{alignat*}{4}
    97 \mathtt{jump} & \omit\rlap{$\mathtt{\_increase} \equiv \lambda pc.\lambda op.\lambda p.$} \notag\\
    98         & \omit\rlap{$\forall i.i < |prefix| \rightarrow$} \notag\\     
    99 &       \mathbf{let}\  && oj \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ op)\ \mathbf{in} \notag\\
    100 &       \mathbf{let}\ && j \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ p)\ \mathbf{in} \notag\\
    101 &&&     \mathtt{jmpleq}\ oj\ j
    102 \end{alignat*}
    103 
     91\mathtt{jump} & \mathtt{\_increase} \equiv \lambda pc.\lambda op.\lambda p.\forall i.i < |prefix| \rightarrow \notag\\ 
     92&       \mathbf{let}\  oj \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ op)\ \mathbf{in} \notag\\
     93&       \mathbf{let}\ j \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ p)\ \mathbf{in}\ \mathtt{jmpleq}\ oj\ j
     94\end{alignat*}}
     95%
    10496This invariant states that between iterations (with $op$ being the previous
    10597iteration, and $p$ the current one), jump lengths either remain equal or
    10698increase. It is needed for proving termination.
    107 
    108 \begin{figure}[ht]
    109 \begin{alignat*}{6}
    110 \mathtt{sigma} & \omit\rlap{$\mathtt{\_compact\_unsafe} \equiv \lambda prefix.\lambda sigma.$}\notag\\
    111 & \omit\rlap{$\forall n.n < |prefix| \rightarrow$}\notag\\
    112 & \mathbf{match}\ && \omit\rlap{$\mathtt{lookup\_opt}\ n\ (\mathtt{snd}\ sigma)\ \mathbf{with}$}\notag\\
     99%
     100\begin{figure}[h]
     101\small
     102\begin{alignat*}{6}
     103\mathtt{sigma} & \omit\rlap{$\mathtt{\_compact\_unsafe} \equiv \lambda prefix.\lambda strie.\forall n.n < |prefix| \rightarrow$}\notag\\
     104& \mathbf{match}\ && \omit\rlap{$\mathtt{lookup\_opt}\ n\ (\mathtt{snd}\ strie)\ \mathbf{with}$}\notag\\
    113105&&& \omit\rlap{$\mathtt{None} \Rightarrow \mathrm{False}$} \notag\\
    114106&&& \omit\rlap{$\mathtt{Some}\ \langle pc, j \rangle \Rightarrow$} \notag\\
    115 &&& \mathbf{match}\ && \mathtt{lookup\_opt}\ (n+1)\ (\mathtt{snd}\ sigma)\ \mathbf{with}\notag\\
     107&&& \mathbf{match}\ && \mathtt{lookup\_opt}\ (n+1)\ (\mathtt{snd}\ strie)\ \mathbf{with}\notag\\
    116108&&&&& \mathtt{None} \Rightarrow \mathrm{False} \notag\\
    117109&&&&& \mathtt{Some}\ \langle pc_1, j_1 \rangle \Rightarrow
    … …  
    122114\label{sigmacompactunsafe}
    123115\end{figure}
    124 
     116%
    125117We now proceed with the safety lemmas. The lemma in
    126118Figure~\ref{sigmacompactunsafe} is a temporary formulation of the main
    … …  
    132124$\sigma$ is still under construction; we will prove below that after the
    133125final iteration, {\tt sigma\_compact\_unsafe} is equivalent to the main
    134 property.
    135 
    136 \begin{figure}[ht]
    137 \begin{alignat*}{6}
    138 \mathtt{sigma} & \omit\rlap{$\mathtt{\_safe} \equiv \lambda prefix.\lambda labels.\lambda old\_sigma.\lambda sigma$}\notag\\
    139 & \omit\rlap{$\forall i.i < |prefix| \rightarrow$} \notag\\
     126property in Figure~\ref{sigmasafe} which holds at the end of the computation.
     127%
     128\begin{figure}[h]
     129\small
     130\begin{alignat*}{6}
     131\mathtt{sigma} & \omit\rlap{$\mathtt{\_safe} \equiv \lambda prefix.\lambda labels.\lambda old\_strie.\lambda strie.\forall i.i < |prefix| \rightarrow$} \notag\\
    140132& \omit\rlap{$\forall dest\_label.\mathtt{is\_jump\_to\ (\mathtt{nth}\ i\ prefix})\ dest\_label \rightarrow$} \notag\\
    141133& \mathbf{let} && \omit\rlap{$\ paddr \equiv \mathtt{lookup}\ labels\ dest\_label\ \mathbf{in}$} \notag\\
    142 & \mathbf{let} && \omit\rlap{$\ \langle j, src, dest \rangle \equiv$}\notag\\
    143 &&& \omit\rlap{$\mathbf{if} \ paddr\ \leq\ i\ \mathbf{then}$}\notag\\
    144 &&&&& \mathbf{let}\ \langle \_, j \rangle \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ sigma)\ \mathbf{in} \notag\\
    145 &&&&& \mathbf{let}\ \langle pc\_plus\_jl, \_ \rangle \equiv \mathtt{lookup}\ (i+1)\ (\mathtt{snd}\ sigma)\ \mathbf{in}\notag\\
    146 &&&&& \mathbf{let}\ \langle addr, \_ \rangle \equiv \mathtt{lookup}\ paddr\ (\mathtt{snd}\ sigma)\ \mathbf{in}\notag\\
     134& \mathbf{let} && \omit\rlap{$\ \langle j, src, dest \rangle \equiv \mathbf{if} \ paddr\ \leq\ i\ \mathbf{then}$}\notag\\
     135&&&&& \mathbf{let}\ \langle \_, j \rangle \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ strie)\ \mathbf{in} \notag\\
     136&&&&& \mathbf{let}\ \langle pc\_plus\_jl, \_ \rangle \equiv \mathtt{lookup}\ (i+1)\ (\mathtt{snd}\ strie)\ \mathbf{in}\notag\\
     137&&&&& \mathbf{let}\ \langle addr, \_ \rangle \equiv \mathtt{lookup}\ paddr\ (\mathtt{snd}\ strie)\ \mathbf{in}\notag\\
    147138&&&&&   \langle j, pc\_plus\_jl, addr \rangle\notag\\
    148139&&&\mathbf{else} \notag\\
    149 &&&&&\mathbf{let}\ \langle \_, j \rangle \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ sigma)\ \mathbf{in} \notag\\
    150 &&&&&\mathbf{let}\ \langle pc\_plus\_jl, \_ \rangle \equiv \mathtt{lookup}\ (i+1)\ (\mathtt{snd}\ old\_sigma)\ \mathbf{in}\notag\\
    151 &&&&&\mathbf{let}\ \langle addr, \_ \rangle \equiv \mathtt{lookup}\ paddr\ (\mathtt{snd}\ old\_sigma)\ \mathbf{in}\notag\\
    152 &&&&&\langle j, pc\_plus\_jl, addr \rangle\notag\\
    153 &&&\omit\rlap{$\mathbf{in}$}\notag\\
     140&&&&&\mathbf{let}\ \langle \_, j \rangle \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ strie)\ \mathbf{in} \notag\\
     141&&&&&\mathbf{let}\ \langle pc\_plus\_jl, \_ \rangle \equiv \mathtt{lookup}\ (i+1)\ (\mathtt{snd}\ old\_strie)\ \mathbf{in}\notag\\
     142&&&&&\mathbf{let}\ \langle addr, \_ \rangle \equiv \mathtt{lookup}\ paddr\ (\mathtt{snd}\ old\_strie)\ \mathbf{in}\notag\\
     143&&&&&\langle j, pc\_plus\_jl, addr \rangle \mathbf{in}\ \notag\\
    154144&&&\mathbf{match} && \ j\ \mathbf{with} \notag\\
    155145&&&&&\mathrm{short\_jump} \Rightarrow \mathtt{short\_jump\_valid}\ src\ dest\notag\\
    … …  
    160150\label{sigmasafe}
    161151\end{figure}
    162 
    163 The lemma in figure~\ref{sigmasafe} is a safety property. It states
    164 that branch instructions are encoded properly, and that no wrong branch
    165 instructions are chosen.
    166 
    167 Note that we compute the distance using the memory address of the instruction
     152%
     153We compute the distance using the memory address of the instruction
    168154plus its size. This follows the behaviour of the MCS-51 microprocessor, which
    169155increases the program counter directly after fetching, and only then executes
    170156the branch instruction (by changing the program counter again).
    171157
    172 We now encode some final, simple, properties to make sure that our policy
     158There are also some simple, properties to make sure that our policy
    173159remains consistent, and to keep track of whether the fixed point has been
    174 reached.
    175 
    176 \begin{align*}
    177 & \mathtt{lookup}\ 0\ (\mathtt{snd}\ policy) = 0 \notag\\
    178 & \mathtt{lookup}\ |prefix|\ (\mathtt{snd}\ policy) = \mathtt{fst}\ policy
    179 \end{align*}
    180 
    181 These two properties give the values of $\sigma$ for the start and end of the
    182 program; $\sigma(0) = 0$ and $\sigma(n)$, where $n$ is the number of
    183 instructions up until now, is equal to the maximum memory address so far.
    184 
    185 \begin{align*}
    186 & added = 0\ \rightarrow\ \mathtt{policy\_pc\_equal}\ prefix\ old\_sigma\ policy \notag\\
    187 & \mathtt{policy\_jump\_equal}\ prefix\ old\_sigma\ policy\ \rightarrow\ added = 0
    188 \end{align*}
    189 
    190 And finally, two properties that deal with what happens when the previous
     160reached. We do not include them here in detail. Two of these properties give the values of $\sigma$ for the start and end of the program; $\sigma(0) = 0$ and $\sigma(n)$, where $n$ is the number of instructions up until now, is equal to the maximum memory address so far. There are also two properties that deal with what happens when the previous
    191161iteration does not change with respect to the current one. $added$ is a
    192162variable that keeps track of the number of bytes we have added to the program
    … …  
    194164has not changed and vice versa.
    195165
     166%{\small
     167%\begin{align*}
     168%& \mathtt{lookup}\ 0\ (\mathtt{snd}\ strie) = 0 \notag\\
     169%& \mathtt{lookup}\ |prefix|\ (\mathtt{snd}\ strie) = \mathtt{fst}\ strie
     170%\end{align*}}
     171
     172
     173%{\small
     174%\begin{align*}
     175%& added = 0\ \rightarrow\ \mathtt{policy\_pc\_equal}\ prefix\ old\_strie\ strie \notag\\
     176%& \mathtt{policy\_jump\_equal}\ prefix\ old\_strie\ strie\ \rightarrow\ added = 0
     177%\end{align*}}
     178
    196179We need to use two different formulations, because the fact that $added$ is 0
    197180does not guarantee that no branch instructions have changed.  For instance,
    198181it is possible that we have replaced a short jump with an absolute jump, which
    199 does not change the size of the branch instruction.
    200 
    201 Therefore {\tt policy\_pc\_equal} states that $old\_sigma_1(x) = sigma_1(x)$,
    202 whereas {\tt policy\_jump\_equal} states that $old\_sigma_2(x) = sigma_2(x)$.
    203 This formulation is sufficient to prove termination and compactness.
     182does not change the size of the branch instruction. Therefore {\tt policy\_pc\_equal} states that $old\_sigma_1(x) = sigma_1(x)$, whereas {\tt policy\_jump\_equal} states that $old\_sigma_2(x) = sigma_2(x)$. This formulation is sufficient to prove termination and compactness. 
    204183
    205184Proving these invariants is simple, usually by induction on the prefix length.
    … …  
    210189difference between these invariants and the fold invariants is that after the
    211190completion of the fold, we check whether the program size does not supersede
    212 64 Kb, the maximum memory size the MCS-51 can address.
    213 
    214 The type of an iteration therefore becomes an option type: {\tt None} in case
     19164 Kb, the maximum memory size the MCS-51 can address. The type of an iteration therefore becomes an option type: {\tt None} in case
    215192the program becomes larger than 64 Kb, or $\mathtt{Some}\ \sigma$
    216193otherwise. We also no longer pass along the number of bytes added to the
    217194program size, but a boolean that indicates whether we have changed something
    218 during the iteration or not.
    219 
    220 If an iteration returns {\tt None}, we have the following invariant:
    221 
    222 \begin{alignat*}{2}
    223 \mathtt{nec} & \mathtt{\_plus\_ultra} \equiv \lambda program.\lambda p. \notag\\
    224 &\neg(\forall i.i < |program|\ \rightarrow \notag\\
    225 & \mathtt{is\_jump}\ (\mathtt{nth}\ i\ program)\ \rightarrow \notag\\
    226 & \mathtt{lookup}\ i\ (\mathtt{snd}\ p) = \mathrm{long\_jump}).
    227 \end{alignat*}
    228 
    229 This invariant is applied to $old\_sigma$; if our program becomes too large
    230 for memory, the previous iteration cannot have every branch instruction encoded
    231 as a long jump. This is needed later in the proof of termination.
    232 
    233 If the iteration returns $\mathtt{Some}\ \sigma$, the invariants
    234 {\tt out\_of\_program\_none},\\
    235 {\tt not\_jump\_default}, {\tt jump\_increase},
    236 and the two invariants that deal with $\sigma(0)$ and $\sigma(n)$ are
    237 retained without change.
     195during the iteration or not.
     196
     197If the iteration returns {\tt None}, which means that it has become too large for memory, there is an invariant that states that the previous iteration cannot
     198have every branch instruction encoded as a long jump. This is needed later in the proof of termination. If the iteration returns $\mathtt{Some}\ \sigma$, the fold invariants are retained without change.
    238199
    239200Instead of using {\tt sigma\_compact\_unsafe}, we can now use the proper
    240201invariant:
    241 
     202%
     203{\small
    242204\begin{alignat*}{6}
    243205\mathtt{sigma} & \omit\rlap{$\mathtt{\_compact} \equiv \lambda program.\lambda sigma.$} \notag\\
    … …  
    250212&&&&& \mathrm{Some} \langle pc1, j1 \rangle \Rightarrow\notag\\
    251213&&&&& \ \ pc1 = pc + \mathtt{instruction\_size}\ n\ (\mathtt{nth}\ n\ program)
    252 \end{alignat*}
    253 
    254 
     214\end{alignat*}}
     215%
    255216This is almost the same invariant as ${\tt sigma\_compact\_unsafe}$, but differs in that it
    256217computes the sizes of branch instructions by looking at the distance between
    257 position and destination using $\sigma$.
    258 
    259 In actual use, the invariant is qualified: $\sigma$ is compact if there have
     218position and destination using $\sigma$. In actual use, the invariant is qualified: $\sigma$ is compact if there have
    260219been no changes (i.e. the boolean passed along is {\tt true}). This is to
    261220reflect the fact that we are doing a least fixed point computation: the result
    … …  
    265224$\mathtt{Some}\ \sigma$: it must hold that $\mathtt{fst}\ sigma < 2^{16}$.
    266225We need this invariant to make sure that addresses do not overflow.
    267 
    268 The invariants taken directly from the fold invariants are trivial to prove.
    269226
    270227The proof of {\tt nec\_plus\_ultra} goes as follows: if we return {\tt None},
Note: See TracChangeset for help on using the changeset viewer.