source: Deliverables/D1.1/Presentations/management_and_overall-sacerdoti-presentation.tex @ 655

\documentclass{beamer}

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

\usepackage{amsfonts}
\usepackage{amsmath}
\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 Managemnt}
\date{March 11, 2011}

\setlength{\parskip}{1em}

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

\begin{document}

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

\section{Long, middle and short term objectives}

\begin{frame}
 \frametitle{The ICT of the future}
 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}
 Signals in this direction:

 \begin{itemize}
  \item Formal methods are more and more embraced in industry
  \item If total certification remains mostly unfeasible,
        techniques for pay-as-you-ride certification are reaching larger
        audiences\\
        (model checking, type systems, abstract interpretation, dependent
         types, \ldots)
  \item Larger varities of user-friendly tools for partial certifications\\
        (termination checkers, WCET analyzers, source code analyzers based
         on WP, \ldots)
  \item New open tools that integrate collaborating plug-ins to perform
        automatic or interactive analyses (e.g. Frama-C)
 \end{itemize}
\end{frame}

\begin{frame}
 \frametitle{The ICT of the future}
 Compiler = a tool to translates programs
  \alert{preserving something}\\~\\

 In our long-term vision:
 \begin{center}
 \alert{\Large A compiler maps triples specification-implementation-certificate
  to triples specification-implementation-certificate.}
 \end{center}

 Questions:
 \begin{enumerate}
  \item What properties are \alert{preserved} during compilation?
  \item What properties are \alert{affected} by the compilation strategy?
  \item To what extent can you trust your compiler in preserving those properties?
 \end{enumerate}
\end{frame}

\begin{frame}
 \frametitle{The ICT of the future}
 Preservation of properties during compilation:
 \begin{itemize}
  \item Extensional properties are easily specifiable and easily preserved
        during compilation, but \alert{only assuming infinite resources}
  \item Little is known even foundationally on the
        \alert{preservation of intensional properties}
        (e.g. use of space, time, energy)
  \item For sure \alert{compilation} (which is not compositional)
        \alert{affects the intensional properties}\\
        E.g. the cost of different occurrences of $x+1$ can be different
  \item Hence \alert{how} can you \alert{specify} intensional properties
        as a function of the compilation strategy?
 \end{itemize}
\end{frame}

\begin{frame}
 \frametitle{Long term theoretical objectives}
 \begin{enumerate}
  \item to study the \alert{specification} of intensional properties
        under \alert{realistic and precise cost models} induced by the
        compilation strategy
  \item to study \alert{preservation} of extensional and intensional
        properties (\alert{under finiteness assumption})
 \end{enumerate}

 Byproducts:
 \begin{enumerate}
  \item being able to prove the efficacity of optimizations
  \item being able to state completeness of compilation under
        finiteness assumptions
 \end{enumerate}
\end{frame}

\begin{frame}
 \frametitle{Long term practical objectives}
 \begin{enumerate}
  \item allow developers of \alert{(hard) real time systems} to comfortably
    prove meeting of deadline on \alert{high level languages} with the guarantee
    that they hold on the object code
  \item allow developers of \alert{embedded systems} to reason on
    \alert{resource consumption} on \alert{high level languages} with the same
     guarantee
  \item augment the \alert{precision of formal methods} for intensional
    properties on high level languages
  \item obtain a new generation of \alert{precise and fully trustable WCET}
    analyzers
 \end{enumerate}
\end{frame}

\begin{frame}
 \frametitle{Short term objectives}
 \begin{enumerate}
  \item develop a \alert{compiler} from
        \alert{$\approx\!\!$ C} to the \alert{MCS-51} microprocessor
        used for embedded systems
  \item have the compiler infer from the assembly code a \alert{precise cost
        model} for the source program
  \item \alert{certify} the compiler
  \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} automatically or interactively the generated proof obligations
   \end{itemize}
  \item lift the technique to a \alert{synchronous languaged} (e.g. Esterel)
        compiled via C
 \end{enumerate}
\end{frame}

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

\begin{frame}[fragile]
 \frametitle{Source code}
\begin{Verbatim}[commandchars=\\\{\}]
char search (char tab[], char size, char to_find) \{
  char low = 0, high = size-1, i;

  while (high >= low) \{
    i = (high+low) / 2;
    if (tab[i] == to_find) return i;

    if (tab[i] > to_find) high = i-1;

    if (tab[i] < to_find) low = i+1;

  \}

  return (-1);
\}
\end{Verbatim}
\end{frame}

\begin{frame}[fragile]
 \frametitle{Instrumented source code}
\begin{Verbatim}[commandchars=\\\{\}]
char search (char tab[], char size, char to_find) \{
  char low = 0, high = size-1, i;
  \alert{cost_incr(117);}
  while (high >= low) \{
    \alert{cost_incr(77);}
    i = (high+low) / 2;
    if (tab[i] == to_find) \{\alert{cost_incr(30);} return i;\}
    \alert{else cost_incr(103);}
    if (tab[i] > to_find) \{\alert{cost_incr(98);} high = i-1;\}
    \alert{else cost_incr(85);}
    if (tab[i] < to_find) \{\alert{cost_incr(98);} low = i+1;\}
    \alert{else cost_incr(88);}
  \}
  \alert{cost_incr(43);}
  return (-1);
\}
\end{Verbatim}
\end{frame}

\begin{frame}[fragile]
 \frametitle{Foreseen problems}
 \begin{itemize}
  \item The \alert{high level implicit control structures}
    (e.g. missing \texttt{else}) must be made explicit
  \item Additional \alert{low level control structures} must be made explicit\\
    (e.g. add low bytes; if overflow then add high bytes)\\
    Alternative: loss of precision
  \item The \alert{guards} of the low level control structures could be
    \alert{``unrelated''} to the high level data\\
    (e.g. if the carry bit is set then \ldots else \ldots)
  \item Optimizations can \alert{modify the control flow}\\
    (e.g. loop hoisting and unrolling)
  \item The cost can depend on the data manipulated (\alert{dependent annotations}) (e.g. shift, multiplication in simple microprocessors)
  \item Precise information on the source code required to avoid total
    alteration (e.g. comments)
 \end{itemize}
\end{frame}

\begin{frame}[fragile]
 \frametitle{Foreseen problems}
 Strategy in CerCo:
 \begin{enumerate}
  \item We consider \alert{simple optimizations} that do not alter the control
    flow (cfr. CompCert)\\
    The study of control flow altering optimizations left as optional
  \item Complex low level control flows \alert{encapsulated} in library
    functions (if possible) or else \alert{precision loss} (not required yet)
  \item \alert{Partial alteration of the source program} for justified reasons
    (e.g. explicit CFs) and for temporary ones (reusal of the CIL suite)\\
    \alert{To be refined in the next periods}
 \end{enumerate}
\end{frame}

\begin{frame}[fragile]
 \frametitle{Cost invariants: loose invariants}
{\small
\begin{Verbatim}[commandchars=\\\{\}]
char search (char tab[], char size, char to_find) \{
  char low = 0, high = size-1, i;
  cost_incr(117);
  \alert{/* @ label L}
     \alert{@ invariant cost <= at(cost,L) +}
      \alert{(77+103+98+88)*((at(high,L) - at(low,L))/(high - low))-1) */}
  while (high >= low) \{
    cost_incr(\alert{77});
    i = (high+low) / 2;
    if (tab[i] == to_find) \{cost_incr(\alert{30}); return i;\}
    else cost_incr(\alert{103});
    if (tab[i] > to_find) \{cost_incr(\alert{98}); high = i-1;\}
    else cost_incr(\alert{85});
    if (tab[i] < to_find) \{cost_incr(\alert{98}); low = i+1;\}
    else cost_incr(\alert{88});
  \}
  cost_incr(43);
  return (-1);
\}
\end{Verbatim}
}
\end{frame}

\begin{frame}[fragile]
 \frametitle{Cost invariants: precise invariants}
 When needed the \alert{user} can also state a precise invariant:
 \begin{Verbatim}[commandchars=\\\{\}]
 \alert{cost = at(cost,L) +}
   \alert{(77 + 103 + 98 + 85) * min(0,#iterations - 1) +}
   \alert{if tab[(high+low)/2] == to_find then 30 else 103 +}
   \alert{3 * #high_decremented}
 \end{Verbatim}
 where \verb+#high_decremented+ has a complex description.\\~\\

 The more precise the invariant, the more knowledge is required on the
 extensional semantics of the program.
\end{frame}

\begin{frame}[fragile]
 \frametitle{Proof obligations for costs}
 \alert{Proof obligations} are then generated from the cost invariants using standard
 techniques (e.g. Weakest Precondition generators for Hoare logic)\\~\\

 \begin{itemize}
  \item Can use off-the-shelf WP generators
  \item Ad-hoc tactics/proof strategies to handle the proof obligations will
        probably help
 \end{itemize}
\end{frame}

\begin{frame}
 \frametitle{Other cost obligations}
 The same technique applies to: space (stack, heap), energy, etc.\\~\\

 But
 \begin{center}
   \alert{\Large space constraints have an effect on the\\extensional semantics too}\end{center}

 Similarly
 \begin{center}
   \alert{\Large time constraints have an effect on the\\extensional semantics too when\\considering timers or I/O}\end{center}
\end{frame}

\begin{frame}
 \frametitle{Other cost obligations and embedded systems}
 In CerCo \alert{we have not committed} to other kinds of costs but time.\\~\\

 \alert{Embedded and reactive systems} could greatly benefit from space
 constraints and from time in presence of timers.\\~\\

 Compatibly with the project timing and effort required, we would like to
 experiment with other costs too.\\~\\

 Otherwise, this will be left to \alert{future work}.
\end{frame}

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

\section{Project context}

\begin{frame}
 \frametitle{Related work}
 \alert{Invariant generation} (also for termination)
 \begin{itemize}
  \item Automatic and assisted invariant discovery plays a \alert{central role}
    for the long term objectives
  \item Existing techniques are \alert{fully orthogonal} to CerCo: we provide
    a realistic and precise cost model to be used for cost invariants
  \item CerCo will \alert{guarantee} that the inferred intensional properties
    will \alert{carry over to assembly code}
 \end{itemize}
\end{frame}

\begin{frame}
 \frametitle{Related work}
 \alert{Worst Case Execution Time}
 \begin{itemize}
  \item Sophisticated techniques for computing approximate costs of
    object code programs
  \item Can target modern architectures (caches, pipelines, reordering of
    instructions, \ldots) using \alert{static (precise) or dinamic (empyrical)
    techniques}
  \item Main problem: \alert{how to relate} analysis on object code to the
    intermediate and source languages and \alert{how to trust} the results
  \item In CerCo:
   \begin{enumerate}
    \item Costs are tightly related by designing \alert{compilers} with this aim
     (cfr. wcc)
    \item WCET computations are \alert{certified}
    \item \alert{Interactivity} vs full automation
   \end{enumerate}
  \item CerCo will target only a simple architecture;\\ \alert{combination} with
    (dynamic?) WCET \alert{necessary}\\ in the long term
 \end{itemize}
\end{frame}

\begin{frame}
 \frametitle{Related work}
 \alert{Compiler certification and interactive theorem proving}
 \begin{itemize}
  \item A large and older litterature that focuses on academic examples
  \item Some impressive recent examples that targets realistic
    mildly optimizing compilers (e.g. CompCert, FR)
  \item On-going projects that targets more complex scenarios:
    intensional properties (CerCo, EU), whole software/hardware
    architectures (e.g. VeriSoft, DE), concurrent systems (USA), \ldots
 \end{itemize}
\end{frame}

\section{Project planning and achievements}

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

\begin{frame}
 \frametitle{Achievements (1st period)}
 Main theoretical achievements (D2.1):
 \begin{center}
  \alert{\Large a methodology for lifting in a provably correct way
    costs on the object code to costs in the source code}
 \end{center}~\\

 Main practical achievements (D2.2):
 \begin{center}
  \alert{\Large an untrusted compiler from C-Light to the MCS-51 microprocessor
   that lifts costs on the object code to costs in the source code}
 \end{center}
\end{frame}

\begin{frame}
 \frametitle{Achievements (1st period)}
 More in detail:
 \begin{enumerate}
  \item The methodology itself, with comparison with an alternative proposal.
    Main issues:
   \begin{enumerate}
    \item meaning of cost annotations
    \item method to prove them sound and precise
    \item compositionality
   \end{enumerate}
  \item Assessment of the methodology: formalization of a toy compiler in Coq
  \item First untrusted prototype from C-Light to Mips
  \item Full formalization in O'Caml of the MCS-51 ``environment'':
    \begin{enumerate}
     \item ALU
     \item UART, I/O lines, timers, interrupts
     \item an assembly language with pseudo-instructions + an assembler
     \item an Intel HEX parser/pretty printer
    \end{enumerate}
 \end{enumerate}
\end{frame}

\begin{frame}
 \frametitle{Achievements (1st period)}
 More in detail:
 \begin{enumerate}
  \item \alert{Partial} assessment of the MCS-51 O'Caml formalization
  \item Extension of C, the CIL suite and the CompCert memory model to the
    MCS-51 unorthogonal memory model (new type and pointer modifiers taken
    from SDCC)
  \item \alert{Partial} porting of the CerCo untrusted prototype to the
    MCS-51 and to the extended C
  \item Partial porting of the MCS-51 O'Caml formalization to Matita\\
        The formalization is directly executable
  \item Formalization in Matita of the extended C-Light version\\
        The formalization is directly executable
  \item \alert{Partial} assessment of the executable semantics by
        proving it equivalent to the CompCert one (up to extensions)
 \end{enumerate}
\end{frame}

\begin{frame}
 \frametitle{Assessment}
 Assessment level and strategies:
 \begin{enumerate}
  \item Untrusted CerCo compiler (D2.2, M1):\\
    the compiler will be fully certified; several bugs already found after
    the release of the deliverables
  \item MCS-51 model (D4.1):\\
    more thorough testing vs emulators and real processors is required;\\
    minor impact on the rest of the projects;\\
    the assembler will be certified (some bugs already found + unimplemented
    features)
  \item extended C semantics (D3.1):\\
    already proved to be equivalent to the CompCert one (up to extensions);\\
    we do not commit to support the planned extensions 
 \end{enumerate}
\end{frame}

\begin{frame}
 \frametitle{Deviations from DoW}
 Minor deviations from the DoW (no significant impact on the future schedule):
 \begin{enumerate}
  \item Late delivery of the deliverable related to the Web site and
    internal work-flow due to hardware problems. \alert{Solved}
  \item Compiler prototype D2.2 (M1):\\
    computation of realistic costs requires full integration with D4.1
    (not completed/tested at release time) \alert{Solved}
  \item MCS-51 memory model + C extensions:\\
    we did not foresee the need of MCS-51 specific extensions;\\
    they will be taken in account with low priority\\
    at the moment, only partially implemented in a branch of D2.2
    not ready for release. \alert{Under consideration}
 \end{enumerate}
\end{frame}

\begin{frame}
 \frametitle{Foreseen deviations from DoW}
\end{frame}

\end{document}