Changeset 654 for Deliverables

Mar 9, 2011, 12:58:42 AM (10 years ago)

In progress

1 edited


  • Deliverables/D1.1/Presentations/management_and_overall-sacerdoti-presentation.tex

    r652 r654  
     26  \begin{frame}<beamer>
     27    \frametitle{Outline}
     28    \tableofcontents[currentsection]
     29  \end{frame}
     38\section{Long, middle and short term objectives}
     332\section{Project context}
     335 \frametitle{Related work}
     336 \alert{Invariant generation} (also for termination)
     337 \begin{itemize}
     338  \item Automatic and assisted invariant discovery plays a \alert{central role}
     339    for the long term objectives
     340  \item Existing techniques are \alert{fully orthogonal} to CerCo: we provide
     341    a realistic and precise cost model to be used for cost invariants
     342  \item CerCo will \alert{guarantee} that the inferred intensional properties
     343    will \alert{carry over to assembly code}
     344 \end{itemize}
     348 \frametitle{Related work}
     349 \alert{Worst Case Execution Time}
     350 \begin{itemize}
     351  \item Sophisticated techniques for computing approximate costs of
     352    object code programs
     353  \item Can target modern architectures (caches, pipelines, reordering of
     354    instructions, \ldots) using \alert{static (precise) or dinamic (empyrical)
     355    techniques}
     356  \item Main problem: \alert{how to relate} analysis on object code to the
     357    intermediate and source languages and \alert{how to trust} the results
     358  \item In CerCo:
     359   \begin{enumerate}
     360    \item Costs are tightly related by designing \alert{compilers} with this aim
     361     (cfr. wcc)
     362    \item WCET computations are \alert{certified}
     363    \item \alert{Interactivity} vs full automation
     364   \end{enumerate}
     365  \item CerCo will target only a simple architecture;\\ \alert{combination} with
     366    (dynamic?) WCET \alert{necessary}\\ in the long term
     367 \end{itemize}
     371 \frametitle{Related work}
     372 \alert{Compiler certification and interactive theorem proving}
     373 \begin{itemize}
     374  \item A large and older litterature that focuses on academic examples
     375  \item Some impressive recent examples that targets realistic
     376    mildly optimizing compilers (e.g. CompCert, FR)
     377  \item On-going projects that targets more complex scenarios:
     378    intensional properties (CerCo, EU), whole software/hardware
     379    architectures (e.g. VeriSoft, DE), concurrent systems (USA), \ldots
     380 \end{itemize}
     383\section{Project planning and achievements}
    323386 \includegraphics[height=8cm]{figs/pert.pdf}
     390 \frametitle{Achievements (1st period)}
     391 Main theoretical achievements (D2.1):
     392 \begin{center}
     393  \alert{\Large a methodology for lifting in a provably correct way
     394    costs on the object code to costs in the source code}
     395 \end{center}~\\
     397 Main practical achievements (D2.2):
     398 \begin{center}
     399  \alert{\Large an untrusted compiler from C-Light to the MCS-51 microprocessor
     400   that lifts costs on the object code to costs in the source code}
     401 \end{center}
     405 \frametitle{Achievements (1st period)}
     406 More in detail:
     407 \begin{enumerate}
     408  \item The methodology itself, with comparison with an alternative proposal.
     409    Main issues:
     410   \begin{enumerate}
     411    \item meaning of cost annotations
     412    \item method to prove them sound and precise
     413    \item compositionality
     414   \end{enumerate}
     415  \item Assessment of the methodology: formalization of a toy compiler in Coq
     416  \item First untrusted prototype from C-Light to Mips
     417  \item Full formalization in O'Caml of the MCS-51 ``environment'':
     418    \begin{enumerate}
     419     \item ALU
     420     \item UART, I/O lines, timers, interrupts
     421     \item an assembly language with pseudo-instructions + an assembler
     422     \item an Intel HEX parser/pretty printer
     423    \end{enumerate}
     424 \end{enumerate}
     428 \frametitle{Achievements (1st period)}
     429 More in detail:
     430 \begin{enumerate}
     431  \item \alert{Partial} assessment of the MCS-51 O'Caml formalization
     432  \item Extension of C, the CIL suite and the CompCert memory model to the
     433    MCS-51 unorthogonal memory model (new type and pointer modifiers taken
     434    from SDCC)
     435  \item \alert{Partial} porting of the CerCo untrusted prototype to the
     436    MCS-51 and to the extended C
     437  \item Partial porting of the MCS-51 O'Caml formalization to Matita\\
     438        The formalization is directly executable
     439  \item Formalization in Matita of the extended C-Light version\\
     440        The formalization is directly executable
     441  \item \alert{Partial} assessment of the executable semantics by
     442        proving it equivalent to the CompCert one (up to extensions)
     443 \end{enumerate}
     447 \frametitle{Assessment}
     448 Assessment level and strategies:
     449 \begin{enumerate}
     450  \item Untrusted CerCo compiler (D2.2, M1):\\
     451    the compiler will be fully certified; several bugs already found after
     452    the release of the deliverables
     453  \item MCS-51 model (D4.1):\\
     454    more thorough testing vs emulators and real processors is required;\\
     455    minor impact on the rest of the projects;\\
     456    the assembler will be certified (some bugs already found + unimplemented
     457    features)
     458  \item extended C semantics (D3.1):\\
     459    already proved to be equivalent to the CompCert one (up to extensions);\\
     460    we do not commit to support the planned extensions
     461 \end{enumerate}
     465 \frametitle{Deviations from DoW}
     466 Minor deviations from the DoW (no significant impact on the future schedule):
     467 \begin{enumerate}
     468  \item Late delivery of the deliverable related to the Web site and
     469    internal work-flow due to hardware problems. \alert{Solved}
     470  \item Compiler prototype D2.2 (M1):\\
     471    computation of realistic costs requires full integration with D4.1
     472    (not completed/tested at release time) \alert{Solved}
     473  \item MCS-51 memory model + C extensions:\\
     474    we did not foresee the need of MCS-51 specific extensions;\\
     475    they will be taken in account with low priority\\
     476    at the moment, only partially implemented in a branch of D2.2
     477    not ready for release. \alert{Under consideration}
     478 \end{enumerate}
     482 \frametitle{Foreseen deviations from DoW}
Note: See TracChangeset for help on using the changeset viewer.