Changeset 1743


Ignore:
Timestamp:
Feb 24, 2012, 3:45:54 PM (8 years ago)
Author:
mulligan
Message:

diagrams finished, adding text

File:
1 edited

Legend:

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

    r1742 r1743  
    317317\begin{center}
    318318\begin{picture}(2, 2)
    319 \put(0,-20){\framebox(25,25)[c]{\texttt{v}}}
    320 \put(26,-20){\framebox(25,25)[c]{\texttt{4}}}
    321 \put(51,-20){\framebox(25,25)[c]{\texttt{cont}}}
    322 \put(76,-20){\framebox(25,25)[c]{\texttt{cont}}}
    323 \put(101,-20){\framebox(25,25)[c]{\texttt{cont}}}
     319\put(-150,-20){\framebox(25,25)[c]{\texttt{v}}}
     320\put(-125,-20){\framebox(25,25)[c]{\texttt{4}}}
     321\put(-100,-20){\framebox(25,25)[c]{\texttt{cont}}}
     322\put(-75,-20){\framebox(25,25)[c]{\texttt{cont}}}
     323\put(-50,-20){\framebox(25,25)[c]{\texttt{cont}}}
     324\put(-15,-10){\vector(1, 0){30}}
     325\put(25,-20){\framebox(25,25)[c]{\texttt{\texttt{v1}}}}
     326\put(50,-20){\framebox(25,25)[c]{\texttt{\texttt{v2}}}}
     327\put(75,-20){\framebox(25,25)[c]{\texttt{\texttt{v3}}}}
     328\put(100,-20){\framebox(25,25)[c]{\texttt{\texttt{v4}}}}
    324329\end{picture}
    325330\end{center}
     
    331336\begin{displaymath}
    332337\sigma(\mathtt{store}\ v\ M) = \mathtt{store}\ \sigma(v)\ \sigma(M)
     338\end{displaymath}
     339
     340\begin{displaymath}
     341\texttt{load}^* (\mathtt{store}\ \sigma(v)\ \sigma(M))\ \sigma(a)\ \sigma(M) = \mathtt{load}^*\ \sigma(s)\ \sigma(a)\ \sigma(M)
    333342\end{displaymath}
    334343
     
    382391
    383392\begin{displaymath}
    384 \begin{diagram}
    385 \mathtt{CALL}(\mathtt{id},\ \mathtt{args},\ \mathtt{dst},\ \mathtt{pc}),\ \mathtt{State}(\mathtt{Frame},\ \mathtt{Frames}) & \rTo & \mathtt{Call}(FINISH ME)
    386 \end{diagram}
    387 \end{displaymath}
     393\begin{array}{rcl}
     394\mathtt{Call(id,\ args,\ dst,\ pc),\ State(FRAME, FRAMES)} & \longrightarrow & \mathtt{Call(M(args), dst)}, \\
     395                                                           &                 & \mathtt{PUSH(current\_frame[PC := after\_return])}
     396\end{array}
     397\end{displaymath}
     398
     399In the case where the call is to an external function, we have:
     400
     401\begin{displaymath}
     402\begin{array}{rcl}
     403\mathtt{Call(M(args), dst)},                       & \stackrel{\mathtt{ret\_val = f(M(args))}}{\longrightarrow} & \mathtt{Return(ret\_val,\ dst,\ PUSH(...))} \\
     404\mathtt{PUSH(current\_frame[PC := after\_return])} &                                                            &
     405\end{array}
     406\end{displaymath}
     407
     408then:
     409
     410\begin{displaymath}
     411\begin{array}{rcl}
     412\mathtt{Return(ret\_val,\ dst,\ PUSH(...))} & \longrightarrow & \mathtt{pc = POP\_STACK(regs[dst := M(ret\_val)],\ pc)}
     413\end{array}
     414\end{displaymath}
     415
     416In the case where the call is to an internal function, we have:
    388417
    389418\begin{displaymath}
     
    396425\begin{displaymath}
    397426\begin{array}{rcl}
     427\mathtt{Call(M(args), dst)}                        & \longrightarrow & \mathtt{sp = alloc}, regs = \emptyset[- := PARAMS] \\
     428\mathtt{PUSH(current\_frame[PC := after\_return])} &                 & \mathtt{State}(regs,\ sp,\ pc_\emptyset,\ dst)
     429\end{array}
     430\end{displaymath}
     431
     432then:
     433
     434\begin{displaymath}
     435\begin{array}{rcl}
     436\mathtt{sp = alloc}, regs = \emptyset[- := PARAMS] & \longrightarrow & \mathtt{free(sp)} \\
     437\mathtt{State}(regs,\ sp,\ pc_\emptyset,\ dst)     &                 & \mathtt{Return(M(ret\_val), dst, frames)}
     438\end{array}
     439\end{displaymath}
     440
     441and finally:
     442
     443\begin{displaymath}
     444\begin{array}{rcl}
     445\mathtt{free(sp)}                         & \longrightarrow & \mathtt{pc = POP\_STACK(regs[dst := M(ret\_val)],\ pc)} \\
     446\mathtt{Return(M(ret\_val), dst, frames)} &                 &
     447\end{array}
     448\end{displaymath}
     449
     450\begin{displaymath}
     451\begin{array}{rcl}
    398452\sigma & : & \mathtt{register} \rightarrow \mathtt{list\ register} \\
    399453\sigma' & : & \mathtt{list\ register} \rightarrow \mathtt{list\ register}
    400 \end{array} 
     454\end{array}
    401455\end{displaymath}
    402456
Note: See TracChangeset for help on using the changeset viewer.