Changeset 1016
- Timestamp:
- Jun 21, 2011, 10:20:20 AM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/CPP2011/cpp-2011.tex
r1013 r1016 292 292 | long_jump: jump_length. 293 293 \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. 294 A \texttt{jump\_expansion\_policy} is a map from pseudo program counters (implemented as \texttt{Word}s) to \texttt{jump\_length}s. Efficient implementations 295 of policies are based on tries. 295 296 Intuitively, a policy maps positions in a program (indexed using program counters implemented as \texttt{Word}s) to a particular variety of jump. 296 297 \begin{lstlisting} 297 definition jump_expansion_policy := BitVectorTrie jump_length 16.298 definition policy_type ≝ Word → jump_length. 298 299 \end{lstlisting} 299 300 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: 303 304 \begin{lstlisting} 304 definition sigma0: pseudo_assembly_program 305 definition sigma0: pseudo_assembly_program $\rightarrow$ policy_type 305 306 $\rightarrow$ option (nat $\times$ (nat $\times$ (BitVectorTrie Word 16))) := $\ldots$ 306 307 \end{lstlisting} … … 311 312 \begin{lstlisting} 312 313 definition 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} 316 Now, it's possible to define what a `good policy' is for a program \texttt{p}. 317 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 318 short/middle jumps to too far locations or when the prouced object code does 319 not fit in code memory. A \texttt{policy} for a program \texttt{p} 320 is a policy that is good for \texttt{p}. 321 \begin{lstlisting} 322 definition policy_ok := $\lambda$pol.$\lambda$p. sigma_safe p $\neq$ None $\ldots$. 323 definition policy ≝ λp. $\Sigma$jump_expansion:policy_type. policy_ok jump_expansion p. 324 \end{lstlisting} 325 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 326 we avoid failure here and in most of the remaining functions by restricting 327 the domain using the dependent type \texttt{policy}. 323 328 \begin{lstlisting} 324 329 definition sigma: $\forall$p. policy p $\rightarrow$ Word $\rightarrow$ Word := $\ldots$
Note: See TracChangeset
for help on using the changeset viewer.