Changeset 3642


Ignore:
Timestamp:
Mar 8, 2017, 4:24:40 PM (7 weeks ago)
Author:
mulligan
Message:

...

Location:
Papers/jar-cerco-2017
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Papers/jar-cerco-2017/cerco.bib

    r3632 r3642  
    210210  isbn      = {978-1-84150-176-5},
    211211}
     212
     213@article{DBLP:journals/corr/abs-1202-4905,
     214  author    = {Andrea Asperti and
     215               Wilmer Ricciotti and
     216               Claudio Sacerdoti Coen and
     217               Enrico Tassi},
     218  title     = {A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive
     219               Constructions},
     220  journal   = {Logical Methods in Computer Science},
     221  volume    = {8},
     222  number    = {1},
     223  year      = {2012},
     224  url       = {http://dx.doi.org/10.2168/LMCS-8(1:18)2012},
     225  doi       = {10.2168/LMCS-8(1:18)2012},
     226  timestamp = {Mon, 15 Oct 2012 13:17:50 +0200},
     227  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/corr/abs-1202-4905},
     228  bibsource = {dblp computer science bibliography, http://dblp.org}
     229}
     230
    212231
    213232@inproceedings{matita,
  • Papers/jar-cerco-2017/introduction.tex

    r3641 r3642  
    108108In this work, we have instantiated the CerCo approach with a cost model for the MCS-51 hardware that our prototype compiler targets.
    109109As this hardware is relatively simple, it admits a precise cost model, and this is reflected in our final theorem, which demonstrates that our high-level cost annotations are both accurate and precise.
    110 On more modern, exhibiting features such as caches, pipelines, and speculative execution, an exact cost model for time or space will be hard-to-impossible to define.
     110On more modern hardware, exhibiting features such as caches, pipelines, and speculative execution, an exact cost model for time or space will be hard-to-impossible to define.
    111111Instead, existing WCET analyses could be used, and then lifted to high-level annotations using our non-standard compiler architecture.
    112112
    113 We take it as an article of faith that software used to verify properties of programs must be as bug-free as possible.
     113We take it as an article of faith that software used to verify other software must itself be as bug-free as possible---preferably verified itself.
    114114One way to achieve this is to reduce the trusted code base of any tools used.
    115115Here, `trusted code base' refers to the corpus of code that must be trusted to believe that the analysis being carried out is accurate.
    116 The trusted code base of state-of-the-art WCET tools is significant: one needs to trust the control flow analyser, the linear programming libraries used, and also the formal models of the hardware under analysis.
     116The trusted code base of state-of-the-art static analysis tools, such as WCET analysers, is significant.
     117These are sophisticated, complex pieces of software that are built around a control flow analyser, linear programming libraries, and also detailed formal models of the hardware under analysis.
     118To trust a WCET tool, each of these subcomponents, along with their eventual combination, must all be trusted.
     119
    117120In CerCo we move the control flow analysis to the source code level, and we introduce a non-standard compiler.
    118 As this compiler architecture is completely novel, we wish to ensure that our implementation (and by extension, our entire approach) is correct.
    119 Therefore, to reduce the size of our trusted code base, we have implemented a prototype compiler and static analyser in an interactive theorem prover---the Matita interactive theorem prover, an implementation of the Calculus of Coinductive Constructions---which was used to certify that the costs added to the source code are indeed those incurred by the hardware.
     121As this compiler architecture is completely novel, we wish to ensure that our implementation (and by extension, our entire approach to lifting cost models) is correct.
     122Therefore, to reduce the size of our trusted code base, we have implemented a prototype compiler and static analyser in an interactive theorem prover---Matita~\cite{matita,asperti:user:2007}, an implementation of the Calculus of Coinductive Constructions---which was used to certify that the cost annotations supplementing the program's source code are indeed an accurate reflection of those incurred by the hardware.
    120123We have also implemented formal models of the hardware and of the high-level source-language in the interactive theorem prover.
    121124
     
    128131We now briefly introduce Matita, the interactive theorem prover that was used in CerCo to certify all proofs.
    129132
    130 Matita is an interactive theorem proving system based on a variant of the Calculus of Coinductive Constructions~\cite{asperti:user:2007}.
    131 The system features a full spectrum of dependent types and (co)inductive families, a system of coercions, a tactic-driven proof construction engine~\cite{sacerdoti-coen:tinycals:2007}, and paramodulation based automation~\cite{asperti:higher-order:2007}, all of which we exploit in the formalisation described herein.
     133Matita is an interactive theorem proving system based on a variant of the Calculus of Coinductive Constructions~\cite{matita,asperti:user:2007}.
     134The system features (co)inductive families of types, a system of coercions, a tactic-driven proof construction engine~\cite{sacerdoti-coen:tinycals:2007}, and paramodulation based automation~\cite{asperti:higher-order:2007}, all of which we exploit in the formalisation described herein.
    132135
    133136Matita's syntax is similar to the syntaxes of mainstream functional programming languages such as OCaml or Standard ML.
     
    139142Recursive functions are introduced with \texttt{let rec}.
    140143Mutually recursive functions are separated via the \texttt{and} keyword.
    141 Matita's termination checker ensures that all recursive functions are terminating before being admitted to maintain soundness of the system's logic.
     144Matita's termination checker ensures that all recursive functions are terminating before being admitted into the global environment, to maintain soundness.
    142145\item
    143146Matita has an infinite hierarchy of type universes.
    144147A single impredicative universe of types, \texttt{Prop}, exists at the base of this hierarchy.
    145 An infinite series of predicative universes, \texttt{Type[0]} : \texttt{Type[1]} : \texttt{Type[2]}, and so on and so forth, sits atop \texttt{Prop}.
     148An unbounded series of predicative universes, \texttt{Type[0]}, \texttt{Type[1]}, \texttt{Type[2]}, and so on and so forth, sits atop \texttt{Prop}.
     149One peculiarity of Matita is a user-customisable hierarchy of universes.
     150In our development, we work in a context where \texttt{Prop} is contained in \texttt{Type[0]}, \texttt{Type[0]} is contained in \texttt{Type[1]}, and so on.
    146151Matita, unlike Coq or Agda, implements no form of typical ambiguity or universe polymorphism, with explicit concrete universe levels being preferred instead.
    147152\item
     
    149154Constants \texttt{True} and \texttt{False} represent truth and falsity in \texttt{Prop} respectively.
    150155Two inductive families in \texttt{Prop} encode conjunction and disjunction---$\mathtt{P \wedge Q}$ and $\mathtt{P \vee Q}$ respectively.
    151 
    152156As is usual, implication and universal quantification are identified with the dependent function space ($\Pi$ types), whereas (constructive) existential quantification is encoded as a dependent sum (a $\Sigma$-type).
    153157We write $\All{x : \phi}\psi$ for the dependent function space, and abbreviate this as $\phi \rightarrow \psi$ when $x \not\in fv(\psi)$ as usual.
     
    161165\end{lstlisting}
    162166We call $P_i$ for $0 \leq i \leq n$ the \textbf{parameters} of \texttt{I} and $\phi_j$ for $0 \leq j \leq m$ the \textbf{indices} of \texttt{I}.
    163 Matita's positivity checker ensures that constructors have strictly-positive types before admitting an inductive family to maintain soundness of the system's logic.
     167Matita's positivity checker ensures that constructors have strictly-positive types before admitting a (co)inductive family of types into the global environment, to maintain soundness.
    164168\item
    165169Records are introduced with the \texttt{record} keyword.
     
    168172record R : Type[0] := { F1 : nat }.
    169173\end{lstlisting}
    170 may be thought of as syntactic sugar for a single-constructor inductive data type of the same name:
     174may be thought of as syntactic sugar for a single-constructor inductive type of the same name:
    171175\begin{lstlisting}[language=Grafite]
    172176inductive R : Type[0] :=
    173177  | mk_R : nat -> R.
    174178\end{lstlisting}
    175 A record field's type may depend on fields declared earlier in the record.
    176 
     179Types of later fields may depend on fields declared earlier in the record.
    177180Records may be decomposed with projections.
    178181Projections, one for each of field of a record, are registered in the global context.
    179182In the example record above, \texttt{F1} of type $R \rightarrow nat$ is registered as a field projection and $mk\_R$ of type $nat \rightarrow R$ is registered as a constructor.
    180 
    181183Record fields may also be marked as coercions.
    182184In the following example
     
    193195Terms may be freely omitted, allowing the user to write down partial types and terms.
    194196A question mark, \texttt{?}, denotes a single term that has been omitted by the user.
    195 Some omitted terms can be deduced by Matita's refinement system.
     197Some omitted terms can be deduced by Matita's refinement system~\cite{DBLP:journals/corr/abs-1202-4905}.
    196198Other, more complex goals arising from omitted terms may require user input to solve, in which case a proof obligation is opened for each term that cannot be deduced automatically.
    197 Three consecutive dots, \texttt{$\ldots$}, denote multiple terms or types that have been omitted.
    198 \item
    199 Data may be decomposed by pattern matching with a \texttt{match} expression.
     199Three consecutive dots, \texttt{$\ldots$}, denote a vector of terms or types that have been omitted, and need to be inferred.
     200\item
     201(Co)data may be decomposed by pattern matching with a \texttt{match} expression.
    200202We may fully annotate a \texttt{match} expression with its return type.
    201203This is especially useful when working with indexed families of types or with invariants, expressed as types, on functions.
     
    225227\subsection{Map of the paper}
    226228
    227 The rest of the paper is structured as follows.
    228 
    229 In section~\ref{sect.compiler.architecture}, we describe the architecture of the
    230 CerCo compiler, as well as the intermediate languages that it uses. We also
    231 describe the target hardware and its formal model.
    232 
    233 In section~\ref{sect.compiler.proof}, we describe the proof of correctness of
    234 the compiler in more detail. We explain our use of structured traces, the
    235 labelling approach, and discuss the assembler.
    236 
    237 In section~\ref{sect.formal.development}, we present data on the formal
    238 development.
    239 
    240 In section~\ref{sect.framac.plugin}, we discuss the Frama-C plugin, as well as
    241 some of the case studies we have performed to validate it.
    242 
    243 Finally, in section~\ref{sect.conclusions} we present conclusions, as well as
    244 related and future work.
     229The rest of the paper is structured as follows:
     230
     231In Section~\ref{sect.compiler.architecture}, we describe the architecture of the CerCo compiler.
     232We describe the compiler's intermediate languages, from CerCo C down to MCS-51 machine code, and their formal semantics.
     233We also describe the optimisations that the CerCo verified C compiler implements.
     234
     235In Section~\ref{sect.compiler.proof}, we describe the proof of correctness of the compiler in more detail.
     236We explain \emph{structured traces}, a technical device developed to complete the proof, and our labelling approach.
     237We further discuss the verification of our translation and optimisation passes for the intermediate languages, and discuss our verified assembler.
     238
     239In Section~\ref{sect.formal.development}, we present statistical data on the formal development, including line counts, and so on, and discuss remaining axioms in our proof of the compiler's correctness.
     240We also briefly discuss `lessons learnt' in the formal development of the CerCo verified C compiler.
     241
     242In Section~\ref{sect.framac.plugin}, we discuss the Frama-C plugin for certifying the concrete complexity of programs written in CerCo C.
     243We also present a case study, demonstrating the plugin in action.
     244
     245Finally, in Section~\ref{sect.conclusions} we conclude, discussing related and future work.
Note: See TracChangeset for help on using the changeset viewer.