Changeset 2350


Ignore:
Timestamp:
Sep 26, 2012, 5:53:31 PM (7 years ago)
Author:
mulligan
Message:

Got to the conclusions.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/cpp-asm-2012/cpp-2012-asm.tex

    r2349 r2350  
    530530    $\times$ (option address_entry).
    531531\end{lstlisting}
    532 [dpm update]
     532Here, \texttt{upper\_lower} is a type isomorphic to the booleans denoting whether a byte value is the upper or lower byte of some 16-bit address.
     533
    533534The implementation of \texttt{internal\_pseudo\_address\_map} is complicated by some peculiarities of the MCS-51's instruction set.
    534535Note here that all addresses are 16 bit words, but are stored (and manipulated) as 8 bit bytes.
    535536All \texttt{MOV} instructions in the MCS-51 must use the accumulator \texttt{A} as an intermediary, moving a byte at a time.
    536 The second component of \texttt{internal\_pseudo\_address\_map} therefore states whether the accumulator currently holds a piece of an address, and if so, whether it is the upper or lower byte of the address (using the boolean flag) complete with the corresponding source address in full.
    537 The first component, on the other hand, performs a similar task for the rest of external RAM.
    538 Again, we use a boolean flag to describe whether a byte is the upper or lower component of a 16-bit address.
     537The third component of \texttt{internal\_pseudo\_address\_map} therefore states whether the accumulator currently holds a piece of an address, and if so, whether it is the upper or lower byte of the address (using the \texttt{upper\_lower} flag) complete with the corresponding source address in full.
     538The first and second components, on the other hand, performs a similar task for the higher and lower external RAM.
     539Again, we use our \texttt{upper\_lower} flag to describe whether a byte is the upper or lower component of a 16-bit address.
    539540
    540541The \texttt{low\_internal\_ram\_of\_pseudo\_low\_internal\_ram} function converts the lower internal RAM of a \texttt{PseudoStatus} into the lower internal RAM of a \texttt{Status}.
    541542A similar function exists for high internal RAM.
    542 Note that both RAM segments are indexed using addresses 7-bits long.
    543 The function is currently axiomatised, and an associated set of axioms prescribe the behaviour of the function:
     543Note that both RAM segments are indexed using addresses 7-bits long:
    544544\begin{lstlisting}
    545545definition low_internal_ram_of_pseudo_low_internal_ram:
     
    565565   program_counter s < $2^{16}$ $\rightarrow$ option internal_pseudo_address_map
    566566\end{lstlisting}
    567 [dpm change]
    568 Note, if we wished to allow `benign manipulations' of addresses, it would be this function that needs to be changed.
     567If we wished to allow `benign manipulations' of addresses, it would be this function that needs to be changed.
     568Note we once again use dependent types to ensure that program counters are properly within bounds.
     569The third argument is a function that resolves the concrete address of a label.
    569570
    570571The function \texttt{ticks\_of0} computes how long---in clock cycles---a pseudoinstruction will take to execute when expanded in accordance with a given policy.
     
    595596       (ticks_of program ($\lambda$id. addr_of id ps) policy) ps) policy.
    596597\end{lstlisting}
    597 [dpm change]
    598598The statement is standard for forward simulation, but restricted to \texttt{PseudoStatuses} \texttt{ps} whose next instruction to be executed is well-behaved with respect to the \texttt{internal\_pseudo\_address\_map} \texttt{M}.
    599 Further, we explicitly require proof that our policy is correct and the pseudo-program counter lies within the bounds of the program.
     599Further, we explicitly require proof that our policy is correct, our program is well-labelled (i.e. no repeated labels, and so on) and the pseudo-program counter lies within the bounds of the program.
    600600Theorem \texttt{main\_thm} establishes the total correctness of the assembly process and can simply be lifted to the forward simulation of an arbitrary number of well behaved steps on the assembly program.
    601601
Note: See TracChangeset for help on using the changeset viewer.