Changeset 1016

Timestamp:

Jun 21, 2011, 10:20:20 AM (10 years ago)

Author:

sacerdot

Message:

Many fixes to the code snippets.

File:

• src/ASM/CPP2011/cpp-2011.tex (modified) (3 diffs)

src/ASM/CPP2011/cpp-2011.tex

@@ -292 +292 @@
   | long_jump: jump_length.
 \end{lstlisting}
-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.
+A \texttt{jump\_expansion\_policy} is a map from pseudo program counters (implemented as \texttt{Word}s) to \texttt{jump\_length}s. Efficient implementations
+of policies are based on tries.
 Intuitively, a policy maps positions in a program (indexed using program counters implemented as \texttt{Word}s) to a particular variety of jump.
 \begin{lstlisting}
-definition jump_expansion_policy := BitVectorTrie jump_length 16.
+definition policy_type ≝ Word → jump_length.
 \end{lstlisting}
 Next, we require a series of `sigma' functions.
@@ -302 +303 @@
 This 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:
 \begin{lstlisting}
-definition sigma0: pseudo_assembly_program
+definition sigma0: pseudo_assembly_program $\rightarrow$ policy_type
   $\rightarrow$ option (nat $\times$ (nat $\times$ (BitVectorTrie Word 16))) := $\ldots$
 \end{lstlisting}
@@ -311 +312 @@
 \begin{lstlisting}
 definition sigma_safe:
-  pseudo_assembly_program $\rightarrow$ option (Word $\rightarrow$ Word) := $\ldots$
-\end{lstlisting}
-Now, it's possible to define what a `good policy' is.
-A policy is deemed good when it prevents \texttt{sigma\_safe} from ever failing.
-As mentioned, \texttt{sigma\_safe} can only fail if an assembly program fails to be assembled:
-\begin{lstlisting}
-definition policy_ok := $\lambda$p. sigma_safe p $\neq$ None $\ldots$.
-\end{lstlisting}
-Finally, we obtain \texttt{sigma}, a mapping from pseudo program counters to program counters which incorporates, depending also on a policy.
-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:
+  pseudo_assembly_program $\rightarrow$ policy_type $\rightarrow$ option (Word $\rightarrow$ Word) := $\ldots$
+\end{lstlisting}
+Now, it's possible to define what a `good policy' is for a program \texttt{p}.
+A 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
+short/middle jumps to too far locations or when the prouced object code does
+not fit in code memory. A \texttt{policy} for a program \texttt{p}
+is a policy that is good for \texttt{p}.
+\begin{lstlisting}
+definition policy_ok := $\lambda$pol.$\lambda$p. sigma_safe p $\neq$ None $\ldots$.
+definition policy ≝ λp. $\Sigma$jump_expansion:policy_type. policy_ok jump_expansion p.
+\end{lstlisting}
+Finally, 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
+we avoid failure here and in most of the remaining functions by restricting
+the domain using the dependent type \texttt{policy}.
 \begin{lstlisting}
 definition sigma: $\forall$p. policy p $\rightarrow$ Word $\rightarrow$ Word := $\ldots$