Changeset 3649


Ignore:
Timestamp:
Mar 13, 2017, 6:01:45 PM (9 months ago)
Author:
mulligan
Message:

more work on related work from this afternoon

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

Legend:

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

    r3648 r3649  
    9696  publisher = {Intellect},
    9797  isbn = {978-1-84150-277-9}
     98}
     99
     100@Inbook{DalLago2012,
     101author="Dal Lago, Ugo",
     102editor="Bezhanishvili, Nick
     103and Goranko, Valentin",
     104title="A Short Introduction to Implicit Computational Complexity",
     105bookTitle="Lectures on Logic and Computation: ESSLLI 2010 Copenhagen, Denmark, August 2010, ESSLLI 2011, Ljubljana, Slovenia, August 2011, Selected Lecture Notes",
     106year="2012",
     107publisher="Springer Berlin Heidelberg",
     108address="Berlin, Heidelberg",
     109pages="89--109",
     110isbn="978-3-642-31485-8",
     111doi="10.1007/978-3-642-31485-8_3",
     112url="http://dx.doi.org/10.1007/978-3-642-31485-8_3"
     113}
     114
     115@misc { clang,
     116  url = {https://clang.llvm.org/},
     117  title = {The {clang} {C} language frontend for {LLVM}},
     118  note = {Accessed March 2017},
     119  year = {2017},
     120  key = {clang}
     121}
     122
     123@misc { gcc,
     124  url = {https://gcc.gnu.org/},
     125  title = {The {GNU} compiler collection},
     126  note = {Accessed March 2017},
     127  year = {2017},
     128  key = {gcc}
     129}
     130
     131@misc { icc,
     132  url = {https://software.intel.com/en-us/c-compilers},
     133  title = {The {Intel} {C} and {C++} compiler},
     134  note = {Accessed March 2017},
     135  year = {2017},
     136  key = {icc}
    98137}
    99138
  • Papers/jar-cerco-2017/conclusions.tex

    r3648 r3649  
    3030
    3131We believe that the work presented in this paper represents a general approach to structuring compilers for lifting cost models to the source-level.
    32 In particular, the CerCo verified C compiler itself is a lightly-optimising compiler for a large subset of the C programming language, and whilst not as aggressive in its optimisation passes as commercial and open-source C compilers, such as \texttt{gcc}, \texttt{clang}, or \texttt{icc}, the compiler is still a relatively substantial piece of software.
     32In particular, the CerCo verified C compiler itself is a lightly-optimising compiler for a large subset of the C programming language, and whilst not as aggressive in its optimisation passes as commercial and open-source C compilers, such as \texttt{gcc}~\cite{gcc}, \texttt{clang}~\cite{clang}, or \texttt{icc}~\cite{icc}, the compiler is still a relatively substantial piece of software.
    3333As a result, the application of the techniques described herein, first described with pen-and-paper proofs, to the full CerCo compiler is, in our view, already evidence of their scalability, and we see no reason why these techniques could not be applied to a more aggressively optimising compiler, given that none of our techniques are tied to any particular choice of intermediate language or set of optimisations.
    3434Further, the techniques that we have presented are not tied to any particular programming language, or to any one programming paradigm, and are in fact amenable to arbitrary imperative and functional programming languages.
     
    6464However, recent work on the CompCert verified C compiler has investigated the verification of loop-bound analysis, a subcomponent of wider WCET analyses for the Clight intermediate language~\cite{DBLP:conf/wcet/MaronezeBPP14}.
    6565Note that this work is related but orthogonal to the work presented in this paper: our cost annotations at the C source-level are \emph{parametric} in the number of iterations of loops appearing in the source code.
    66 Indeed, to obtain a final resource analysis using our toolchain, the user must manually bound loop iterations.\footnote{This is typical for embedded and safety- or mission-critical applications, where unrestricted looping and recursion are not permitted.  See for example rule 16.2 of MISRA C 2004, which prohibits recursive function calls entirely in safety-critical code, and Nasa JPL's programming guidelines, which states all loops must have a bounded number of iterations.} %cite
     66Indeed, to obtain a final resource analysis using our toolchain, the user must manually bound loop iterations.\footnote{This is typical for embedded and safety- or mission-critical applications, where unrestricted looping and recursion are not permitted.
     67See for example rule 16.2 of MISRA C 2004, which prohibits recursive function calls entirely in safety-critical code, and Nasa JPL's programming guidelines, which states all loops must have a bounded number of iterations.} %cite
    6768As a result, one could potentially imagine pairing the loop-bound analysis with our parametric cost model to reduce the amount of user interaction required when using it.
    6869
     
    7677Campbell also used a variant of this approach to predict stack space usage~\cite{bac-thesis08,bac-giveback08,bac-esop09}.
    7778
    78 % implicit computational complexity
     79Implicit Computational Complexity represents another related approach to bounding resource usage via types~\cite{DalLago2012}.
     80Here, a fragment of Linear Logic, or some other substructural logic, is taken as the type-language of a programming language, with a provable guarantee that typeable terms normalise to a value in some bounded (e.g. polynomial in the size of the term) number of reduction steps.
     81Note that complained to the concrete complexity measures dealt with in this work, bounding reduction steps is rather coarse-grained: one reduction step in the calculus may decompose into some non-constant number of primitive machine operations, when executed on physical hardware.
     82Indeed, the focus of Implicit Computational Complexity is not to capture \emph{concrete} resource usage of programs, but to provide a type-theoretic interpretation of complexity classes.
    7983
    8084Several program logics for reasoning about a program's resource consumption have been investigated in the literature.
     
    99103
    100104\paragraph{Verified compilation}
     105
     106As a verified compilation project, CerCo is also related to various other verified compilation projects.
     107
     108Perhaps the most closely related verified compiler to our own is the CompCert verified C compiler project~\cite{compcert}.
     109Indeed, the intermediate languages chosen into the CerCo verified C compiler are at least partially inspired by those implemented in the CompCert compiler.
     110Several differences between the two projects stand out.
     111Most importantly, the vanilla CompCert compiler does not consider the lifting of any cost model from machine code to the source-level, which we do.
    101112
    102113% CompCert, CompCertTSO, CakeML, C0, etc.
Note: See TracChangeset for help on using the changeset viewer.