Ignore:
Timestamp:
Jun 15, 2012, 11:36:47 AM (8 years ago)
Author:
boender
Message:
  • rewrote introduction
  • changed 'medium' to 'absolute'
  • added a bit to conclusion (CompCert?, Piton, ...)
File:
1 edited

Legend:

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

    r2084 r2085  
    55
    66The main correctness statement is as follows:
     7
     8\clearpage
    79
    810\begin{lstlisting}
     
    5557$2n$ the number of jumps in the program. This worst case is reached if at every
    5658iteration, we change the encoding of exactly one jump; since a jump can change
    57 from {\tt short} to {\tt medium} and from {\tt medium} to {\tt long}, there
    58 can be at most $2n$ changes.
     59from short to absolute and from absolute to long, there can be at most $2n$
     60changes.
    5961
    6062This proof has been executed in the ``Russell'' style from~\cite{Sozeau2006}.
     
    114116iteration, and $p$ the current one), jump lengths either remain equal or
    115117increase. It is needed for proving termination.
     118
     119\clearpage
    116120
    117121\begin{lstlisting}
     
    160164    [ short_jump $\Rightarrow$ $\neg$is_call instr $\wedge$
    161165       \fst (short_jump_cond pc_plus_jmp_length addr) = true
    162     | medium_jump $\Rightarrow$ $\neg$is_relative_jump instr $\wedge$
    163        \fst (medium_jump_cond pc_plus_jmp_length addr) = true $\wedge$
     166    | absolute_jump $\Rightarrow$ $\neg$is_relative_jump instr $\wedge$
     167       \fst (absolute_jump_cond pc_plus_jmp_length addr) = true $\wedge$
    164168       \fst (short_jump_cond pc_plus_jmp_length addr) = false
    165169    | long_jump $\Rightarrow$ \fst (short_jump_cond pc_plus_jmp_length addr) = false
    166        $\wedge$ \fst (medium_jump_cond pc_plus_jmp_length addr) = false
     170       $\wedge$ \fst (absolute_jump_cond pc_plus_jmp_length addr) = false
    167171    ].
    168172\end{lstlisting}
     
    200204We need to use two different formulations, because the fact that $added$ is 0
    201205does not guarantee that no jumps have changed: it is possible that we have
    202 replaced a short jump with a medium jump, which does not change the size.
     206replaced a short jump with a absolute jump, which does not change the size.
    203207
    204208Therefore {\tt policy\_pc\_equal} states that $old\_sigma_1(x) = sigma_1(x)$,
     
    245249
    246250\begin{lstlisting}
    247 definition sigma_compact: list labelled_instruction → label_map → ppc_pc_map → Prop :=
    248  λprogram.λlabels.λsigma.
     251definition sigma_compact :=
     252 λprogram:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map.
    249253 ∀n.n < |program| →
    250254  match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? n) (\snd sigma) with
Note: See TracChangeset for help on using the changeset viewer.