Ignore:
Timestamp:
Sep 9, 2011, 9:49:44 AM (8 years ago)
Author:
mulligan
Message:

got paper down to 15 and a half pages with nothing much added to document

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

Legend:

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

    r819 r1199  
    11@article
    22{ asperti:user:2007,
    3   author = {Andrea Asperti and Claudio Sacerdoti Coen and Enrico Tassi and Stefano Zacchiroli},
     3  author = {A. Asperti and C. Sacerdoti Coen and E. Tassi and S. Zacchiroli},
    44  title = {User interaction with the {Matita} proof assistant},
    5   journal = {Journal of Automated Reasoning},
     5  journal = {Automated Reasoning},
    66  pages = {109--139},
    77  volume = {39},
     
    1212@article
    1313{ bate:wcet:2011,
    14   author = {Iain Bate and Usman Khan},
     14  author = {I. Bate and U. Khan},
    1515  title = {{WCET} analysis of modern processors using multi-criteria optimisation},
    1616  journal = {Empirical Software Engineering},
     
    2323@article
    2424{ leroy:formal:2009,
    25   author = {Xavier Leroy},
     25  author = {X. Leroy},
    2626  title = {Formal verification of a realistic compiler},
    27   journal = {Communications of the {Association of Computing Machinery}},
     27  journal = {CACM},
    2828  volume = {52},
    2929  number = {7},
     
    3434@article
    3535{ leroy:formally:2009,
    36   author = {Xavier Leroy},
     36  author = {X. Leroy},
    3737  title = {A formally verified compiler back-end},
    38   journal = {Journal of Automated Reasoning},
     38  journal = {Automated Reasoning},
    3939  volume = {43},
    4040  number = {4},
     
    4545@article
    4646{ luo:coercive:1999,
    47   author = {Zhaohui Luo},
     47  author = {Z. Luo},
    4848  title = {Coercive subtyping},
    49   journal = {Journal of Logic and Computation},
     49  journal = {Logic and Computation},
    5050  volume = {9},
    5151  number = {1},
     
    5656@inproceedings
    5757{ yan:wcet:2008,
    58   author = {Jun Yan and Wei Zhang},
     58  author = {J. Yan and W. Zhang},
    5959  title = {{WCET} Analysis for Multi-Core Processors with Shared {L2} Instruction Caches},
    60   booktitle = {$\mathrm{14^{th}}$ {IEEE} Symposium on Real-time and Embedded Technology and Applications},
     60  booktitle = {{RTAS}},
    6161  pages = {80--89},
    6262  year = {2008}
     
    6565@inproceedings
    6666{ atkey:coqjvm:2007,
    67   author = {Robert Atkey},
     67  author = {R. Atkey},
    6868  title = {{CoqJVM}: An executable specification of the {Java Virtual Machine} using dependent types},
    69   booktitle = {Conference of the {TYPES} Project},
     69  booktitle = {{TYPES}},
    7070  pages = {18--32},
    7171  year = {2007}
     
    7575{ blanqui:designing:2010,
    7676  title = {Designing a {CPU} model: from a pseudo-formal document to fast code},
    77   author = {Fr\'ed\'eric Blanqui and Claude Helmstetter and Vania Joloboff and Jean-Fran\c{c}ois Monin and Xiaomu Shi},
    78   booktitle = {$\mathrm{3^{rd}}$ Workshop on Rapid Simulation and Performance Evaluation: Methods and Tools},
     77  author = {F. Blanqui and C. Helmstetter and V. Joloboff and J. Monin and X. Shi},
     78  booktitle = {{RAPIDO}},
    7979  year = {2010}
    8080}
     
    8282@inproceedings
    8383{ blazy:formal:2006,
    84   author = {Sandrine Blazy and Zaynah Dargaye and Xavier Leroy},
     84  author = {S. Blazy and Z. Dargaye and X. Leroy},
    8585  title = {Formal Verification of a {C} Compiler Front-End},
    86   booktitle = {International Symposium on Formal Methods},
     86  booktitle = {FM},
    8787  pages = {460--475},
    8888  year = {2006}
     
    9191@inproceedings
    9292{ chlipala:verified:2010,
    93   author = {Adam Chlipala},
     93  author = {A. Chlipala},
    9494  title = {A verified compiler for an impure functional language},
    95   booktitle = {$\mathrm{37^{th}}$ Annual Symposium on Principles of Programming Languages},
     95  booktitle = {POPL},
    9696  pages = {93--106},
    9797  year = {2010}
     
    100100@inproceedings
    101101{ fox:trustworthy:2010,
    102   author = {Anthony Fox and Magnus O. Myreen},
     102  author = {A. Fox and M. O. Myreen},
    103103  title = {A Trustworthy Monadic Formalization of the {ARMv7} Instruction Set Architecture},
    104   booktitle = {$\mathrm{1^{st}}$ International Conference on Interactive Theorem Proving},
     104  booktitle = {ITP},
    105105  pages = {243--258},
    106106  year = {2010}
     
    109109@inproceedings
    110110{ garrigue:programming:1998,
    111   author = {Jacques Garrigue},
     111  author = {J. Garrigue},
    112112  title = {Programming with polymorphic variants},
    113113  booktitle = {{ML} Workshop},
     
    117117@inproceedings
    118118{ leijen:domain:1999,
    119   author = {Daan Leijen and Erik Meijer},
     119  author = {D. Leijen and E. Meijer},
    120120  title = {Domain specific embedded compilers},
    121   booktitle = {$\mathrm{2^{nd}}$ Conference on Domain Specific Languages},
     121  booktitle = {DSL},
    122122  pages = {109--122},
    123123  year = {1999}
     
    126126@inproceedings
    127127{ sarkar:semantics:2009,
    128   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},
     128  author = {S. Sarkar and P. Sewell and F. Zappa Nardelli and S. Owens and T. Ridge and T. Braibant and M. O. Myreen and J. Alglave},
    129129  title = {The semantics of {x86-CC} multiprocessor machine code},
    130   booktitle = {$\mathrm{36^{th}}$ Annual Symposium on Principles of Programming Languages},
     130  booktitle = {POPL},
    131131  pages = {379--391},
    132132  year = {2009}
     
    135135@inproceedings
    136136{ shankar:principles:1999,
    137   author = {Natarajan Shankar and Sam Owre},
     137  author = {N. Shankar and S. Owre},
    138138  title = {Principles and Pragmatics of Subtyping in {PVS}},
    139139  booktitle = {Recent Trends in Algebraic Development Techniques},
     
    144144@inproceedings
    145145{ sozeau:subset:2006,
    146   author = {Matthieu Sozeau},
     146  author = {M. Sozeau},
    147147  title = {Subset coercions in {Coq}},
    148   booktitle = {Conference of the {TYPES} Project},
     148  booktitle = {{TYPES}},
    149149  pages = {237--252},
    150150  year = {2006}
     
    153153@inproceedings
    154154{ xi:guarded:2003,
    155   author = {Hongwei Xi and Chiyan Chen and Gang Chen},
     155  author = {H. Xi and C. Chen and G. Chen},
    156156  title = {Guarded recursive datatype constructors},
    157   booktitle = {$\mathrm{30^{th}}$ Annual Symposium on Principles of Programming Languages},
     157  booktitle = {POPL},
    158158  pages = {224--235},
    159159  year = {2003}
     
    162162@misc
    163163{ cerco:2011,
    164   title = {The {CerCo} {FET-Open} Project},
     164  title = {The {CerCo} Project},
    165165  howpublished = {\url{http://cerco.cs.unibo.it}},
    166166  year = {2011},
     
    186186@misc
    187187{ moore:grand:2005,
    188   author = {J Strother Moore},
     188  author = {J S. Moore},
    189189  title = {A Grand Challenge Proposal for Formal Methods},
    190190  year = {2005}
     
    193193@misc
    194194{ oliboni:matita:2008,
    195   author = {Cosimo A. Oliboni},
     195  author = {C. A. Oliboni},
    196196  title = {{Matita} come Supporto per Specifiche Eseguibili: Formalizzazione Interattiva dei Microcontroller a 8 bit {Freescale}},
    197   institution = {Dipartimento di Scienze dell'Informazione, Universit\`a di Bologna},
     197  institution = {Universit\`a di Bologna},
    198198  howpublished = {\url{http://matita.cs.unibo.it/library.shtml}},
    199199  year = {2008}
     
    218218@techreport
    219219{ amadio:certifying:2010,
    220   author = {Roberto M. Amadio and Nicolas Ayache and Yann R\'{e}gis-Gianas and Ronan Saillard},
     220  author = {R. M. Amadio and N. Ayache and Y. R\'{e}gis-Gianas and R. Saillard},
    221221  title = {Cerifying cost annotations in compilers},
    222   institution = {Universit\'{e} Paris Diderot {(Paris 7)}, Laboratoire {PPS}},
    223   year = {2010}
    224 }
     222  institution = {Universit\'{e} Paris Diderot},
     223  year = {2010}
     224}
  • Deliverables/D4.1/ITP-Paper/itp-2011.tex

    r1190 r1199  
    3636   mathescape=true,
    3737  }
    38 \lstset{language=matita-ocaml,basicstyle=\tt,columns=flexible,breaklines=false,
     38\lstset{language=matita-ocaml,basicstyle=\scriptsize\tt,columns=flexible,breaklines=false,
    3939        keywordstyle=\bfseries, %\color{red}\bfseries,
    4040        keywordstyle=[2]\bfseries, %\color{blue},
     
    5454}
    5555
     56\setlength{\belowcaptionskip}{0pt}
     57\setlength{\textfloatsep}{1em}
     58
    5659\begin{document}
    5760
    5861\author{Dominic P. Mulligan \and Claudio Sacerdoti Coen}
    5962\authorrunning{D. P. Mulligan \and C. Sacerdoti Coen}
    60 \institute{Dipartimento di Scienze dell'Informazione,\\ Universit\`a di Bologna}
    61 %\and
    62 %  \IEEEauthorblockN{Claudio Sacerdoti Coen}
    63 %  \IEEEauthorblockA{Dipartimento di Scienze dell'Informazione,\\ Universit\`a di Bologna}
    64 %}
     63\institute{\vspace{-2em}}
     64% \institute{Dipartimento di Scienze dell'Informazione,\\ Universit\`a di Bologna}
    6565
    6666\bibliographystyle{plain}
     
    8282\end{abstract}
    8383
    84 \begin{keywords}
    85 Hardware formalisation, Matita, dependent types, CerCo
    86 \end{keywords}
     84%\begin{keywords}
     85%Hardware formalisation, Matita, dependent types, CerCo
     86%\end{keywords}
    8787
    8888%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     
    395395inductive BitVectorTrie(A: Type[0]):nat $\rightarrow$ Type[0] :=
    396396  Leaf: A $\rightarrow$ BitVectorTrie A 0
    397 | Node: ∀n. BitVectorTrie A n $\rightarrow$ BitVectorTrie A n $\rightarrow$
    398   BitVectorTrie A (S n)
     397| Node: ∀n. BitVectorTrie A n $\rightarrow$ BitVectorTrie A n $\rightarrow$ BitVectorTrie A (S n)
    399398| Stub: ∀n. BitVectorTrie A n.
    400399\end{lstlisting}
     
    473472These costs are taken from a Siemens Semiconductor Group data sheet for the MCS-51~\cite{siemens:2011}, and will likely vary between particular implementations.
    474473\begin{lstlisting}[frame=single]
    475 definition fetch: BitVectorTrie Byte 16 $\rightarrow$ Word $\rightarrow$
    476   instruction $\times$ Word $\times$ nat
     474definition fetch: BitVectorTrie Byte 16 $\rightarrow$ Word $\rightarrow$ instruction $\times$ Word $\times$ nat
    477475\end{lstlisting}
    478476Instruction are assembled to bit encodings by \texttt{assembly1}:
     
    484482A map associating memory locations and cost labels (see Subsection~\ref{subsect.computation.cost.traces}) is produced.
    485483\begin{lstlisting}[frame=single]
    486 definition assembly: assembly_program $\rightarrow$
    487   option (list Byte $\times$ (BitVectorTrie String 16))
     484definition assembly: assembly_program $\rightarrow$ option (list Byte $\times$ (BitVectorTrie String 16))
    488485\end{lstlisting}
    489486A single fetch-decode-execute cycle is performed by \texttt{execute\_1}:
     
    523520[ `ADD of acc * [ reg | direct | indirect | data ]
    524521...
    525 | `MOV of
    526    (acc * [ reg| direct | indirect | data ],
     522| `MOV of (acc * [ reg| direct | indirect | data ],
    527523   [ reg | indirect ] * [ acc | direct | data ],
    528524   direct * [ acc | reg | direct | indirect | data ],
     
    535531Here, \texttt{union6} is a disjoint union type, defined as follows:
    536532\begin{lstlisting}
    537 type ('a,'b,'c,'d,'e,'f) union6 =
    538   [ `U1 of 'a | ... | `U6 of 'f ]
     533type ('a,'b,'c,'d,'e,'f) union6 = [ `U1 of 'a | ... | `U6 of 'f ]
    539534\end{lstlisting}
    540535The types \texttt{union2}, \texttt{union3} and \texttt{union6} sufficed.
     
    566561  $\lambda$d: addressing_mode_tag. $\lambda$A: addressing_mode.
    567562match d with
    568 [ direct $\Rightarrow$
    569   match A with [ DIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ]
    570 | indirect $\Rightarrow$
    571   match A with [ INDIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ]
     563[ direct $\Rightarrow$ match A with [ DIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ]
     564| indirect $\Rightarrow$ match A with [ INDIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ]
    572565...
    573566\end{lstlisting}
     
    577570A \texttt{subaddressing\_mode} is an \emph{ad hoc} non-empty $\Sigma$-type of \texttt{addressing\_mode}s in a set of tags:
    578571\begin{lstlisting}[frame=single]
    579 record subaddressing_mode
    580   (n: nat)
    581   (l: Vector addressing_mode_tag (S n)): Type[0] :=
    582 {
     572record subaddressing_mode (n: nat) (l: Vector addressing_mode_tag (S n)): Type[0] := {
    583573  subaddressing_modeel :> addressing_mode;
    584   subaddressing_modein:
    585     bool_to_Prop (is_in $\ldots$ l subaddressing_modeel)
     574  subaddressing_modein: bool_to_Prop (is_in $\ldots$ l subaddressing_modeel)
    586575}.
    587576\end{lstlisting}
     
    589578\begin{lstlisting}[frame=single]
    590579inductive preinstruction (A: Type[0]): Type[0] ≝
    591   ADD: $\llbracket$acc_a$\rrbracket$ $\rightarrow$ $\llbracket$register;direct;indirect;data$\rrbracket$ $\rightarrow$
    592        preinstruction A
    593 | ADDC: $\llbracket$acc_a$\rrbracket$ $\rightarrow$ $\llbracket$register;direct;indirect;data$\rrbracket$ $\rightarrow$
    594         preinstruction A
     580  ADD: $\llbracket$acc_a$\rrbracket$ $\rightarrow$ $\llbracket$register;direct;indirect;data$\rrbracket$ $\rightarrow$ preinstruction A
     581| ADDC: $\llbracket$acc_a$\rrbracket$ $\rightarrow$ $\llbracket$register;direct;indirect;data$\rrbracket$ $\rightarrow$ preinstruction A
    595582...
    596583\end{lstlisting}
     
    656643type line =
    657644[ `P1 of byte | `P3 of byte
    658 | `SerialBuff of
    659    [ `Eight of byte
    660    | `Nine of BitVectors.bit * byte ]  ]
     645| `SerialBuff of [ `Eight of byte | `Nine of BitVectors.bit * byte ]  ]
     646
    661647type continuation =
    662 [`In of time * line *
    663   epsilon * continuation] option *
     648[`In of time * line * epsilon * continuation] option *
    664649[`Out of (time -> line -> time * continuation)]
    665650\end{lstlisting}
Note: See TracChangeset for help on using the changeset viewer.