Changeset 555


Ignore:
Timestamp:
Feb 17, 2011, 2:17:11 PM (6 years ago)
Author:
mulligan
Message:

Resolved conflict, updated bibtex, finished bibliography, and llncs.cls updated to latest version.

Location:
Deliverables/D4.1/ITP-Paper
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/ITP-Paper/itp-2011.bib

    r551 r555  
     1@article
     2{ bate:wcet:2011,
     3  author = {Iain Bate and Usman Khan},
     4  title = {{WCET} analysis of modern processors using multi-criteria optimisation},
     5  journal = {Empirical Software Engineering},
     6  pages = {5--28},
     7  volume = {16},
     8  issue = {1},
     9  year = {2011}
     10}
     11
    112@article
    213{ leroy:formal:2009,
     
    1930  pages = {363--446},
    2031  year = {2009}
     32}
     33
     34@inproceedings
     35{ yan:wcet:2008,
     36  author = {Jun Yan and Wei Zhang},
     37  title = {{WCET} Analysis for Multi-Core Processors with Shared {L2} Instruction Caches},
     38  booktitle = {Proceedings of the Fourteenth {IEEE} Symposium on Real-time and Embedded Technology and Applications ({RTAS 2008})},
     39  pages = {80--89},
     40  year = {2008}
    2141}
    2242
     
    6686
    6787@inproceedings
     88{ garrigue:programming:1998,
     89  author = {Jacques Garrigue},
     90  title = {Programming with polymorphic variants},
     91  booktitle = {The {ML} Workshop},
     92  year = {1998}
     93}
     94
     95@inproceedings
     96{ leijen:domain:1999,
     97  author = {Daan Leijen and Erik Meijer},
     98  title = {Domain specific embedded compilers},
     99  booktitle = {Proceedings of the Second Conference on Domain Specific Languages {(DSL 1999)}},
     100  series = {{ACM SIGPLAN} Notices},
     101  pages = {109--122},
     102  volume = {2},
     103  year = {1999}
     104}
     105
     106@inproceedings
    68107{ sarkar:semantics:2009,
    69108  author = {Susmit Sarkar and Peter Sewell and Francesco Zappa Nardelli and Scott Owens and Tom Ridge and Thomas Braibant and Magnus O. Myreen and Jade Alglave},
     
    94133
    95134@misc
     135{ oliboni:matita:2008,
     136  author = {Cosimo A. Oliboni},
     137  title = {{Matita} come Supporto per Specifiche Eseguibili: Formalizzazione Interattiva dei Microcontroller a 8 bit {Freescale}},
     138  institution = {Dipartimento di Scienze dell'Informazione, Universit\`a di Bologna},
     139  howpublished = {\url{http://matita.cs.unibo.it/library.shtml}},
     140  year = {2008}
     141}
     142
     143@misc
    96144{ sdcc:2010,
    97145  title = {Small Device {C} Compiler {(SDCC)} 3.0.0},
     
    99147  year = {2010},
    100148  key = {{SDCC}}
     149}
     150
     151@misc
     152{ siemens:2011,
     153  title = {Siemens Semiconductor Group 8051 derivative instruction set},
     154  howpublished = {\url{http://www.win.tue.nl/~aeb/comp/8051/instruction-set.pdf}},
     155  year = {2011},
     156  key = {{Siemens}}
    101157}
    102158
  • Deliverables/D4.1/ITP-Paper/itp-2011.tex

    r554 r555  
    88\usepackage{fancybox}
    99\usepackage{graphicx}
     10\usepackage[colorlinks]{hyperref}
    1011\usepackage[utf8x]{inputenc}
    1112\usepackage{listings}
     
    5859\institute{Dipartimento di Scienze dell'Informazione, Universit\`a di Bologna}
    5960
    60 \bibliographystyle{alpha}
     61\bibliographystyle{plain}
    6162
    6263\begin{document}
     
    101102To what extent can you trust your compiler in preserving those properties?
    102103\end{itemize*}
    103 These questions, and others like them, motivate a current `hot topic' in computer science research: \emph{compiler verification} (for instance~\cite{leroy:formal:2009, chlipala:verified:2010}, and many others).
     104These questions, and others like them, motivate a current `hot topic' in computer science research: \emph{compiler verification} (for instance~\cite{leroy:formal:2009,chlipala:verified:2010}, and many others).
    104105So far, the field has been focused on the first and last questions only.
    105106In particular, much attention has been placed on verifying compiler correctness with respect to extensional properties of programs, which are easily preserved during compilation; it is sufficient to completely preserve the denotational semantics of the input program.
     
    130131
    131132In the methodology proposed in CerCo we assume we are able to compute on the object code exact and realistic costs for sequential blocks of instructions.
    132 With modern processors, though possible~\cite{??,??,??}, it is difficult to compute exact costs or to reasonably approximate them.
     133With modern processors, though possible (see~\cite{bate:wcet:2011,yan:wcet:2008} for instance), it is difficult to compute exact costs or to reasonably approximate them.
    133134This is because the execution of a program itself has an influence on the speed of processing.
    134135For instance, caching, memory effects and other advanced features such as branch prediction all have a profound effect on execution speeds.
     
    136137These are still widely used in embedded systems, and have the advantage of an easily predictable cost model due to the relative sparcity of features that they possess.
    137138
    138 In particular, we have fully formalised an executable formal semantics of a family of 8 bit Freescale Microprocessors~\cite{oliboni}, and provided a similar executable formal semantics for the MCS-51 microprocessor.
     139In particular, we have fully formalised an executable formal semantics of a family of 8 bit Freescale Microprocessors~\cite{oliboni:matita:2008}, and provided a similar executable formal semantics for the MCS-51 microprocessor.
    139140The latter work is what we describe in this paper.
    140141The main focus of the formalisation has been on capturing the intensional behaviour of the processor.
     
    279280\end{figure}
    280281
    281 The formalization of MCS-51 must deal with bytes (8 bits), words (16 bits) but also with more exoteric quantities (7 bits, 3 bits, 9 bits). To avoid size mismatch bugs difficult to spot, we represent all of these quantities using bitvectors, i.e. fixed length vectors of booleans.
     282The formalization of MCS-51 must deal with bytes (8 bits), words (16 bits) but also with more exoteric quantities (7 bits, 3 bits, 9 bits).
     283To avoid size mismatch bugs difficult to spot, we represent all of these quantities using bitvectors, i.e. fixed length vectors of booleans.
    282284In our O'Caml emulator, we `faked' bitvectors using phantom types implemented with polymorphic variants\cite{phantom_types_ocaml}, as in Figure~\ref{fig.ocaml.implementation.bitvectors}.
    283 From within the bitvector module (left column) bitvectors are just lists of bits and no guarantee is provided on sizes. However, the module's interface (right column) enforces the size invariants in the rest of the code.
     285From within the bitvector module (left column) bitvectors are just lists of bits and no guarantee is provided on sizes.
     286However, the module's interface (right column) enforces the size invariants in the rest of the code.
    284287
    285288In Matita, we are able to use the full power of dependent types to always work with vectors of a known size:
     
    387390The next instruction to be processed, indexed by the program counter, is fetched from code memory with \texttt{fetch}.
    388391An updated program counter, along with the concrete cost, in processor cycles for executing this instruction, is also returned.
    389 These costs are taken from a Siemen's data sheet for the MCS-51, and will likely vary across manufacturers and particular derivatives of the processor.
     392These costs are taken from a Siemens Semiconductor Group data sheet for the MCS-51~\cite{siemens:2011}, and will likely vary across manufacturers and particular derivatives of the processor.
    390393\begin{lstlisting}
    391394definition fetch:
     
    680683
    681684Executability is another key difference between our work and~\cite{fox:trustworthy:2010}.
     685Our formalisation is executable: applying the emulation function to an input state eventually reduces to an output state that already satisfies the appropriate conditions.
     686This is because Matita is based on a logic that internalizes conversion.
    682687In~\cite{fox:trustworthy:2010} the authors provide an automation layer to derive single step theorems: if the processor is in a particular state that satisfies some preconditions, then after execution of an instruction it will reside in another state satisfying some postconditions.
    683688We do not need single step theorems of this form.
    684 This is because Matita is based on a logic that internalizes conversion.
    685 As a result, our formalisation is executable: applying the emulation function to an input state eventually reduces to an output state that already satisfies the appropriate conditions.
    686689
    687690Our main difficulties resided in the non-uniformity of an old 8-bit architecture, in terms of the instruction set, addressing modes and memory models.
  • Deliverables/D4.1/ITP-Paper/llncs.cls

    r492 r555  
    1 % LLNCS DOCUMENT CLASS -- version 2.14 (17-Aug-2004)
     1% LLNCS DOCUMENT CLASS -- version 2.17 (12-Jul-2010)
    22% Springer Verlag LaTeX2e support for Lecture Notes in Computer Science
    33%
     
    2020%%
    2121\NeedsTeXFormat{LaTeX2e}[1995/12/01]
    22 \ProvidesClass{llncs}[2004/08/17 v2.14
     22\ProvidesClass{llncs}[2010/07/12 v2.17
    2323^^J LaTeX document class for Lecture Notes in Computer Science]
    2424% Options
     
    3636\DeclareOption{runningheads}{\let\if@runhead\iftrue}
    3737
     38\let\if@openright\iftrue
    3839\let\if@openbib\iffalse
    3940\DeclareOption{openbib}{\let\if@openbib\iftrue}
     
    5051\LoadClass[twoside]{article}
    5152\RequirePackage{multicol} % needed for the list of participants, index
     53\RequirePackage{aliascnt}
    5254
    5355\setlength{\textwidth}{12.2cm}
     
    9092\def\exercisename{Exercise}
    9193\def\figurename{Fig.}
    92 \def\keywordname{{\bf Key words:}}
     94\def\keywordname{{\bf Keywords:}}
    9395\def\indexname{Index}
    9496\def\lemmaname{Lemma}
     
    540542\def\@dotsep{2}
    541543
     544\let\phantomsection=\relax
     545
    542546\def\hyperhrefextend{\ifx\hyper@anchor\@undefined\else
    543 {chapter.\thechapter}\fi}
     547{}\fi}
    544548
    545549\def\addnumcontentsmark#1#2#3{%
    546550\addtocontents{#1}{\protect\contentsline{#2}{\protect\numberline
    547                      {\thechapter}#3}{\thepage}\hyperhrefextend}}
     551                     {\thechapter}#3}{\thepage}\hyperhrefextend}}%
    548552\def\addcontentsmark#1#2#3{%
    549 \addtocontents{#1}{\protect\contentsline{#2}{#3}{\thepage}\hyperhrefextend}}
     553\addtocontents{#1}{\protect\contentsline{#2}{#3}{\thepage}\hyperhrefextend}}%
    550554\def\addcontentsmarkwop#1#2#3{%
    551 \addtocontents{#1}{\protect\contentsline{#2}{#3}{0}\hyperhrefextend}}
     555\addtocontents{#1}{\protect\contentsline{#2}{#3}{0}\hyperhrefextend}}%
    552556
    553557\def\@adcmk[#1]{\ifcase #1 \or
     
    555559  \or    \def\@gtempa{\addcontentsmark}%
    556560  \or    \def\@gtempa{\addcontentsmarkwop}%
    557   \fi\@gtempa{toc}{chapter}}
    558 \def\addtocmark{\@ifnextchar[{\@adcmk}{\@adcmk[3]}}
     561  \fi\@gtempa{toc}{chapter}%
     562}
     563\def\addtocmark{%
     564\phantomsection
     565\@ifnextchar[{\@adcmk}{\@adcmk[3]}%
     566}
    559567
    560568\def\l@chapter#1#2{\addpenalty{-\@highpenalty}
     
    780788
    781789\long\def\@makecaption#1#2{%
     790  \small
    782791  \vskip\abovecaptionskip
    783792  \sbox\@tempboxa{{\bfseries #1.} #2}%
     
    875884\@ifundefined{extrasgerman}{}{\addto\extrasgerman{\switcht@deutsch}}%
    876885}{\switcht@@therlang}%
     886\providecommand{\keywords}[1]{\par\addvspace\baselineskip
     887\noindent\keywordname\enspace\ignorespaces#1}%
    877888}
    878889\def\homedir{\~{ }}
     
    881892\clearheadinfo
    882893%
     894%%% to avoid hyperref warnings
     895\providecommand*{\toclevel@author}{999}
     896%%% to make title-entry parent of section-entries
     897\providecommand*{\toclevel@title}{0}
     898%
    883899\renewcommand\maketitle{\newpage
     900\phantomsection
    884901  \refstepcounter{chapter}%
    885902  \stepcounter{section}%
     
    10401057  \@ifundefined{c@#2}{\@latexerr{No theorem environment `#2' defined}\@eha}%
    10411058  {\expandafter\@ifdefinable\csname #1\endcsname
    1042   {\global\@namedef{the#1}{\@nameuse{the#2}}%
     1059  {\newaliascnt{#1}{#2}%
    10431060  \expandafter\xdef\csname #1name\endcsname{#3}%
    1044   \global\@namedef{#1}{\@spthm{#2}{\csname #1name\endcsname}{#4}{#5}}%
     1061  \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#4}{#5}}%
    10451062  \global\@namedef{end#1}{\@endtheorem}}}}
    10461063
Note: See TracChangeset for help on using the changeset viewer.