Changeset 620


Ignore:
Timestamp:
Mar 2, 2011, 3:56:18 PM (9 years ago)
Author:
mulligan
Message:

More changes to presentation. Modified some of the C examples to test for Ayache's reported bug.

Location:
Deliverables
Files:
4 edited

Legend:

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

    r618 r620  
    44\logo{\includegraphics[height=1.0cm]{fetopen.png}}
    55
     6\usepackage{amsfonts}
     7\usepackage{amsmath}
     8\usepackage{amssymb}
    69\usepackage[english]{babel}
    7 \usepackage{inputenc}
     10\usepackage{color}
     11\usepackage[utf8x]{inputenc}
     12\usepackage{listings}
     13\usepackage{stmaryrd}
     14% \usepackage{microtype}
    815
    916\author{Dominic P. Mulligan and Claudio Sacerdoti Coen}
     
    1320\setlength{\parskip}{1em}
    1421
     22\lstdefinelanguage{matita-ocaml}
     23  {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try,on,to},
     24   morekeywords={[2]whd,normalize,elim,cases,destruct},
     25   morekeywords={[3]type,of,val,assert,let,function},
     26   mathescape=true,
     27  }
     28\lstset{language=matita-ocaml,basicstyle=\small\tt,columns=flexible,breaklines=false,
     29        keywordstyle=\color{red}\bfseries,
     30        keywordstyle=[2]\color{blue},
     31        keywordstyle=[3]\color{blue}\bfseries,
     32        commentstyle=\color{green},
     33        stringstyle=\color{blue},
     34        showspaces=false,showstringspaces=false}
     35
    1536\begin{document}
    1637
     
    105126\end{frame}
    106127
    107 \begin{frame}
     128\begin{frame}[fragile]
    108129\frametitle{Polymorphic variants and phantom types}
    109 \begin{itemize}
    110 \item
    111130The instruction set is highly non-orthogonal.
    112 \item
    113 We needed a way of
    114 \end{itemize}
    115 \end{frame}
    116 
    117 \begin{frame}
    118 \frametitle{Use of dependent types}
     131We used polymorphic variants and phantom types to capture this non-orthogonality in the type system.
     132For instance:
     133
     134\begin{small}
     135\begin{lstlisting}
     136type direct = [ `DIRECT of byte ]
     137type indirect = [ `INDIRECT of bit ]
     138...
     139type 'addr preinstruction =
     140 [ `ADD of acc * [ reg | direct | indirect | data ]
     141...
     142 | `MOV of
     143    (acc * [ reg | direct | indirect | data ],
     144     [ reg | indirect ] * [ acc | direct | data ],
     145     direct * [ acc | reg | direct | indirect | data ], ...)
     146...
     147\end{lstlisting}
     148\end{small}
     149\end{frame}
     150
     151\begin{frame}[fragile]
     152\frametitle{Use of dependent types I}
     153This approach worked well in O'Caml, but Matita does not have polymorphic variants, so we need a substitute.
     154We use dependent types.
     155
     156Introduce a type for addressing modes:
     157\begin{small}
     158\begin{lstlisting}
     159inductive addressing_mode: Type[0] :=
     160  DIRECT: Byte $\rightarrow$ addressing_mode
     161...
     162\end{lstlisting}
     163\end{small}
     164And another type \texttt{addressing\_mode\_tag} of `tags' whose constructors are in correspondence with those of \texttt{addressing\_mode}.
     165\end{frame}
     166
     167\begin{frame}[fragile]
     168\frametitle{Use of dependent types II}
     169We use vectors of \texttt{addressing\_mode\_tag}s in our type signatures for instructions.
     170For instance:
     171\begin{small}
     172\begin{lstlisting}
     173inductive preinstruction (A: Type[0]): Type[0] :=
     174   ADD: $\llbracket$ acc_a $\rrbracket$
     175        $\rightarrow$ $\llbracket$ register; direct; indirect; data $\rrbracket$
     176        $\rightarrow$ preinstruction A
     177...
     178\end{lstlisting}
     179\end{small}
     180We need: an \emph{ad hoc} $\Sigma$ type and two coercions.
     181One coercion automatically opens up a proof obligation when it is used, which requires some lemmas.
     182
     183These lemmas and automation close all proof obligations generated (over 300 in typechecking the main interpreter function).
     184\end{frame}
     185
     186\begin{frame}
     187\frametitle{Overlapping memory spaces and addressing modes}
     188MCS-51 memory spaces overlap, and can be addressed using different modes and sized pointers.
     189The status record models memory merely as disjoint spaces, using a `tries with holes' datastructure.
     190
     191All complications to do with overlapping are handled
    119192\end{frame}
    120193
  • Deliverables/D3.1/Report/report.tex

    r417 r620  
    176176\qbezier(-2,407)(-6,407)(-6,393)
    177177\qbezier(-6,393)(-6,324)(-10,324)
    178 \put(-12,324){\makebox(0,0)[r]{indirect}}
     178\put(-12,324){\makebox(0,0)[r]{Indirect/Stack}}
    179179\qbezier(-6,256)(-6,324)(-10,324)
    180180\qbezier(-2,242)(-6,242)(-6,256)
     
    182182\qbezier(94,407)(98,407)(98,393)
    183183\qbezier(98,393)(98,349)(102,349)
    184 \put(104,349){\makebox(0,0)[l]{direct/stack}}
     184\put(104,349){\makebox(0,0)[l]{Direct}}
    185185\qbezier(98,305)(98,349)(102,349)
    186186\qbezier(94,291)(98,291)(98,305)
    187187
    188 \put(102,242){\framebox(20,49){sfr}}
     188\put(102,242){\framebox(20,49){SFR}}
    189189% bit access to sfrs?
    190190
    191191\qbezier(124,291)(128,291)(128,277)
    192192\qbezier(128,277)(128,266)(132,266)
    193 \put(134,266){\makebox(0,0)[l]{direct}}
     193\put(134,266){\makebox(0,0)[l]{Direct}}
    194194\qbezier(128,257)(128,266)(132,266)
    195195\qbezier(124,242)(128,242)(128,256)
     
    201201\put(164,242){\line(1,0){80}}
    202202\put(163,400){\makebox(0,0)[r]{0h}}
    203 \put(164,324){\makebox(80,0){paged access}}
     203\put(164,324){\makebox(80,0){Paged access}}
    204204  \put(164,310){\makebox(80,0){direct/indirect}}
    205205\put(163,235){\makebox(0,0)[r]{80h}}
    206206  \put(164,228){\makebox(80,0){\vdots}}
    207   \put(164,210){\makebox(80,0){direct/indirect}}
     207  \put(164,210){\makebox(80,0){Direct/indirect}}
    208208
    209209\put(264,410){\makebox(80,0)[b]{Code (64kB)}}
     
    213213\put(263,400){\makebox(0,0)[r]{0h}}
    214214  \put(264,228){\makebox(80,0){\vdots}}
    215   \put(264,324){\makebox(80,0){direct}}
     215  \put(264,324){\makebox(80,0){Dsirect}}
    216216  \put(264,310){\makebox(80,0){PC relative}}
    217217\end{picture}
  • Deliverables/D4.1/GCC/IntegerSquareRoot.c

    r165 r620  
    1 #include "stdio.h"
    2 
    31unsigned int isqrt(unsigned int n){
    42  unsigned int a;
     
    119  int i = 0;
    1210  i = isqrt(16);
    13   printf("%d", i);
     11  if(i == 4)
     12    return 1;
    1413  return 0;
    1514}
  • Deliverables/D4.1/Test.hex

    r212 r620  
    1 :03000000020008F3
    2 :0300610002000397
    3 :0500030012006480FE04
    4 :0A006400780575050FD69000002204
    5 :06003700E478FFF6D8FD9D
    6 :080015007900E94400601B7A48
    7 :05001D00009000727864
    8 :030022000075A0C6
    9 :0A00250000E493F2A308B8000205FE
    10 :08002F00A0D9F4DAF275A0FF7C
    11 :08003D007800E84400600A7934
    12 :030045000075A0A3
    13 :0600480000E4F309D8FCFE
    14 :08004E007800E84400600C7921
    15 :0B00560000900000E4F0A3D8FCD9FAF1
    16 :03000800758107F8
    17 :0A000B0012006EE58260030200039C
    18 :04006E007582002275
     1:100000000200081200A480FE7581071200BCE58280
     2:0E00100060030200037900E94400601B7A00DF
     3:10001E009000C0780075A000E493F2A308B8000227
     4:0F002E0005A0D9F4DAF275A0FFE478FFF6D8FD4B
     5:0F003D007800E84400600A790075A000E4F30938
     6:10004C00D8FC7800E84400600C7900900000E4F0E3
     7:10005C00A3D8FCD9FA020003AA82AB837C007D00F2
     8:10006C008C06EDCE25E0CE33FF0EBE00010FC3EAA9
     9:10007C009EEB9F401E8C068D070CBC00010DEFCE35
     10:10008C0025E0CE33FF0EBE00010FEAC39EFAEB9FB4
     11:10009C00FB80CD8C828D8322900010120064AA828A
     12:1000AC00AB83BA0407BB000490000122900000222D
     13:0400BC007582002227
    1914:00000001FF
Note: See TracChangeset for help on using the changeset viewer.