Ignore:
Timestamp:
Jun 17, 2013, 1:08:27 PM (6 years ago)
Author:
boender
Message:
  • added some bits as per Claudio's mail
  • rewrote some small things
  • general reread, spell check, grammar check
  • 16 pages again now
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2012-policy/proof.tex

    r3361 r3362  
    22
    33In this section, we present the correctness proof for the algorithm in more
    4 detail.  The main correctness statement is shown, slightly simplified, in~Figure~\cite{statement}.
    5 
     4detail.  The main correctness statement is shown, slightly simplified, in~Figure~\ref{statement}.
     5
     6\label{sigmapolspec}
    67\begin{figure}[t]
    78\begin{alignat*}{6}
     
    6162\subsection{Fold invariants}
    6263
    63 These are the invariants that hold during the fold of {\sc f} over the program,
    64 and that will later on be used to prove the properties of the iteration.
     64In this section, we present the invariants that hold during the fold of {\sc f}
     65over the program. These will be used later on to prove the properties of the
     66iteration.
    6567
    6668Note that during the fixed point computation, the $\sigma$ function is
    67 implemented as a trie for ease of access; computing $\sigma(x)$ is achieved by looking
    68 up the value of $x$ in the trie. Actually, during the fold, the value we
    69 pass along is a pair $\mathbb{N} \times \mathtt{ppc\_pc\_map}$. The first component
    70 is the number of bytes added to the program so far with respect to
     69implemented as a trie for ease of access; computing $\sigma(x)$ is achieved by
     70looking up the value of $x$ in the trie. Actually, during the fold, the value
     71we pass along is a pair $\mathbb{N} \times \mathtt{ppc\_pc\_map}$. The first
     72component is the number of bytes added to the program so far with respect to
    7173the previous iteration, and the second component, {\tt ppc\_pc\_map}, is the
    72 acual $\sigma$ trie.
     74actual $\sigma$ trie.
    7375
    7476\begin{alignat*}{2}
     
    7880\end{alignat*}
    7981
    80 This invariant states that any pseudo-address not yet examined is not
     82The first invariant states that any pseudo-address not yet examined is not
    8183present in the lookup trie.
    8284
     
    104106increase. It is needed for proving termination.
    105107
     108\begin{figure}[ht]
    106109\begin{alignat*}{6}
    107110\mathtt{sigma} & \omit\rlap{$\mathtt{\_compact\_unsafe} \equiv \lambda prefix.\lambda sigma.$}\notag\\
     
    116119&&&&& \ \ \mathtt{instruction\_size\_jmplen}\ j\ (\mathtt{nth}\ n\ prefix)
    117120\end{alignat*}
    118 
    119 This is a temporary formulation of the main property\\
    120 ({\tt sigma\_policy\_specification}); its main difference
     121\caption{Temporary safety property}
     122\label{sigmacompactunsafe}
     123\end{figure}
     124
     125We can now proceed with the lemmas that are needed for algorithm safety.
     126The lemma in Figure~\ref{sigmacompactunsafe} is a temporary formulation of
     127the main property\\ ({\tt sigma\_policy\_specification}). Its main difference
    121128from the final version is that it uses {\tt instruction\_size\_jmplen} to
    122129compute the instruction size. This function uses $j$ to compute the span
     
    127134property.
    128135
     136\begin{figure}[ht]
    129137\begin{alignat*}{6}
    130138\mathtt{sigma} & \omit\rlap{$\mathtt{\_safe} \equiv \lambda prefix.\lambda labels.\lambda old\_sigma.\lambda sigma$}\notag\\
     
    149157&&&&&\mathrm{long\_jump} \Rightarrow \mathrm{True}
    150158\end{alignat*}
    151 
    152 This is a more direct safety property: it states that branch instructions are
    153 encoded properly, and that no wrong branch instructions are chosen.
     159\caption{Safety property}
     160\label{sigmasafe}
     161\end{figure}
     162
     163The lemma in figure~\ref{sigmasafe} is a more direct safety property. It states
     164that branch instructions are encoded properly, and that no wrong branch
     165instructions are chosen.
    154166
    155167Note that we compute the distance using the memory address of the instruction
    156 plus its size: this follows the behaviour of the MCS-51 microprocessor, which
     168plus its size. This follows the behaviour of the MCS-51 microprocessor, which
    157169increases the program counter directly after fetching, and only then executes
    158170the branch instruction (by changing the program counter again).
     171
     172We now encode some final, simple, properties to make sure that our policy
     173remains consistent, and to keep track of whether the fixed point has been
     174reached.
    159175
    160176\begin{align*}
     
    198214The type of an iteration therefore becomes an option type: {\tt None} in case
    199215the program becomes larger than 64 Kb, or $\mathtt{Some}\ \sigma$
    200 otherwise. We also no longer use a natural number to pass along the number of
    201 bytes added to the program size, but a boolean that indicates whether we have
    202 changed something during the iteration or not.
     216otherwise. We also no longer pass along the number of bytes added to the
     217program size, but a boolean that indicates whether we have changed something
     218during the iteration or not.
    203219
    204220If an iteration returns {\tt None}, we have the following invariant:
     
    246262is only correct when we have reached the fixed point.
    247263
    248 There is another, trivial, invariant if the iteration returns
    249 $\mathtt{Some}\ \sigma$: $\mathtt{fst}\ sigma = 2^{16}$.
     264There is another, trivial, invariant in case the iteration returns
     265$\mathtt{Some}\ \sigma$: it must hold that $\mathtt{fst}\ sigma < 2^{16}$.
     266We need this invariant to make sure that addresses do not overflow.
    250267
    251268The invariants that are taken directly from the fold invariants are trivial to
    252269prove.
    253270
    254 The proof of {\tt nec\_plus\_ultra} works as follows: if we return {\tt None},
     271The proof of {\tt nec\_plus\_ultra} goes as follows: if we return {\tt None},
    255272then the program size must be greater than 64 Kb. However, since the
    256273previous iteration did not return {\tt None} (because otherwise we would
     
    288305longer jumps, in iteration $2n$ every branch instruction must be encoded as
    289306a long jump. In this case, iteration $2n$ is equal to iteration $2n+1$ and the
    290 fixpoint is reached.
     307fixed point is reached.
Note: See TracChangeset for help on using the changeset viewer.