source: Deliverables/D1.3/Presentations/WP1-claudio.tex @ 3534

\documentclass{beamer}

\usetheme{Frankfurt}
\logo{\includegraphics[height=1.0cm]{fetopen.png}}

\usepackage{wasysym}
\usepackage{amsfonts}
\usepackage{amsmath}
\usepackage{eurosym}
\usepackage{amssymb}
\usepackage[english]{babel}
\usepackage{color}
\usepackage[utf8x]{inputenc}
\usepackage{listings}
\usepackage{stmaryrd}
\usepackage{fancyvrb}
% \usepackage{microtype}

\author{Claudio Sacerdoti Coen}
\title{Certified Complexity (CerCo)\\
       Overall Presentation and Project Management}
\date{May 16, 2013}

\setlength{\parskip}{1em}

\AtBeginSection[]
{
  \begin{frame}<beamer>
    \frametitle{Outline}
    \tableofcontents[currentsection]
  \end{frame}
}

\begin{document}

\begin{frame}
\maketitle
\end{frame}

\begin{frame}
  \frametitle{Outline}
  \tableofcontents
\end{frame}

\section{Long, middle and short term objectives}

\begin{frame}
 \frametitle{The ICT of the future: Programs}
 We envision a (long term) future where formal methods will be pervasive:
 \begin{center}
   \alert{\Large Most programs will be (partially) specified and certified}
 \end{center}

 The very same definition of ``program'' will change:
 \begin{center}
  \alert{\Large A program will be a triple made of a specification,
  an implementation and a proof certificate}
 \end{center}

 Cfr: Proof Carrying Code (PCC)
\end{frame}

\begin{frame}
 \frametitle{The ICT of the future: the ITP point of view}
 There is always a trade off between expressivity (precision) and
 automation (partiality, abstraction).\\~\\

 Interactive theorem proving perspective:
   \alert{\Large
   \begin{itemize}
    \item Maximal expressivity (precision) in specification
    \item Interactive proofs
    \item Abstraction, loss of precision as special cases of specification
    \item Automation as special cases of interaction
   \end{itemize}
   }
\end{frame}

\begin{frame}
 \frametitle{The ICT of the future: Compilation}
 In our long-term vision:
 \begin{center}
 \alert{\Large A compiler maps triples specification-implementation-certificate
  to triples specification-implementation-certificate.}
 \end{center}

 What is investigated in CerCo:
 \begin{center}
 \alert{\Large Inclusion of intensional (non functional) properties into the
  specification to enable high level but precise reasoning.}
 \end{center}
\end{frame}

\begin{frame}
 \frametitle{The ICT of the future: Difficulties}
 Non functional properties (time, space, energy) are affected by:

 \begin{itemize}
  \item \alert{The compilation process} (which is not compositional)\\
        E.g. the cost of different high level occurrences of the same
        instruction is different.\\
        E.g. aggressive optimizations that change the control flow
  \item \alert{Hardware status} (caches, pipelines, branch prediction unit)
 \end{itemize}

 Questions and trade-offs:
 \begin{itemize}
  \item How much \alert{precision} can be achieved?
  \item How \alert{complex} are precise cost models for advanced compilation
        strategies and/or modern hardware?
  \item How much complexity can be tamed by \alert{abstraction}\\
        and automation at the source code level?
 \end{itemize}
\end{frame}

\begin{frame}
 \frametitle{The ICT of the future: Coping with the difficulties}

 In the project timeframe:

 \alert{We started with a simple scenario:}
 \begin{itemize}
  \item Conventional compilation model without changes to the control flow
  \item Deterministic widely deployed hardware model (no caching, pipelining)
 \end{itemize}

 \alert{We provided a formal certification of preservation of the
        non functional properties, modulo functional correctness}\\~\\

 \alert{We have started to scale to most complex scenarios\\
        (without certification).}\\~\\
\end{frame}

\begin{frame}
 \frametitle{Short term objectives (achievements)}
 \begin{enumerate}
  \item develop a \alert{compiler} from
        \alert{$\approx\!\!$ C} to \alert{MCS-51} processor
        (1st period)
  \item have the compiler infer from the assembly code a \alert{precise cost
        model} for the source program (1st period)
  \item \alert{certify} the preservation of non functional properties
        by the compiler (3rd period, open proof obligations for
        functional properties)
  \item embed the compiler in a \alert{prototypical environment} for
   \begin{itemize}
    \item stating \alert{cost invariants} based on the inferred cost model
    \item computing \alert{proof obligations}
    \item \alert{proving} generated obligations automatically or interactively
   \end{itemize}
   (2nd period and 3rd period)
  \item lift the technique to a \alert{synchronous language}
        (2nd period)
  \item \alert{Scale} the approach to \alert{more complex scenarios}
        (loop optimizations in 2nd period, investigations on modern hardware
         in 3rd period)
 \end{enumerate}
\end{frame}

\begin{frame}
 \frametitle{CerCo interaction diagram}
 \includegraphics[height=8cm]{figs/interaction_diagram.pdf}
\end{frame}

\begin{frame}
 \frametitle{Case study interaction diagram}
 \includegraphics[height=7cm]{figs/case_study_diagram.pdf}
\end{frame}

\section{State at the end of second period}

\begin{frame}
 \frametitle{Achievements (2nd period)}
 Main theoretical achievements (D2.1):
 \begin{center}
  \alert{A methodology (basic labelling approach) for lifting in a provably correct way costs on the object code to costs in the source code}\\
 \end{center}

 \begin{itemize}
  \item Scaled to dependent labelling to cover optimizations that do not
        preserve the control flow (D5.1)
  \item Applied to imperative and functional languages (D5.1)
  \item \alert{The proof did not cover function calls}
 \end{itemize}
\end{frame}

\begin{frame}
 \frametitle{Achievements (2nd period)}

 Main practical achievements (1/2):
  \alert{\begin{enumerate}
   \item An untrusted compiler from C-Light to the MCS-51 processor
   that implements the methodology (D2.2), also extended with
   loop optimizations (D5.1)\\
   \item Its formalization in Matita (D3.2, D4.2)\\
   \item Formalized executable semantics for source, target and intermediate
         languages (D3.1, D3.3, D4.1, D4.3)
  \end{enumerate}}

 \begin{itemize}
  \item The code was not extracted
  \item Not completely executable because of calls to untrusted code
        (cfr. translation validation, but also parsing/pretty printing)
  \item Code correct, not necessarily proof friendly
 \end{itemize}
\end{frame}

\begin{frame}
 \frametitle{Achievements (1st period)}

 Main practical achievements (2/2):

 \begin{center}
  \alert{Implementation for the Frama-C platform of a cost invariant
         synthesizer based on the CerCo's compiler (D5.1)}
 \end{center}

 \begin{itemize}
  \item Considered only simple cases
  \item Proof obligations produced by Jessie for the Why tool
        (Why3 in development, Frama-C under significant rewriting too)
 \end{itemize}
\end{frame}

\begin{frame}
 \hspace{-5.5cm}\includegraphics[height=8cm]{figs/pert.pdf}
\end{frame}

\begin{frame}
 \frametitle{Recommendations from the reviewers}
  ``The consortium should concentrate on positioning the project with
    respect to the state of the art which requires a detailed literature
    survey. In particular, the consortium should clearly formulate what
    distinguishes the project from existing work and which results are
    clear improvements.''

  \begin{itemize}
   \item We got in touch with \alert{other EU projects} active in the area of WCET,
         in particular EMBounded, PROARTIS, TACLe, PARMERASA, T-CREST, REMS.
   \item Direct contacts during the \alert{CerCo events}
   \item It \alert{really helped} in understanding what are the relevant novelties,
         the possible application scenarios and the weaknesses
         from the engineering perspective
   \item More details in D1.4 and the \alert{final presentation}
  \end{itemize}
\end{frame}

\begin{frame}
 \frametitle{Recommendations from the reviewers}
 ``The consortium should as soon as possible start with the verification of
   the compiler.'' ``The reviewers are worried that the whole verification tasks
   cannot be successfully completed by the end of the third project period.''

  \begin{itemize}
   \item The formal proof for the While language (1st period) was \alert{misleading}:
    function calls introduce a \alert{much larger set of novel intensional invariants}
   \item Moreover, the invariants are no longer expressed in terms of static
         code $\Rightarrow$ complete redesign of the proof strategy
   \item Had to consider \alert{stack space} too
   \item \alert{Contingency plan}: focus on the \alert{novel parts}
         (preservation of non functional properties), also exploiting the
         \alert{uniform representation of backend languages}
   \item Proof of preservation of costs \alert{completed up to} proofs\\
         of preservation of functional properties
  \end{itemize}
\end{frame}

\begin{frame}
 \frametitle{Recommendations from the reviewers}
 ``The consortium should develop a code extractor for MATITA which allows
obtaining executable code from specifications s.t. an executable
version of the trusted CerCo compiler can be automatically generated. This
extraction will be crucial to apply the CerCo approach to practical case studies
and to present it to industry.''

 \vspace{-0.25cm}
 \begin{itemize}
  \item \alert{Done}
  \item Many issues faced on the \alert{quality of the extracted code}
        (e.g. because of dependent types) (D5.2)
  \item \alert{Very nice example of very weakly typed extracted code}:
        opens several nice research directions
   \begin{itemize}
    \item Targeting OCaml's new \alert{first class modules} to capture $\Sigma$-types
    \item Targeting \alert{GADTs} to capture most dependent types
    \item A new technique to represent \alert{polymorphic variants} and
          \alert{extensible records} (had to be presented at TYPES'13)
    \item Targeting GHC \alert{$F_\omega$-like} language (working prototype,\\
          does not accept all programs, much harder than expected)
   \end{itemize}
 \end{itemize}
\end{frame}

\begin{frame}
 \frametitle{Recommendations from the reviewers}
 ``The consortium should concentrate on further developing and publishing
the dependent labelling approach. In particular, the approach should be
extended to further compiler optimizations, apart from loop peeling and
hoisting, and be applied to more modern processor architectures, eventually
aiming at multi-level caches and pipelines.''

 \begin{itemize}
  \item Dependent labelling \alert{published} at QAPL (journal version in preparation)
  \item One Post-Doc hired by UNIBO to work on \alert{application of dependent
        labelling to history sensitive hardware components} (pipelines, caches)
  \item Outcome in my next talk
 \end{itemize}
\end{frame}

\begin{frame}
 \frametitle{Recommendations from the reviewers}
 The reviewers required a revision of some deliverables and a few addenda.\\~\\

 The new versions and addenda were submitted to the EU as expected.
\end{frame}

\section{Project planning and achievements}

\begin{frame}
 \hspace{-5.5cm}\includegraphics[height=8cm]{figs/pert.pdf}
\end{frame}

\begin{frame}
 \frametitle{Achievements (3rd period) (WP3/WP4 talks)}
 From the \alert{formalized CerCo compiler} (2nd period)\\
  ~~~ - untrusted code\\
  ~~~ - not optimized for proving\\
  ~~~ - with axiomatized fixpoint computer and\\
  ~~~~~ graph colouring algorithm\\
  ~~~ - with formalized semantics for intermediate languages\\~\\
 to the \alert{trusted CerCo compiler} (3rd period) (WP5 talk)\\
  ~~~ - \alert{extracted code} integrated with untrusted code\\
  ~~~~~ from the untrusted prototype\\
  ~~~ - preservation of costs (time + \alert{stack space}) \alert{certified}\\
  ~~~~~ modulo preservation of functional properties
\end{frame}

\begin{frame}
 \frametitle{Achievements (3rd period) (WP5 talk)}
 From the \alert{untrusted CerCo prototype} (2nd period)\\
 ~~~ - untrusted compiler +\\
 ~~~~~ plug-in for Frama-C + Jessie + Why\\~\\
 to the \alert{trusted CerCo prototype} (3rd period)\\
 ~~~ - trusted/untrusted compiler +\\
 ~~~~~ plug-in for \alert{experimental Frama-C + Jessie + Why3}\\
 ~~~ - code simplification, \alert{better coverage}, integration with\\
 ~~~~~ \alert{separation logic} to cover arrays\\
 ~~~ - \alert{fine tuning of the generated invariants} to match\\
 ~~~~~ the automatic provers expertises\\
 ~~~ - a simplified interface for \alert{casual users}\\
 ~~~ - testing\\
 ~~~ - Debian packages + \alert{Live CD} for dissemination
\end{frame}

\begin{frame}
 \frametitle{Achievements (3rd period) (second WP4 talk)}
 \alert{Enlarging the scope} of CerCo techniques\\
 ~~~ - application of the \alert{dependent labelling approach} to cover\\
 ~~~~~ certain cost models that capture \alert{parametricity} of the cost\\
 ~~~~~ on the \alert{internal state of hardware} components that is\\
 ~~~~~ \alert{history dependent}\\
 ~~~ - sufficient to deal with pipelines (further research required)\\
 ~~~ - caches still problematic: towards \alert{probabilistic static analysis}?
\end{frame}

\begin{frame}
 \frametitle{Other activities (3rd period) (WP6 talk)}
 Organization of CerCo events targeted to potential industrial stakeholders
 and the academic community.
\end{frame}

\begin{frame}
 \frametitle{Assessment}
 Assessment level and strategies:
 \begin{enumerate}
  \item Trusted CerCo compiler encoding: (D3.4/D4.4):\\
    - extracted code \alert{tested};\\
    - partially \alert{certified} using Matita\\
  \item Trusted CerCo prototype (D5.2, D6.3, M3):\\
    - tested (methodology + code) in the \alert{case study} (D5.3);\\
    - tested on library of cryptographic functions (D6.3)\\
  \item Case study: analysis of synchronous code (D5.3):\\
   - \alert{self testing code} checks correctness and precision\\
   - tested on examples
 \end{enumerate}
\end{frame}

\begin{frame}
 \frametitle{Deviations from DoW}
 \alert{Minor deviations} from the DoW
 (no significant impact on the schedule):
 \begin{enumerate}
  \item At month 28: submission of the
    addenda required by the reviewers. \alert{Done}
  \item Late delivery of D5.3 (at end of project, planned at 36).\\
    Most job completed during the 2nd period, we needed to test it again
    on the last version of the trusted compiler.
  \item Late delivery of D6.6 (at end of project, planned
    at 33).\\
    The source code of the Debian packages and the infrastructure for the
    Live CD were ready on time, but the extracted code came later and was
    changing because of adjustments to the proofs.
 \end{enumerate}
\end{frame}

\begin{frame}
 \frametitle{Deviations from DoW}
 \alert{Major deviations} from the DoW
 \begin{enumerate}
  \item DoW amended for administrative issues and to extend the length of
        the projects by two months 
  \item Research on handling history sensitive hardware in response to
        reviewers.\\
    \alert{No impact on the schedule, work done by additional Post-Doc.}
  \item Bring forward work on D5.3 from the third to the second period.\\
    Enabled by replacement of PhD student by Post-Doc in Paris
  \item Compared to the formal proof for the Why language, the one for C
        revealed a \alert{much larger set of intensional invariants}
        to be preserved; our \alert{contingency plan} dictated that we focused
        on the aspects that
        are novel of our approach. The proof was finally \alert{completed up to
        proofs of functional correctness} already covered by existing projects.
 \end{enumerate}
\end{frame}

\section{Project management}

\begin{frame}
 \frametitle{Management activities}
 Management WP1:
 \begin{enumerate}
  \item \alert{coordinate and supervise} activities to be
    carried out
  \item carry out the overall \alert{administrative and
    financial management} of the project
  \item manage \alert{contacts with the European Commission}
  \item \alert{monitor quality and timing} of project deliverables
  \item establish effective internal and external
        \alert{communication procedures}
 \end{enumerate}
\end{frame}

\begin{frame}
 \frametitle{Financial management and coordination}
 During second period:
 \begin{enumerate}
  \item \alert{amend} the DoW for administrative reasons (organizational changes
        in UNIBO) and to \alert{extend the duration to 38 months}
  \item transmission \alert{pre-financing} to all beneficiaries
  \item \alert{collecting and checking} partner's \alert{financial information} for the
    Second Progress Report
  \item \alert{submission of financial statement} through NEF system (in progress)
  \item gathering all necessary information and submission of \alert{management
   reports, activity reports and deliverables}
  \item two sites (UNIBO and UEDIN) are undergoing the \alert{financial
        auditing}
 \end{enumerate}
\end{frame}

\begin{frame}
 \frametitle{Periodic Meetings}
 Two project meetings and two short meetings during 3rd period
 (one planned in DoW):
 \begin{itemize}
  \item Short project meeting, Paris, March 2012.\\
   %Planning; review of decisions taken during implementor's meeting, discussion on the proof strategy and on the actions to be taken as an answer to the reviewer's recommendations.
  \item Short project meeting, Tallin, March 2012.\\
   At ETAPS, negotiation of the CerCo event at next ETAPS
   %(for dissemination and to establish co-operation). Review of deliverables due at month 18. Invited speaker from WCET community.
  \item Project meeting, Bologna, May 2012\\
   %Discussion of issues found in the global proof strategy; introduction of the notion of structured traces and re-planning of the global proof strategy. Integration problems\\ addressed.
  \item Implementer's meeting, Edinburgh, August 2012\\
 \end{itemize}
\end{frame}

\end{document}