Changeset 1016 for src/ASM/CPP2011


Ignore:
Timestamp:
Jun 21, 2011, 10:20:20 AM (8 years ago)
Author:
sacerdot
Message:

Many fixes to the code snippets.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2011/cpp-2011.tex

    r1013 r1016  
    292292  | long_jump: jump_length.
    293293\end{lstlisting}
    294 A \texttt{jump\_expansion\_policy} is a map from pseudo program counters (implemented as \texttt{Word}s) to \texttt{jump\_length}s, implemented as a trie.
     294A \texttt{jump\_expansion\_policy} is a map from pseudo program counters (implemented as \texttt{Word}s) to \texttt{jump\_length}s. Efficient implementations
     295of policies are based on tries.
    295296Intuitively, a policy maps positions in a program (indexed using program counters implemented as \texttt{Word}s) to a particular variety of jump.
    296297\begin{lstlisting}
    297 definition jump_expansion_policy := BitVectorTrie jump_length 16.
     298definition policy_type ≝ Word → jump_length.
    298299\end{lstlisting}
    299300Next, we require a series of `sigma' functions.
     
    302303This function fails if and only if an internal call to \texttt{assembly\_1\_pseudoinstruction\_safe} fails, which happens if a jump pseudoinstruction is expanded incorrectly:
    303304\begin{lstlisting}
    304 definition sigma0: pseudo_assembly_program
     305definition sigma0: pseudo_assembly_program $\rightarrow$ policy_type
    305306  $\rightarrow$ option (nat $\times$ (nat $\times$ (BitVectorTrie Word 16))) := $\ldots$
    306307\end{lstlisting}
     
    311312\begin{lstlisting}
    312313definition sigma_safe:
    313   pseudo_assembly_program $\rightarrow$ option (Word $\rightarrow$ Word) := $\ldots$
    314 \end{lstlisting}
    315 Now, it's possible to define what a `good policy' is.
    316 A policy is deemed good when it prevents \texttt{sigma\_safe} from ever failing.
    317 As mentioned, \texttt{sigma\_safe} can only fail if an assembly program fails to be assembled:
    318 \begin{lstlisting}
    319 definition policy_ok := $\lambda$p. sigma_safe p $\neq$ None $\ldots$.
    320 \end{lstlisting}
    321 Finally, we obtain \texttt{sigma}, a mapping from pseudo program counters to program counters which incorporates, depending also on a policy.
    322 This is a thin shell around \texttt{sigma\_safe}, and dispenses with the option type via a proof that \texttt{sigma\_safe} never fails under the assumption that a supplied policy is correct:
     314  pseudo_assembly_program $\rightarrow$ policy_type $\rightarrow$ option (Word $\rightarrow$ Word) := $\ldots$
     315\end{lstlisting}
     316Now, it's possible to define what a `good policy' is for a program \texttt{p}.
     317A policy \texttt{pol} is deemed good when it prevents \texttt{sigma\_safe} from failing on \texttt{p}. Failure is only possible when the policy prescribes
     318short/middle jumps to too far locations or when the prouced object code does
     319not fit in code memory. A \texttt{policy} for a program \texttt{p}
     320is a policy that is good for \texttt{p}.
     321\begin{lstlisting}
     322definition policy_ok := $\lambda$pol.$\lambda$p. sigma_safe p $\neq$ None $\ldots$.
     323definition policy ≝ λp. $\Sigma$jump_expansion:policy_type. policy_ok jump_expansion p.
     324\end{lstlisting}
     325Finally, we obtain \texttt{sigma}, a mapping from pseudo program counters to program counters that takes in input a good policy and thus never fails. Note how
     326we avoid failure here and in most of the remaining functions by restricting
     327the domain using the dependent type \texttt{policy}.
    323328\begin{lstlisting}
    324329definition sigma: $\forall$p. policy p $\rightarrow$ Word $\rightarrow$ Word := $\ldots$
Note: See TracChangeset for help on using the changeset viewer.