Changeset 1816
 Timestamp:
 Mar 12, 2012, 1:52:49 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D1.1/Presentations/Paris presentation March 2012/WP4dominic.tex
r1815 r1816 143 143  COST_LABEL: costlabel $\rightarrow$ joint_instruction p globals 144 144 ... 145  COND: acc_a_reg p →label $\rightarrow$ joint_instruction p globals145  COND: acc_a_reg p $\rightarrow$ label $\rightarrow$ joint_instruction p globals 146 146  extension: extend_statements p $\rightarrow$ joint_instruction p globals. 147 147 \end{lstlisting} … … 216 216 \item 217 217 As mentioned, use of \texttt{Joint} also unifies semantics of these languages 218 \end{itemize} 219 \end{frame} 220 221 \begin{frame} 218 \item 219 We use several sets of records, which represent the state that a program is in 220 \item 221 These records are parametric in representations for e.g. frames 222 \end{itemize} 223 \end{frame} 224 225 \begin{frame}[fragile] 222 226 \frametitle{Semantics of \texttt{Joint} II} 227 \begin{lstlisting} 228 record 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} 244 Generic functions: 245 \begin{lstlisting} 246 definition 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} 252 definition 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} 263 Individual semantics obtained by instantiating records to concrete types (ERTL here): 264 \begin{lstlisting} 265 definition 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} 286 For languages with `extensions', we provide a semantics: 287 \begin{lstlisting} 288 definition 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 310 Using \texttt{Joint} we get a modular semantics 311 \item 312 `Common' semantics are shared amongst all languages 313 \item 314 Specific languages are responsible for providing the semantics of the extensions that they provide 315 \item 316 Show differences (and similarities) between languages clearly 317 \item 318 Reduces proofs 319 \item 320 Easy to add new languages 321 \end{itemize} 223 322 \end{frame} 224 323
Note: See TracChangeset
for help on using the changeset viewer.