Changeset 674 for Deliverables/D1.1


Ignore:
Timestamp:
Mar 10, 2011, 4:19:09 PM (9 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D1.1/Presentations/WP1-claudio.tex

    r665 r674  
    1818\author{Claudio Sacerdoti Coen}
    1919\title{Certified Complexity (CerCo)\\
    20        Overall Presentation and Project Managemnt}
     20       Overall Presentation and Project Management}
    2121\date{March 11, 2011}
    2222
     
    7171        (model checking, type systems, abstract interpretation, dependent
    7272         types, \ldots)
    73   \item Larger varities of user-friendly tools for partial certifications\\
    74         (termination checkers, WCET analyzers, source code analyzers based
     73  \item Larger varieties of user-friendly tools for partial certifications\\
     74        (termination checkers, WCET analysers, source code analysers based
    7575         on WP, \ldots)
    7676  \item New open tools that integrate collaborating plug-ins to perform
     
    127127 Byproducts:
    128128 \begin{enumerate}
    129   \item being able to prove the efficacity of optimizations
     129  \item being able to prove the efficacity of optimisations
    130130  \item being able to state completeness of compilation under
    131131        finiteness assumptions
     
    145145    properties on high level languages
    146146  \item obtain a new generation of \alert{precise and fully trustable WCET}
    147     analyzers
     147    analysers
    148148 \end{enumerate}
    149149\end{frame}
     
    164164    \item \alert{proving} automatically or interactively the generated proof obligations
    165165   \end{itemize}
    166   \item lift the technique to a \alert{synchronous languaged} (e.g. Esterel)
     166  \item lift the technique to a \alert{synchronous languages} (e.g. Esterel)
    167167        compiled via C
    168168 \end{enumerate}
     
    228228    \alert{``unrelated''} to the high level data\\
    229229    (e.g. if the carry bit is set then \ldots else \ldots)
    230   \item Optimizations can \alert{modify the control flow}\\
     230  \item Optimisations can \alert{modify the control flow}\\
    231231    (e.g. loop hoisting and unrolling)
    232232  \item The cost can depend on the data manipulated (\alert{dependent annotations}) (e.g. shift, multiplication in simple microprocessors)
     
    240240 Strategy in CerCo:
    241241 \begin{enumerate}
    242   \item We consider \alert{simple optimizations} that do not alter the control
     242  \item We consider \alert{simple optimisations} that do not alter the control
    243243    flow (cfr. CompCert)\\
    244     The study of control flow altering optimizations left as optional
     244    The study of control flow altering optimisations left as optional
    245245  \item Complex low level control flows \alert{encapsulated} in library
    246246    functions (if possible) or else \alert{precision loss} (not required yet)
     
    358358    object code programs
    359359  \item Can target modern architectures (caches, pipelines, reordering of
    360     instructions, \ldots) using \alert{static (precise) or dinamic (empyrical)
     360    instructions, \ldots) using \alert{static (precise) or dynamic (empirical)
    361361    techniques}
    362362  \item Main problem: \alert{how to relate} analysis on object code to the
     
    378378 \alert{Compiler certification and interactive theorem proving}
    379379 \begin{itemize}
    380   \item A large and older litterature that focuses on \alert{academic examples}
     380  \item A large and older literature that focuses on \alert{academic examples}
    381381  \item Some impressive recent examples that targets \alert{realistic
    382     mildly optimizing compilers} (e.g. CompCert, FR)
     382    mildly optimising compilers} (e.g. CompCert, FR)
    383383  \item On-going projects that targets more \alert{complex scenarios}:
    384384    intensional properties (CerCo, EU), whole software/hardware
     
    419419    \item \alert{compositionality}
    420420   \end{enumerate}
    421   \item Assessment of the methodology: formalization of a \alert{toy compiler in Coq}
     421  \item Assessment of the methodology: formalisation of a \alert{toy compiler in Coq}
    422422  \item First untrusted prototype from C-Light to Mips
    423   \item Full \alert{formalization} in O'Caml of the \alert{MCS-51} ``environment'':
     423  \item Full \alert{formalisation} in O'Caml of the \alert{MCS-51} ``environment'':
    424424    \begin{enumerate}
    425425     \item ALU
     
    435435 More in detail:
    436436 \begin{enumerate}
    437   \item \alert{Partial assessment} of the MCS-51 O'Caml formalization
     437  \item \alert{Partial assessment} of the MCS-51 O'Caml formalisation
    438438  \item \alert{Extension of C}, the CIL suite and the CompCert
    439439    \alert{memory model} to the MCS-51 unorthogonal memory model (new type and
     
    441441  \item \alert{Partial porting} of the CerCo untrusted prototype to the
    442442    MCS-51 and to the extended C
    443   \item \alert{Partial porting} of the MCS-51 O'Caml formalization to Matita\\
    444         The formalization is directly executable
    445   \item \alert{Formalization} in Matita of the \alert{extended C-Light version}\\
    446         The formalization is directly \alert{executable}
     443  \item \alert{Partial porting} of the MCS-51 O'Caml formalisation to Matita\\
     444        The formalisation is directly executable
     445  \item \alert{Formalisation} in Matita of the \alert{extended C-Light version}\\
     446        The formalisation is directly \alert{executable}
    447447  \item \alert{Partial assessment} of the executable semantics by
    448448        proving it equivalent to the CompCert one (up to extensions)
     
    494494
    495495  UNIBO (Project Coordinator).\\
    496    \alert{Personel planned:} 1 post-doc (24m) + 1 RTD (non permanent researcher) 24m\\
    497    \alert{Personel acquired:} 1 post-doc (24m)\\
     496   \alert{Personnel planned:} 1 post-doc (24m) + 1 RTD (non permanent researcher) 24m\\
     497   \alert{Personnel acquired:} 1 post-doc (24m)\\
    498498   \alert{Cause:}
    499499   Because of the reform of the Italian University it has not been possible
     
    518518
    519519  UPD.\\
    520    \alert{Personel planned:} 1 post-doc (12m) + 1 PhD student (36m) + master students\\
    521    \alert{Personel acquired:} 1 post-doc (12m) + 1 phd student (6m) + 2 master students\\
     520   \alert{Personnel planned:} 1 post-doc (12m) + 1 PhD student (36m) + master students\\
     521   \alert{Personnel acquired:} 1 post-doc (12m) + 1 PhD student (6m) + 2 master students\\
    522522   \alert{Cause:}
    523523    After 6 months of work the PhD student has decided to resign.
     
    536536
    537537  UEDIN.\\
    538    \alert{Personel planned:} 1 lecturer (36m) + 1 post-doc (36m) + 1 phd-student \\
    539    \alert{Personel acquired:} 1 lecturer (14m) + Senior lecturer (24m) + 1 post-doc
     538   \alert{Personnel planned:} 1 lecturer (36m) + 1 post-doc (36m) + 1 PhD-student \\
     539   \alert{Personnel acquired:} 1 lecturer (14m) + Senior lecturer (24m) + 1 post-doc
    540540   \alert{Cause:}
    541541    Dr. Randy Pollack (former site leader) is moving to Harvard.
     
    633633
    634634\begin{frame}
    635  \frametitle{Finantial management and coordination}
     635 \frametitle{Financial management and coordination}
    636636 During first period:
    637637 \begin{enumerate}
    638638  \item transmission \alert{pre-financing} to all beneficiaries
    639639  \item \alert{providing} to partners detailed \alert{information} on consortium
    640     organization and FP7 management rules during Kick Off
     640    organisation and FP7 management rules during Kick Off
    641641  \item \alert{collecting and checking} partner's \alert{financial information} for the
    642642    First Progress Report
     
    663663  \item \alert{Kick-off, Bologna, February 2010.}\\
    664664   coordination of research activities, planning of future work,
    665    financial and administrative organization
     665   financial and administrative organisation
    666666  \item \alert{Project meeting, Edinburgh, July 2010.}\\
    667667   Just after D2.1. Fixing more precise scheduling; first informal
    668668   dissemination via co-location with FLOC
    669   \item \alert{Project meeting, Paris, Septermber 2010.}\\
     669  \item \alert{Project meeting, Paris, September 2010.}\\
    670670   Adoption of the MCS-51 target; discussion of the design of the costing
    671671   compiler (D2.2), memory model (D4.1). Integration problems foreseen.
Note: See TracChangeset for help on using the changeset viewer.