Changeset 1763


Ignore:
Timestamp:
Feb 27, 2012, 1:52:30 PM (8 years ago)
Author:
mulligan
Message:

to avoid conflicts

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D1.2/CompilerProofOutline/outline.tex

    r1762 r1763  
    408408This will entail more proof obligations, demonstrating that the $\sigma$-map between memory spaces respects memory regions.
    409409
     410RTLabs states come in three flavours:
    410411\begin{displaymath}
    411412\begin{array}{rll}
     
    415416\end{array}
    416417\end{displaymath}
    417 
     418\texttt{State} is the default state in which RTLabs programs are almost always in.
     419The \texttt{Call} state is only entered when a call instruction is being executed, and then we immediately return to being in \texttt{State}.
     420Similarly, \texttt{Return} is only entered when a return instruction is being executed, before returning immediately to \texttt{State}.
     421All RTLabs states are accompanied by a memory, \texttt{Mem}, with \texttt{Call} and \texttt{Return} keeping track of arguments, return addresses and the results of functions.
     422\texttt{State} keeps track of a list of stack frames.
     423
     424RTL states differ from their RTLabs counterparts, in including a program counter \texttt{PC}, stack-pointer \texttt{SP}, internal stack pointer \texttt{ISP}, a carry flag \texttt{CARRY} and a set of registers \texttt{REGS}:
    418425\begin{displaymath}
    419426\mathtt{State} ::= \mathtt{Frame}^* \times \mathtt{PC} \times \mathtt{SP} \times \mathtt{ISP} \times \mathtt{CARRY} \times \mathtt{REGS}
    420427\end{displaymath}
    421 
     428The internal stack pointer \texttt{ISP}, and its relationship with the stack pointer \texttt{SP}, needs some comment.
     429Due to the design of the MCS-51, and its minuscule stack, it was decided that the compiler would implement an emulated stack in external memory.
     430As a result, we have two stack pointers in our state: \texttt{ISP}, which is the real, hardware stack, and \texttt{SP}, which is the stack pointer of the emulated stack in memory.
     431The emulated stack is used for pushing and popping stack frames when calling or returning from function calls, however this is done using the hardware stack, indexed by \texttt{ISP} as an intermediary.
     432Instructions like \texttt{LCALL} and \texttt{ACALL} are hardwired by the processor's design to push on to the hardware stack, therefore after a call has been made, and after a call returns, the compiler emits code to move parameters and return addresses to-and-from the hardware stack.
     433As a result, for most of the execution of the processor, the hardware stack is empty, or contains a single item ready to be moved into external memory.
     434
     435Once more, we require a map from RTLabs states to RTL states.
     436Call it $\sigma$:
    422437\begin{displaymath}
    423438\mathtt{State} \stackrel{\sigma}{\longrightarrow} \mathtt{State}
    424439\end{displaymath}
    425440
    426 \begin{displaymath}
    427 \sigma(\mathtt{State} (\mathtt{Frame}^* \times \mathtt{Frame})) \longrightarrow ((\sigma(\mathtt{Frame}^*), \sigma(\mathtt{PC}), \sigma(\mathtt{SP}), 0, 0, \sigma(\mathtt{REGS})), \sigma(\mathtt{Mem}))
    428 \end{displaymath}
    429 
     441Translating an RTLabs state to an RTL state proceeds by cases on the particular type of state we are trying to translate, either a \texttt{State}, \texttt{Call} or a \texttt{Return}.
     442For \texttt{State} we perform a further case analysis of the top stack frame, which decomposes into a tuple holding the current program counter value, the current stack pointer and the value of the registers:
     443\begin{displaymath}
     444\sigma(\mathtt{State} (\mathtt{Frame}^* \times \mathtt{\langle PC, REGS, SP \rangle})) \longrightarrow ((\sigma(\mathtt{Frame}^*), \sigma(\mathtt{PC}), \sigma(\mathtt{SP}), 0, 0, \sigma(\mathtt{REGS})), \sigma(\mathtt{Mem}))
     445\end{displaymath}
     446Translation then proceeds by translating the remaining stack frames, as well as the contents of the top stack frame, and setting all untranslated values to zero, their default value.
     447
     448Translating \texttt{Call} and \texttt{Return} states is more involved, as a commutation between a single step of execution and the translation process must hold:
    430449\begin{displaymath}
    431450\sigma(\mathtt{Return}(-)) \longrightarrow \sigma \circ \text{return one step}
     
    436455\end{displaymath}
    437456
    438 Return one step commuting diagram:
    439 
     457Here \emph{return one step} and \emph{call one step} refer to a pair of commuting diagrams relating the one-step execution of a call and return state and translation of both.
     458We provide the one step commuting diagrams in Figure~\ref{fig.commuting.diagrams}.
     459
     460\begin{figure}
    440461\begin{displaymath}
    441462\begin{diagram}
     
    446467\end{displaymath}
    447468
    448 Call one step commuting diagram:
    449 
    450469\begin{displaymath}
    451470\begin{diagram}
     
    455474\end{diagram}
    456475\end{displaymath}
    457 
     476\caption{The one-step commuting diagrams for \texttt{Call} and \texttt{Return} state translations}
     477\label{fig.commuting.diagrams}
     478\end{figure}
     479
     480We outline how states are executed:
    458481\begin{displaymath}
    459482\begin{array}{rcl}
    460 \mathtt{Call(id,\ args,\ dst,\ pc),\ State(FRAME, FRAMES)} & \longrightarrow & \mathtt{Call(M(args), dst)}, \\
    461                                                            &                 & \mathtt{PUSH(current\_frame[PC := after\_return])}
     483\mathtt{Call(id,\ args,\ dst,\ pc),\ State(Frame^*, Frame)} & \longrightarrow & \mathtt{Call(M(args), dst)}, \\
     484                                                           &                 & \mathtt{PUSH(Frame[PC := after\_return])}
    462485\end{array}
    463486\end{displaymath}
    464 
     487Suppose we are given a \texttt{State} with a list of stack frames, with the top frame being \texttt{Frame}.
     488Suppose also that the program counter in \texttt{Frame} points to a \texttt{Call} instruction, complete with arguments and destination address.
     489Then this is executed by entering into a \texttt{Call} state were the arguments are looked up in memory, and the destination address is filled in, with the current stack frame being pushed on top of the stack with the return address substituted for the program counter.
     490
     491Now, what happens next depends on whether we are executing an internal or an external function.
    465492In the case where the call is to an external function, we have:
    466 
    467493\begin{displaymath}
    468494\begin{array}{rcl}
     
    472498\end{displaymath}
    473499
     500
    474501then:
    475502
     
    511538\mathtt{free(sp)}                         & \longrightarrow & \mathtt{pc = POP\_STACK(regs[dst := M(ret\_val)],\ pc)} \\
    512539\mathtt{Return(M(ret\_val), dst, frames)} &                 &
    513 \end{array}
    514 \end{displaymath}
    515 
    516 \begin{displaymath}
    517 \begin{array}{rcl}
    518 \sigma & : & \mathtt{register} \rightarrow \mathtt{list\ register} \\
    519 \sigma' & : & \mathtt{list\ register} \rightarrow \mathtt{list\ register}
    520540\end{array}
    521541\end{displaymath}
Note: See TracChangeset for help on using the changeset viewer.