Changeset 659 for Deliverables/D1.1


Ignore:
Timestamp:
Mar 9, 2011, 10:54:50 PM (9 years ago)
Author:
sacerdot
Message:

Draft version completed.

Location:
Deliverables/D1.1/Presentations
Files:
2 edited

Legend:

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

    r654 r659  
    372372 \alert{Compiler certification and interactive theorem proving}
    373373 \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:
     374  \item A large and older litterature that focuses on \alert{academic examples}
     375  \item Some impressive recent examples that targets \alert{realistic
     376    mildly optimizing compilers} (e.g. CompCert, FR)
     377  \item On-going projects that targets more \alert{complex scenarios}:
    378378    intensional properties (CerCo, EU), whole software/hardware
    379     architectures (e.g. VeriSoft, DE), concurrent systems (USA), \ldots
     379    architectures (e.g. VeriSoft, DE), concurrent systems (USA),
     380    higher level languages, \ldots
    380381 \end{itemize}
    381382\end{frame}
     
    406407 More in detail:
    407408 \begin{enumerate}
    408   \item The methodology itself, with comparison with an alternative proposal.
    409     Main issues:
     409  \item The \alert{methodology itself}, with comparison with an alternative proposal (D2.1).  Main issues:
    410410   \begin{enumerate}
    411411    \item meaning of cost annotations
    412412    \item method to prove them sound and precise
    413     \item compositionality
     413    \item \alert{compositionality}
    414414   \end{enumerate}
    415   \item Assessment of the methodology: formalization of a toy compiler in Coq
     415  \item Assessment of the methodology: formalization of a \alert{toy compiler in Coq}
    416416  \item First untrusted prototype from C-Light to Mips
    417   \item Full formalization in O'Caml of the MCS-51 ``environment'':
     417  \item Full \alert{formalization} in O'Caml of the \alert{MCS-51} ``environment'':
    418418    \begin{enumerate}
    419419     \item ALU
    420420     \item UART, I/O lines, timers, interrupts
    421      \item an assembly language with pseudo-instructions + an assembler
     421     \item an assembly language with pseudo-instructions +\\ an assembler
    422422     \item an Intel HEX parser/pretty printer
    423423    \end{enumerate}
     
    429429 More in detail:
    430430 \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
     431  \item \alert{Partial assessment} of the MCS-51 O'Caml formalization
     432  \item \alert{Extension of C}, the CIL suite and the CompCert
     433    \alert{memory model} to the MCS-51 unorthogonal memory model (new type and
     434    pointer modifiers taken from SDCC)
     435  \item \alert{Partial porting} of the CerCo untrusted prototype to the
    436436    MCS-51 and to the extended C
    437   \item Partial porting of the MCS-51 O'Caml formalization to Matita\\
     437  \item \alert{Partial porting} of the MCS-51 O'Caml formalization to Matita\\
    438438        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
     439  \item \alert{Formalization} in Matita of the \alert{extended C-Light version}\\
     440        The formalization is directly \alert{executable}
     441  \item \alert{Partial assessment} of the executable semantics by
    442442        proving it equivalent to the CompCert one (up to extensions)
    443443 \end{enumerate}
     
    449449 \begin{enumerate}
    450450  \item Untrusted CerCo compiler (D2.2, M1):\\
    451     the compiler will be fully certified; several bugs already found after
     451    the compiler will be \alert{fully certified};
     452    several bugs already found after
    452453    the release of the deliverables
    453454  \item MCS-51 model (D4.1):\\
    454     more thorough testing vs emulators and real processors is required;\\
     455    \alert{more thorough testing} vs emulators and real processors is
     456    required;\\
    455457    minor impact on the rest of the projects;\\
    456458    the assembler will be certified (some bugs already found + unimplemented
    457459    features)
    458460  \item extended C semantics (D3.1):\\
    459     already proved to be equivalent to the CompCert one (up to extensions);\\
     461    already \alert{proved to be equivalent} to the CompCert one
     462    (up to extensions);\\
    460463    we do not commit to support the planned extensions
    461464 \end{enumerate}
     
    464467\begin{frame}
    465468 \frametitle{Deviations from DoW}
    466  Minor deviations from the DoW (no significant impact on the future schedule):
     469 \alert{Minor deviations} from the DoW
     470 (no significant impact on the future schedule):
    467471 \begin{enumerate}
    468472  \item Late delivery of the deliverable related to the Web site and
     
    481485\begin{frame}
    482486 \frametitle{Foreseen deviations from DoW}
     487 All sites have faced different hiring problems.\\~\\
     488
     489  UNIBO (Project Coordinator).\\
     490   \alert{Personel planned:} 1 post-doc (24m) + 1 RTD (non permanent researcher) 24m\\
     491   \alert{Personel acquired:} 1 post-doc (24m)\\
     492   \alert{Cause:}
     493   Because of the reform of the Italian University it has not been possible
     494   to hire a RTD yet and it is unlikely to be possible to hire him soon.\\
     495   \alert{Solution:} in place of the RTD, we will acquire two post-docs
     496   (24m + 18m) that will start later then expected and will have a lower
     497   level of expertise. Both positions are still waiting for clarifications
     498   from the ministry or approval from the Corte dei Conti.\\
     499   \alert{Expected impact:} delivery of D4.2 (month 18) could\\
     500   be delayed with no impact on the next milestone\\
     501   (M2, month 24), potential impact on M3, month 36.
     502\end{frame}
     503
     504\begin{frame}
     505 \hspace{-5cm}
     506 \includegraphics[height=8cm]{figs/pert.pdf}
     507\end{frame}
     508
     509\begin{frame}
     510 \frametitle{Foreseen deviations from DoW}
     511 All sites have faced different hiring problems.\\~\\
     512
     513  UPD.\\
     514   \alert{Personel planned:} 1 post-doc (12m) + 1 PhD student (36m) + master students\\
     515   \alert{Personel acquired:} 1 post-doc (12m) + 1 phd student (6m) + 2 master students\\
     516   \alert{Cause:}
     517    After 6 months of work the PhD student has decided to resign.
     518    At this point, it is neither possible (incomplete funding)
     519    nor desirable (bootstrapping period) to look for another PhD
     520    student.\\
     521   \alert{Solution:}
     522    We plan --- if possible --- to extend as much as
     523    possible the post-doc to cover also the second and/or third period.\\
     524   \alert{Expected impact:} no major expected impact.
     525\end{frame}
     526
     527\begin{frame}
     528 \frametitle{Foreseen deviations from DoW}
     529 All sites have faced different hiring problems.\\~\\
     530
     531  UEDIN.\\
     532   \alert{Personel planned:} 1 lecturer (36m) + 1 post-doc (36m) + 1 phd-student \\
     533   \alert{Personel acquired:} 1 lecturer (14m) + Senior lecturer (24m) + 1 post-doc
     534   \alert{Cause:}
     535    Dr. Randy Pollack (former site leader) is moving to Harvard.
     536    He will be employed 90\% of his time there and 10\% on CerCo at UEDIN.
     537    Dr. Ian Stark is the new site leader (since 01 February).
     538    No student with appropriate background was found.\\
     539   \alert{Solution:}
     540    We plan to hire a post-doc during the later part of the project to
     541    compensate for the missing PhD student.\\
     542   \alert{Expected impact:} some trading of person-months between projects
     543    and reassignment of costs: an experienced researcher will be more expensive
     544    than a PhD student, but could reasonably expect to carry out the formal
     545    proof work in less time than a student.
    483546\end{frame}
    484547
Note: See TracChangeset for help on using the changeset viewer.