Changeset 1815 for Deliverables


Ignore:
Timestamp:
Mar 9, 2012, 1:19:48 PM (8 years ago)
Author:
mulligan
Message:

Added more to talk

File:
1 edited

Legend:

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

    r1814 r1815  
    104104
    105105\begin{frame}
    106 \frametitle{\texttt{Joint}: a new approach}
    107 XXX: todo
    108 \end{frame}
    109 
    110 \begin{frame}
    111 \frametitle{Commuting passes}
    112 XXX: todo
    113 \end{frame}
    114 
    115 \begin{frame}
    116 \frametitle{Instruction selection in RTLabs}
    117 XXX: todo
     106\frametitle{\texttt{Joint}: a new approach I}
     107\begin{itemize}
     108\item
     109Looking at O'Caml code, languages after RTLabs are similar
     110\item
     111Similar instructions, similar semantics, and so on
     112\item
     113Differences are slight
     114\item
     115Pseudoregisters used instead of hardware registers
     116\item
     117A few new unique instructions for each language
     118\item
     119In semantics: some notion of `successor' of an instruction, etc.
     120\end{itemize}
     121\end{frame}
     122
     123\begin{frame}
     124\frametitle{\texttt{Joint}: a new approach II}
     125\begin{itemize}
     126\item
     127Idea: all of these languages are just instances of a single language
     128\item
     129This language \texttt{Joint} is parameterised by a type of registers to be used in instructions, and so forth
     130\item
     131Each language after RTLabs is now just defined as the \texttt{Joint} language instantiated with some concrete types
     132\item
     133Similarly for semantics: common definitions that take e.g. type representing program counters as parameters
     134\end{itemize}
     135\end{frame}
     136
     137\begin{frame}[fragile]
     138\frametitle{\texttt{Joint}: a new approach III}
     139\texttt{Joint} instructions allow us to embed language-specific instructions:
     140\begin{lstlisting}
     141inductive joint_instruction (p: params__) (globals: list ident): Type[0] :=
     142 | COMMENT: String $\rightarrow$ joint_instruction p globals
     143 | COST_LABEL: costlabel $\rightarrow$ joint_instruction p globals
     144 ...
     145 | COND: acc_a_reg p → label $\rightarrow$ joint_instruction p globals
     146 | extension: extend_statements p $\rightarrow$ joint_instruction p globals.
     147\end{lstlisting}
     148
     149\begin{lstlisting}
     150inductive ertl_statement_extension: Type[0] :=
     151 | ertl_st_ext_new_frame: ertl_statement_extension
     152 | ertl_st_ext_del_frame: ertl_statement_extension
     153 | ertl_st_ext_frame_size: register $\rightarrow$ ertl_statement_extension.
     154\end{lstlisting}
     155\end{frame}
     156
     157\begin{frame}[fragile]
     158\frametitle{\texttt{Joint}: a new approach IV}
     159For example, the definition of the \texttt{ERTL} language is now:
     160\begin{lstlisting}
     161inductive move_registers: Type[0] :=
     162 | pseudo: register $\rightarrow$ move_registers
     163 | hardware: Register $\rightarrow$ move_registers.
     164
     165definition ertl_params__: params__ :=
     166 mk_params__ register register register register
     167  (move_registers $\times$ move_registers)
     168   register nat unit ertl_statement_extension.
     169definition ertl_params_: params_ :=
     170 graph_params_ ertl_params__.
     171definition ertl_params0: params0 :=
     172 mk_params0 ertl_params__ (list register) nat.
     173definition ertl_params1: params1 :=
     174 rtl_ertl_params1 ertl_params0.
     175definition ertl_params: $\forall$globals. params globals ≝
     176 rtl_ertl_params ertl_params0.
     177\end{lstlisting}
     178\end{frame}
     179
     180\begin{frame}
     181\frametitle{\texttt{Joint}: advantages}
     182\begin{itemize}
     183\item
     184Why use \texttt{Joint}, as opposed to defining all languages individually?
     185\item
     186Reduces repeated code (fewer bugs, or places to change)
     187\item
     188Unify some proofs, making correctness proof easier
     189\item
     190Easier to add new intermediate languages as needed
     191\item
     192Easier to see relationship between consecutive languages at a glance
     193\end{itemize}
     194\end{frame}
     195
     196\begin{frame}[fragile]
     197\frametitle{Instruction embedding in \texttt{Joint}}
     198\begin{lstlisting}
     199inductive joint_instruction (p:params__) (globals: list ident): Type[0] :=
     200 ...
     201 | POP: acc_a_reg p $\rightarrow$ joint_instruction p globals
     202 | PUSH: acc_a_reg p $\rightarrow$ joint_instruction p globals
     203 ...
     204\end{lstlisting}
     205\begin{itemize}
     206\item
     207RTLabs (not a \texttt{Joint} language) to RTL is where instruction selection takes place
     208\item
     209Instructions from the MCS-51 instruction set embedded in \texttt{Joint} syntax
     210\end{itemize}
    118211\end{frame}
    119212
    120213\begin{frame}
    121214\frametitle{Semantics of \texttt{Joint} I}
     215\begin{itemize}
     216\item
     217As mentioned, use of \texttt{Joint} also unifies semantics of these languages
     218\end{itemize}
    122219\end{frame}
    123220
Note: See TracChangeset for help on using the changeset viewer.