Changeset 1816 for Deliverables


Ignore:
Timestamp:
Mar 12, 2012, 1:52:49 PM (8 years ago)
Author:
mulligan
Message:

more slides added, only got topic of changes merged back into o'caml compiler left to discuss

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D1.1/Presentations/Paris presentation March 2012/WP4-dominic.tex

    r1815 r1816  
    143143 | COST_LABEL: costlabel $\rightarrow$ joint_instruction p globals
    144144 ...
    145  | COND: acc_a_reg p label $\rightarrow$ joint_instruction p globals
     145 | COND: acc_a_reg p $\rightarrow$ label $\rightarrow$ joint_instruction p globals
    146146 | extension: extend_statements p $\rightarrow$ joint_instruction p globals.
    147147\end{lstlisting}
     
    216216\item
    217217As mentioned, use of \texttt{Joint} also unifies semantics of these languages
    218 \end{itemize}
    219 \end{frame}
    220 
    221 \begin{frame}
     218\item
     219We use several sets of records, which represent the state that a program is in
     220\item
     221These records are parametric in representations for e.g. frames
     222\end{itemize}
     223\end{frame}
     224
     225\begin{frame}[fragile]
    222226\frametitle{Semantics of \texttt{Joint} II}
     227\begin{lstlisting}
     228record more_sem_params (p:params_): Type[1] :=
     229{
     230  framesT: Type[0];
     231  empty_framesT: framesT;
     232  regsT: Type[0];
     233  ...
     234  acca_store_: acc_a_reg p → beval → regsT → res regsT;
     235  acca_retrieve_: regsT → acc_a_reg p → res beval;
     236  ...
     237  pair_reg_move_: regsT → pair_reg p → res regsT
     238 }.
     239\end{lstlisting}
     240\end{frame}
     241
     242\begin{frame}[fragile]
     243\frametitle{Semantics of \texttt{Joint} III}
     244Generic functions:
     245\begin{lstlisting}
     246definition set_carry: $\forall$p. beval $\rightarrow$ state p $\rightarrow$ state p :=
     247 $\lambda$p, carry, st.
     248  mk_state $\ldots$ (st_frms $\ldots$ st) (pc $\ldots$ st)
     249   (sp $\ldots$ st) (isp $\ldots$ st) carry (regs $\ldots$ st) (m $\ldots$ st).
     250\end{lstlisting}
     251\begin{lstlisting}
     252definition goto: $\forall$globals. $\forall$p:sem_params1 globals. genv globals p $\rightarrow$
     253  label $\rightarrow$ state p $\rightarrow$ res (state p) :=
     254 $\lambda$globals, p, ge, l, st.
     255  do oldpc $\leftarrow$ pointer_of_address (pc $\ldots$ st) ;
     256  do newpc $\leftarrow$ address_of_label $\ldots$ ge oldpc l ;
     257  OK $\ldots$ (set_pc $\ldots$ newpc st).
     258\end{lstlisting}
     259\end{frame}
     260
     261\begin{frame}[fragile]
     262\frametitle{Semantics of \texttt{Joint} IV}
     263Individual semantics obtained by instantiating records to concrete types (ERTL here):
     264\begin{lstlisting}
     265definition ertl_more_sem_params: more_sem_params ertl_params_ :=
     266 mk_more_sem_params ertl_params_
     267  (list (register_env beval)) [] ((register_env beval) $\times$ hw_register_env)
     268   ($\lambda$sp. $\langle$empty_map $\ldots$,init_hw_register_env sp$\rangle$) 0 it
     269   ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve ps_reg_store
     270    ps_reg_retrieve ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
     271     ($\lambda$locals,dest_src.
     272       do v $\leftarrow$
     273        match \snd dest_src with
     274        [ pseudo reg $\Rightarrow$ ps_reg_retrieve locals reg
     275        | hardware reg $\Rightarrow$ hw_reg_retrieve locals reg
     276        ];
     277       match \fst dest_src with
     278       [ pseudo reg $\Rightarrow$ ps_reg_store reg v locals
     279       | hardware reg $\Rightarrow$ hw_reg_store reg v locals
     280       ]).
     281\end{lstlisting}
     282\end{frame}
     283
     284\begin{frame}[fragile]
     285\frametitle{Semantics of \texttt{Joint} V}
     286For languages with `extensions', we provide a semantics:
     287\begin{lstlisting}
     288definition ertl_exec_extended:
     289 $\forall$globals. genv globals (ertl_params globals) $\rightarrow$
     290  ertl_statement_extension $\rightarrow$ label $\rightarrow$ state ertl_sem_params $\rightarrow$
     291   IO io_out io_in (trace $\times$ (state ertl_sem_params)) :=
     292 $\lambda$globals, ge, stm, l, st.
     293  match stm with
     294   [ ertl_st_ext_new_frame $\Rightarrow$
     295      ! v $\leftarrow$ framesize globals $\ldots$ ge st;
     296      let sp := get_hwsp st in
     297      ! newsp $\leftarrow$ addr_sub sp v;
     298      let st := set_hwsp newsp st in
     299      ! st $\leftarrow$ next $\ldots$ (ertl_sem_params1 globals) l st ;
     300        ret ? $\langle$E0, st$\rangle$
     301   | ...
     302   ].
     303\end{lstlisting}
     304\end{frame}
     305
     306\begin{frame}
     307\frametitle{\texttt{Joint} summary}
     308\begin{itemize}
     309\item
     310Using \texttt{Joint} we get a modular semantics
     311\item
     312`Common' semantics are shared amongst all languages
     313\item
     314Specific languages are responsible for providing the semantics of the extensions that they provide
     315\item
     316Show differences (and similarities) between languages clearly
     317\item
     318Reduces proofs
     319\item
     320Easy to add new languages
     321\end{itemize}
    223322\end{frame}
    224323
Note: See TracChangeset for help on using the changeset viewer.