Changeset 335 for Deliverables/D3.1


Ignore:
Timestamp:
Nov 29, 2010, 6:42:10 PM (9 years ago)
Author:
campbell
Message:

Quick pass through 3.1 text.

Location:
Deliverables/D3.1/Report
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/Report/report.tex

    r207 r335  
    128128irregular memory model with tight resource constraints.  The different memory
    129129spaces and access modes are summarised in Figure~\ref{fig:memorymodel} ---
    130 essentially the development of the 8051 family has fragmented memory into
     130essentially the evolution of the 8051 family has fragmented memory into
    131131four regions:  one half of the `internal' memory is fully accessible but also
    132 contains the register banks, the second half cannot be directly addressed
     132contains the register banks, the second half cannot be accessed by direct addressing
    133133because it is shadowed by the `Special Function Registers' (SFRs) for I/O;
    134134`external memory' provides the bulk of memory in a separate address space; and
    135135the code is in its own read-only space.
     136\begin{figure}
     137\setlength{\unitlength}{1pt}
     138\begin{picture}(410,250)(-50,200)
     139%\put(-50,200){\framebox(410,250){}}
     140\put(12,410){\makebox(80,0)[b]{Internal (256B)}}
     141\put(13,242){\line(0,1){165}}
     142\put(93,242){\line(0,1){165}}
     143\put(13,407){\line(1,0){80}}
     144\put(12,400){\makebox(0,0)[r]{0h}}  \put(14,400){\makebox(0,0)[l]{Register bank 0}}
     145\put(13,393){\line(1,0){80}}
     146\put(12,386){\makebox(0,0)[r]{8h}}  \put(14,386){\makebox(0,0)[l]{Register bank 1}}
     147\put(13,379){\line(1,0){80}}
     148\put(12,372){\makebox(0,0)[r]{10h}}  \put(14,372){\makebox(0,0)[l]{Register bank 2}}
     149\put(13,365){\line(1,0){80}}
     150\put(12,358){\makebox(0,0)[r]{18h}} \put(14,358){\makebox(0,0)[l]{Register bank 3}}
     151\put(13,351){\line(1,0){80}}
     152\put(12,344){\makebox(0,0)[r]{20h}} \put(14,344){\makebox(0,0)[l]{Bit addressable}}
     153\put(13,323){\line(1,0){80}}
     154\put(12,316){\makebox(0,0)[r]{30h}}
     155  \put(14,309){\makebox(0,0)[l]{\quad \vdots}}
     156\put(13,291){\line(1,0){80}}
     157\put(12,284){\makebox(0,0)[r]{80h}}
     158  \put(14,263){\makebox(0,0)[l]{\quad \vdots}}
     159\put(12,249){\makebox(0,0)[r]{ffh}}
     160\put(13,242){\line(1,0){80}}
     161
     162\qbezier(-2,407)(-6,407)(-6,393)
     163\qbezier(-6,393)(-6,324)(-10,324)
     164\put(-12,324){\makebox(0,0)[r]{indirect}}
     165\qbezier(-6,256)(-6,324)(-10,324)
     166\qbezier(-2,242)(-6,242)(-6,256)
     167
     168\qbezier(94,407)(98,407)(98,393)
     169\qbezier(98,393)(98,349)(102,349)
     170\put(104,349){\makebox(0,0)[l]{direct/stack}}
     171\qbezier(98,305)(98,349)(102,349)
     172\qbezier(94,291)(98,291)(98,305)
     173
     174\put(102,242){\framebox(20,49){sfr}}
     175% bit access to sfrs?
     176
     177\qbezier(124,291)(128,291)(128,277)
     178\qbezier(128,277)(128,266)(132,266)
     179\put(134,266){\makebox(0,0)[l]{direct}}
     180\qbezier(128,257)(128,266)(132,266)
     181\qbezier(124,242)(128,242)(128,256)
     182
     183\put(164,410){\makebox(80,0)[b]{External (64kB)}}
     184\put(164,220){\line(0,1){187}}
     185\put(164,407){\line(1,0){80}}
     186\put(244,220){\line(0,1){187}}
     187\put(164,242){\line(1,0){80}}
     188\put(163,400){\makebox(0,0)[r]{0h}}
     189\put(164,324){\makebox(80,0){paged access}}
     190  \put(164,310){\makebox(80,0){direct/indirect}}
     191\put(163,235){\makebox(0,0)[r]{80h}}
     192  \put(164,228){\makebox(80,0){\vdots}}
     193  \put(164,210){\makebox(80,0){direct/indirect}}
     194
     195\put(264,410){\makebox(80,0)[b]{Code (64kB)}}
     196\put(264,220){\line(0,1){187}}
     197\put(264,407){\line(1,0){80}}
     198\put(344,220){\line(0,1){187}}
     199\put(263,400){\makebox(0,0)[r]{0h}}
     200  \put(264,228){\makebox(80,0){\vdots}}
     201  \put(264,324){\makebox(80,0){direct}}
     202  \put(264,310){\makebox(80,0){PC relative}}
     203\end{picture}
     204\caption{The extended 8051 memory model}
     205\end{figure}
    136206
    137207To make efficient use of the limited amount of memory, compilers for 8051
     
    142212\begin{table}[ht]
    143213\begin{tabular}{rcl}
    144 Attribute & Pointer size & Memory space \\\hline
     214Attribute & Pointer size (bytes) & Memory space \\\hline
    145215\lstinline'__data' & 1 & Internal, first half (0h -- 7fh) \\
    146216\lstinline'__idata' & 1 & Internal, indirect only (80h -- ffh) \\
     
    154224
    155225We intend the \cerco{} compiler to support extensions that are broadly
    156 compatible with \sdcc{} to enable the compilation of programs with either.  In
    157 particular, this would allow the comparison of the behaviour of test cases
    158 compiled with both compilers.  Thus the C syntax and semantics have been
    159 extended with the memory space attributes listed above.  The syntax follows
    160 \sdcc{} and in the semantics we track the memory space that each block was
    161 allocated in and only permit access via the appropriate kinds of pointers.
    162 The details on these changes are given in the following sections.
     226compatible with \sdcc{} to enable the compilation of programs with
     227either tool.  In particular, this would allow the comparison of the
     228behaviour of test cases compiled with each compiler.  Thus the C
     229syntax and semantics have been extended with the memory space
     230attributes listed above.  The syntax follows \sdcc{} and in the
     231semantics we track the memory space that each block was allocated in
     232and only permit access via the appropriate kinds of pointers.  The
     233details on these changes are given in the following sections.
    163234
    164235The \sdcc{} compiler also supports special variable types for accessing the
    165236SFRs, which provide the standard I/O mechanism for the 8051 family.  (Note
    166 that pointers to these types are not allowed because only direct addressing of
     237that pointers to these types are not permitted because only direct addressing of
    167238the SFRs is allowed.)  We intend to use CompCert-style `external functions'
    168239instead of special types.  These are functions which are declared, but no C
    169 implementation is provided.  Instead they are provided by the runtime or
     240implementation of them is provided.  Instead they are provided by the runtime or
    170241compiled directly to the corresponding machine code.  This has the advantage
    171242that no changes from the CompCert semantics are required, and a compatibility
     
    175246compiler, and so no extension is provided for it.
    176247
     248Finally, we adopt the \sdcc{} extension to allocate a variable at a
     249particular address to provide a way to deal with memory mapped I/O in
     250the external memory space.
     251\todo{Are we really going to do this?}
     252
    177253\section{Port of CompCert \clight{} semantics to \matita{}}
    178254\label{sec:port}
    179255
     256\todo{Could do with some text here}
     257\subsection{Parsing and elaboration}
    180258The first stage taken from the CompCert semantics is the parsing and
    181259elaboration of C programs into the simpler \clight{} language.  This is based
     
    184262information throughout the program, including extra casts for promotion, and
    185263performs simplifications such as breaking up expressions with side effects
    186 into statements that perform the effects using effect-free expressions.  The
     264into effect-free expressions and statements to perform the effects.  The
    187265transformed \clight{} programs are much more manageable and lack the ambiguities
    188266of C, but also remain easily understood by C programmers.
     
    191269above.  The resulting abstract syntax tree records them on global variable
    192270declarations and pointer types.  However, we also need to deal with them
    193 during the elaboration process to produce all of the required information.
     271during the elaboration process to produce all of the required type information.
    194272For example, when the address-of operator \lstinline'&' is used it must decide
    195273which kind of pointer should be used.  Thus the extended elaboration process
     
    201279
    202280
    203 Thus the elaboration turns the C code
     281Thus the elaboration turns the following C code
    204282\begin{quote}
    205283\begin{lstlisting}[language=C]
     
    217295\end{lstlisting}
    218296\end{quote}
    219 into the following Clight program:
     297into the Clight program below:
    220298\begin{quote}
    221299\begin{lstlisting}[language=C]
     
    245323and pointers specific to the \lstinline'__data' section of memory.  The
    246324underlying data structure also has types attached to every expression, but
    247 these are inconvenient to show in source form.
    248 
    249 Note that the translation from C to \clight{} is not proven correct ---
    250 instead it effectively forms a semi-formal part of the whole C semantics.  We
    251 can have some confidence in the code, however, because it has received testing
    252 in the \cerco{} prototype, and it is very close to the version used in
    253 CompCert.  We can also perform testing of the semantics without involving the
    254 rest of the compiler because we have an executable semantics.  Moreover, the
    255 cautious programmer could choose to inspect the \clight{} code, or even work
    256 entirely in the \clight{} language.
     325these are impractical to show in source form.
     326
     327Note that the translation from C to \clight{} is not proven correct
     328--- instead it effectively forms a semi-formal part of the whole C
     329semantics.  We can have some confidence in the code, however, because
     330it has received testing in the \cerco{} prototype, and it is very
     331close to the version used in CompCert.  We can also perform testing of
     332the semantics without involving the rest of the compiler because we
     333have an executable semantics.  Moreover, the cautious programmer could
     334choose to inspect the generated \clight{} code, or even work entirely
     335in the \clight{} language.
     336
     337\subsection{Small-step inductive semantics}
    257338
    258339The semantics for \clight{} itself has been ported from the Coq development
     
    265346development, notably:
    266347\begin{itemize}
    267 \item representation of primitive values (integers, pointers and undefined
     348\item the representation of primitive values (integers, pointers and undefined
    268349values, but not structures or unions) and operations on them,
    269350\item traces of I/O events,
     
    276357\item common error handling constructs, in particular an error monad.
    277358\end{itemize}
    278 We anticipate a similar arrangement for the \cerco{} verified compiler,
    279 although this means that there may be further changes to the common parts of the
    280 semantics later in the project to harmonise the stages of the compiler.
     359We anticipate a similar arrangement for the \cerco{} verified
     360compiler, although this means that there may be further changes to the
     361common parts of the semantics later in the project to harmonise the
     362stages of the compiler.  In particular, some of data structures for
     363environments are just preliminary definitions for developing the
     364semantics.
    281365
    282366The main body of the small-step semantics is a number of inductive definitions
     
    318402\end{lstlisting}
    319403\end{quote}
    320 simply looks up the variable in the local environment.  A similar rule handles
    321 global variables, with an extra check to ensure that no local variable has the
    322 same name.  Note that the two relations are defined using mutual recursion
    323 because \lstinline'eval_lvalue' uses \lstinline'eval_expr' for the evaluation
    324 of the pointer expression in the dereferencing rule.
     404simply looks up the variable in the local environment.  The offset is
     405zero because all variables are given their own memory block to prevent
     406the use of stray pointers.  A similar rule handles global variables,
     407with an extra check to ensure that no local variable has the same
     408name.  Note that the two relations are defined using mutual recursion
     409because \lstinline'eval_lvalue' uses \lstinline'eval_expr' for the
     410evaluation of the pointer expression in the dereferencing rule.
    325411
    326412Casts also have an auxiliary relation to specify the allowed changes, and
     
    328414casting) are given as functions.
    329415
    330 The only new expression in our semantics is the cost label which wraps around
    331 another expression.  It does not change the result, but merely adds the given
    332 label to the trace to identify the branches taken in conditional
    333 expressions so that accurate cost information can be attached to the program:
     416The only new expression in our semantics is the cost label which wraps
     417around another expression.  It does not change the result, but merely
     418prefixes the trace with the given label to identify the branches taken
     419in conditional expressions so that accurate cost information can be
     420attached to the program:
    334421\begin{quote}
    335422\begin{lstlisting}
     
    364451\end{lstlisting}
    365452\end{quote}
    366 During normal execution the state contains the currently executing function's
    367 definition (used to find \lstinline'goto' labels and also to check whether the
    368 function is expected to return a value), the statement to be executed next, a
    369 continuation value to be executed afterwards (where successor statements and
    370 details of function calls and loops are stored), the local environment mapping
    371 variables to memory locations and the current memory state.
    372 \todo{need to note that all variables 'appear' to be memory allocated, even
    373        if they're subsequently optimised away.}
    374 The function call and return states appear to store less information because
    375 the details of the caller are contained in the continuation.
     453During normal execution the state contains the currently executing
     454function's definition (used to find \lstinline'goto' labels and also
     455to check whether the function is expected to return a value), the
     456statement to be executed next, a continuation value to be executed
     457afterwards (where successor statements and details of function calls
     458and loops are stored), the local environment mapping variables to
     459memory locations\footnote{In the semantics all variables are
     460  allocated, although the compiler may subsequently allocate them to
     461  registers where possible.} and the current memory state.  \todo{need
     462  to note that all variables 'appear' to be memory allocated, even if
     463  they're subsequently optimised away.}  The function call and return
     464states appear to store less information because the details of the
     465caller are contained in the continuation.
    376466
    377467An example of the statement execution rules is the assignment rule
     
    393483\begin{itemize}
    394484\item if \lstinline'a1' can evaluate to the location \lstinline'psp,loc,ofs',
    395 \item \lstinline'a2' evaluates to a value \lstinline'v2', and
     485\item \lstinline'a2' can evaluate to a value \lstinline'v2', and
    396486\item storing \lstinline'v2' at location \lstinline'psp,loc,ofs' succeeds,
    397487yielding the new memory state \lstinline-m'-, then
     
    401491\end{itemize}
    402492This rule would be followed by one of the rules to which replaces the
    403 \lstinline'Sskip' statement with the `real' next statement constructed from
    404 the continuation \lstinline'k'.  Note that the only true side-effect here is
    405 the change in memory --- the local environment is initialised once and for all
    406 on function entry, and the only events appearing in the trace are cost labels
    407 used purely for accounting.
    408 \todo{ordering imposed by cost labels?}
     493\lstinline'Sskip' statement with the `real' next statement constructed
     494from the continuation \lstinline'k'.  Note that the only true
     495side-effect here is the change in memory --- the local environment is
     496initialised once and for all on function entry, and the only events
     497appearing in the trace are cost labels used purely for accounting.  At
     498present this imposes an ordering due to the cost labels.  Should this
     499prove too restrictive we may change it to produce a set of labels
     500encountered.
    409501
    410502The \clight{} language provides input and output effects through `external'
     
    428520\label{sec:exec}
    429521
    430 \todo{bit of a cheat to claim that it's equivalent without a completeness
    431 proof.}
    432522We have added an equivalent functional version of the \clight{} semantics that
    433523can be used to animate programs.  The definitions roughly follow the inductive
    434524semantics, but are necessarily rearranged around pattern matching of the
    435525relevant parts of the state rather than presenting each case separately.
     526
     527\subsection{Expressions}
    436528
    437529The code corresponding to the variable lookup definitions on
     
    493585rule from the inductive semantics.
    494586
     587\subsection{Statements}
     588
    495589Evaluating a step of a statement is complicated by the presence of the
    496590`external' functions for I/O, which can return arbitrary values.  These are
Note: See TracChangeset for help on using the changeset viewer.