Changeset 1792 for Deliverables


Ignore:
Timestamp:
Feb 28, 2012, 5:56:20 PM (8 years ago)
Author:
mulligan
Message:

...

File:
1 edited

Legend:

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

    r1791 r1792  
    522522\begin{displaymath}
    523523\begin{array}{rll}
    524 \mathtt{State} & ::=  & (\mathtt{State} : \mathtt{Frame}^* \times \mathtt{Frame} \\
     524\mathtt{StateRTLabs} & ::=  & (\mathtt{State} : \mathtt{Frame}^* \times \mathtt{Frame} \\
    525525               & \mid & \mathtt{Call} : \mathtt{Frame}^* \times \mathtt{Args} \times \mathtt{Return} \times \mathtt{Fun} \\
    526526               & \mid & \mathtt{Return} : \mathtt{Frame}^* \times \mathtt{Value} \times \mathtt{Return}) \times \mathtt{Mem}
     
    536536
    537537\begin{displaymath}
    538 \mathtt{State} ::= \mathtt{Frame}^* \times \mathtt{PC} \times \mathtt{SP} \times \mathtt{ISP} \times \mathtt{CARRY} \times \mathtt{REGS}
     538\mathtt{StateRTL} ::= (\mathtt{Frame}^* \times \mathtt{PC} \times \mathtt{SP} \times \mathtt{ISP} \times \mathtt{CARRY} \times \mathtt{REGS}) \times \mathtt{Mem}
    539539\end{displaymath}
    540540The internal stack pointer \texttt{ISP}, and its relationship with the stack pointer \texttt{SP}, needs some comment.
     
    550550Because $\sigma$ is one-to-many and, morally, a multivalued function, we use in the sequel the functional notation for $\sigma$, using $\star$ as a distinct marker in the range of $\sigma$ to mean that any value is accepted.
    551551\begin{displaymath}
    552 \mathtt{State} \stackrel{\sigma}{\longrightarrow} \mathtt{State}
     552\mathtt{StateRTLabs} \stackrel{\sigma}{\longrightarrow} \mathtt{StateRTL}s
    553553\end{displaymath}
    554554
     
    607607\begin{displaymath}
    608608\begin{array}{rcl}
    609 \mathtt{CALL(id,\ args,\ dst,\ pc) \in State(Frame^*, Frame)} & \longrightarrow & \mathtt{Call(M(args), dst)}, \\
    610                                                            &                 & \mathtt{PUSH(Frame[pc := after\_return])}
     609\mathtt{CALL(id,\ args,\ dst,\ pc) \in State(Frame^*, Frame)} & \longrightarrow & \mathtt{PUSH(Frame[pc := after\_return])}, \\
     610                                                           &                 &  \mathtt{Call(M(args), dst)}
    611611\end{array}
    612612\end{displaymath}
     
    619619\begin{displaymath}
    620620\begin{array}{rcl}
    621 \mathtt{Call(M(args), dst)},                       & \stackrel{\mathtt{ret\_val = f(M(args))}}{\longrightarrow} & \mathtt{Return(ret\_val,\ dst,\ PUSH(...))} \\
    622 \mathtt{PUSH(Frame[pc := after\_return])} &                                                            &
     621\mathtt{PUSH(Frame[pc := after\_return])},  & \stackrel{\mathtt{ret\_val = f(M(args))}}{\longrightarrow} & \mathtt{Return(ret\_val,\ dst,\ PUSH(...))} \\
     622\mathtt{Call(M(args), dst)}                &                                                            &
    623623\end{array}
    624624\end{displaymath}
     
    705705Note, in particular, that this final act of pushing a frame on the stack leaves us in an identical state to the RTLabs case, where the instruction
    706706\begin{displaymath}
    707 \mathtt{PUSH(current\_frame[pc := after\_return])}
     707\mathtt{PUSH(Frame[pc := after\_return])}
    708708\end{displaymath}
    709709was executed.
Note: See TracChangeset for help on using the changeset viewer.