Mar 12, 2012, 1:52:49 PM (9 years ago)

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

1 edited


  • 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.
    217217As mentioned, use of \texttt{Joint} also unifies semantics of these languages
    218 \end{itemize}
    219 \end{frame}
    221 \begin{frame}
     219We use several sets of records, which represent the state that a program is in
     221These records are parametric in representations for e.g. frames
    222226\frametitle{Semantics of \texttt{Joint} II}
     228record more_sem_params (p:params_): Type[1] :=
     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 }.
     243\frametitle{Semantics of \texttt{Joint} III}
     244Generic functions:
     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).
     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).
     262\frametitle{Semantics of \texttt{Joint} IV}
     263Individual semantics obtained by instantiating records to concrete types (ERTL here):
     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       ]).
     285\frametitle{Semantics of \texttt{Joint} V}
     286For languages with `extensions', we provide a semantics:
     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   ].
     307\frametitle{\texttt{Joint} summary}
     310Using \texttt{Joint} we get a modular semantics
     312`Common' semantics are shared amongst all languages
     314Specific languages are responsible for providing the semantics of the extensions that they provide
     316Show differences (and similarities) between languages clearly
     318Reduces proofs
     320Easy to add new languages
Note: See TracChangeset for help on using the changeset viewer.