source: Deliverables/D1.1/Presentations/WP1-claudio.tex @ 2007

\documentclass{beamer}

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

\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{March 11, 2011}

\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}
 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 varieties of user-friendly tools for partial certifications\\
        (termination checkers, WCET analysers, source code analysers 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 optimisations
  \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}
    analysers
 \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 languages} (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 Optimisations 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 optimisations} that do not alter the control
    flow (cfr. CompCert)\\
    The study of control flow altering optimisations 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 dynamic (empirical)
    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 literature that focuses on \alert{academic examples}
  \item Some impressive recent examples that targets \alert{realistic
    mildly optimising compilers} (e.g. CompCert, FR)
  \item On-going projects that targets more \alert{complex scenarios}:
    intensional properties (CerCo, EU), whole software/hardware
    architectures (e.g. VeriSoft, DE), concurrent systems (USA),
    higher level languages, \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 \alert{methodology itself}, with comparison with an alternative proposal (D2.1).  Main issues:
   \begin{enumerate}
    \item meaning of cost annotations
    \item method to prove them sound and precise
    \item \alert{compositionality}
   \end{enumerate}
  \item Assessment of the methodology: formalisation of a \alert{toy compiler in Coq}
  \item First untrusted prototype from C-Light to Mips
  \item Full \alert{formalisation} in O'Caml of the \alert{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 formalisation
  \item \alert{Extension of C}, the CIL suite and the CompCert
    \alert{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 \alert{Partial porting} of the MCS-51 O'Caml formalisation to Matita\\
        The formalisation is directly executable
  \item \alert{Formalisation} in Matita of the \alert{extended C-Light version}\\
        The formalisation is directly \alert{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 \alert{fully certified};
    several bugs already found after
    the release of the deliverables
  \item MCS-51 model (D4.1):\\
    \alert{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 \alert{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}
 \alert{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}
 All sites have faced different hiring problems.\\~\\

  UNIBO (Project Coordinator).\\
   \alert{Personnel planned:} 1 post-doc (24m) + 1 RTD (non permanent researcher) 24m\\
   \alert{Personnel acquired:} 1 post-doc (24m)\\
   \alert{Cause:}
   Because of the reform of the Italian University it has not been possible
   to hire a RTD yet and it is unlikely to be possible to hire him soon.\\
   \alert{Solution:} in place of the RTD, we will acquire two post-docs
   (24m + 18m) that will start later then expected and will have a lower
   level of expertise. Both positions are still waiting for clarifications
   from the ministry or approval from the Corte dei Conti.\\
   \alert{Expected impact:} delivery of D4.2 (month 18) could\\
   be delayed with no impact on the next milestone\\
   (M2, month 24), potential impact on M3, month 36.
\end{frame}

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

\begin{frame}
 \frametitle{Foreseen deviations from DoW}
 All sites have faced different hiring problems.\\~\\

  UPD.\\
   \alert{Personnel planned:} 1 post-doc (12m) + 1 PhD student (36m) + master students\\
   \alert{Personnel acquired:} 1 post-doc (11m) + 1 PhD student (6m) + 2 master students\\
   \alert{Cause:}
    After 6 months of work the PhD student has decided to resign. 
    At this point, it is neither possible (incomplete funding) 
    nor desirable (bootstrapping period) to look for another PhD
    student.\\
   \alert{Solution:}
    The post-doc contract will be extended until October 2012
    to cover also the second and most of the third period.\\
   \alert{Expected impact:} no major expected impact.
\end{frame}

\begin{frame}
 \frametitle{Foreseen deviations from DoW}
 All sites have faced different hiring problems.\\~\\

  UEDIN.\\
   \alert{Personnel planned:} 1 lecturer (36m) + 1 post-doc (36m) + 1 PhD-student \\
   \alert{Personnel acquired:} 1 lecturer (14m) + Senior lecturer (24m) + 1 post-doc
   \alert{Cause:}
    Dr. Randy Pollack (former site leader) is moving to Harvard.
    He will be employed 90\% of his time there and 10\% on CerCo at UEDIN.
    Dr. Ian Stark is the new site leader (since 01 February).
    No student with appropriate background was found.\\
   \alert{Solution:}
    We plan to hire a post-doc during the later part of the project to
    compensate for the missing PhD student.\\
   \alert{Expected impact:} some trading of person-months between projects
    and reassignment of costs: an experienced researcher will be more expensive
    than a PhD student, but could reasonably expect to carry out the formal
    proof work in less time than a student.
\end{frame}

\section{Project management}

\begin{frame}
 \frametitle{The Project at a Glance}
 \begin{tabular}{ll}
 Title: & Certified Complexity \\
 Acronym: & CerCo \\
 Research Area: & ICT-2007.8.0 FET Open \\
 \alert{Number of Partners:} & \alert{3} \\
 Grant Agreement N. & 243881 (13/11/2009) \\
 %Proposal Contract N. & \\
 Oper. Commenc. Date: & 01/02/2010 \\ 
 \alert{Duration}: & \alert{36 months} \\
 Project Cost: & $\geq$ 1,520,000 \euro \\
 Budget: & ~~~~1,164,533 \euro \\
 Pre-Financing: & ~~~~~~~621,084 \euro \\
 \alert{Reporting Periods:} & \alert{1--12}, 13--24, 25--36 \\
 \end{tabular}
\end{frame}

\begin{frame}
 \frametitle{The Partnership at a Glance}
  \alert{UNIBO (ALMA Mater Studiorum, Universit\'a di Bologna)}\\
  79 m.m., 473,040 \euro, Coordinator\\

   \begin{itemize}
    \item Claudio Sacerdoti Coen (project leader)\\
          (Permanent Researcher)
    \item Michela Cozzi (project management team) (Administrative)
    \item Andrea Asperti (Full Professor)
    \item Dominic Mulligan (Post-Doc)
    \item Two Post-Doc to be hired
    \item PhD. Students: Wilmer Ricciotti
    \item Undergraduate/Master Students: Cosimo Arndt Oliboni
   \end{itemize}
\end{frame}

\begin{frame}
 \frametitle{The Partnership at a Glance}
  \alert{UPD (Universit\'e Paris Diderot - Paris VII)}\\ 66 m.m., 314,457 \euro\\
 \begin{itemize}
  \item Roberto Amadio (site leader) (Full Professor)
  \item Yann R\'egis-Gianas (Maitre de Conference)
  \item Nicolas Ayache (Post-Doc)
  \item Ronan Saillard (Internship + PhD student)
  \item Kayvan Memarian (Internship)
 \end{itemize}
\end{frame}

\begin{frame}
 \frametitle{The Partnership at a Glance}
  \alert{UEDIN (University of Edinburgh)}\\ 69 m.m., 377,036 \euro\\
 \begin{itemize}
  \item Ian Stark (site leader), (Senior Lecturer)
  \item Randy Pollack (former site leader), (Senior Research Fellow)
  \item Brian Campbell (Post-Doc)
  \item One Post-Doc to be hired
 \end{itemize}
\end{frame}

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

\begin{frame}
 \frametitle{Consortium structure}
 \includegraphics[height=8cm]{figs/management.pdf}
\end{frame}

\begin{frame}
 \frametitle{Financial management and coordination}
 During first period:
 \begin{enumerate}
  \item transmission \alert{pre-financing} to all beneficiaries
  \item \alert{providing} to partners detailed \alert{information} on consortium
    organisation and FP7 management rules during Kick Off
  \item \alert{collecting and checking} partner's \alert{financial information} for the
    First 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}
 \end{enumerate}
\end{frame}

\begin{frame}
 \frametitle{Consortium agreement}
 \begin{itemize}
  \item signed in \alert{January 2010}
  \item Intellectual Property Rights, Access Rights, roles,
    functioning and responsibilities of governing bodies, liability of the
    partners
 \end{itemize}
\end{frame}

\begin{frame}
 \frametitle{Periodic Meetings}
 Four project meetings during first period (two planned in the DoW):
 \begin{itemize}
  \item \alert{Kick-off, Bologna, February 2010.}\\
   coordination of research activities, planning of future work,
   financial and administrative organisation
  \item \alert{Project meeting, Edinburgh, July 2010.}\\
   Just after D2.1. Fixing more precise scheduling; first informal
   dissemination via co-location with FLOC
  \item \alert{Project meeting, Paris, September 2010.}\\
   Adoption of the MCS-51 target; discussion of the design of the costing
   compiler (D2.2), memory model (D4.1). Integration problems foreseen.
  \item \alert{Implementer's meeting, Bologna, January 2011}\\
   Addressing remaining integration problems regarding\\ D2.2, D3.1 and D4.1.
   Post-poning some integration\\ steps to Task 2.4 (second period).
 \end{itemize}
\end{frame}

\end{document}