Changeset 47


Ignore:
Timestamp:
Sep 9, 2010, 11:04:15 AM (9 years ago)
Author:
mulligan
Message:

Half of report's English fixed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D6.2/report.tex

    r23 r47  
    6262is the first \textbf{report} of the \cerco{} project. The deliverable is
    6363\textbf{confidential} and required an effort of about \textbf{2 person-months}.
    64 The description of the deliverable in the Grant Agreement is the following one:
     64The following is a description of the deliverable in the Grant Agreement:
    6565\begin{quote}
    6666Plan for the Use and dissemination of foreground: An articulated dissemination plan, containing the individuation of the main target communities, and the relative exploitation strategies.
     
    9595theorem proving in particular, critical IT systems are slowly undergoing a
    9696paradigm shift: testing of critical properties is going to be partially
    97 replaced with formal verification on the programs written in an high level
    98 language, and a set of formally verified tools (interpreters, compilers,
    99 operating systems, communication libraries) is going to be used to grant preservation
    100 of the verified property for the actual runs of the low level code.
     97replaced with formal verification of programs written in high level
     98languages, and a set of formally verified tools (interpreters, compilers,
     99operating systems, communication libraries) is going to be used to preserve
     100the verified properties for the execution of the low level code.
    101101
    102102The present state of the art already provides a few mildly optimizing
    103 verified compilers that compete with traditional highly optimized compilers
     103verified compilers that compete with traditional highly optimised compilers,
    104104and a few prototypes and experiments in the verification of operating systems.
    105 However, the only properties that have been formalized are extensional, granting
    106 that the high level semantics of the program --- usually specified in terms
    107 of infinite resources (e.g. memory) --- is respected. All intensional
    108 properties that have to do with resources are not currently preserved during
     105However, the only properties that have been formalized are extensional, proving
     106that the high level semantics of the program---usually specified in terms
     107of infinite resources (e.g. memory)---is respected. All intensional
     108properties that refer to resource consumption are not currently preserved during
    109109compilation or, at least, no formal proof of preservation is provided. Hence
    110110high level programs still need to be extensively tested to verify resource
     
    115115execution time, and we will develop the first certified compiler that is able
    116116to manifest in the source program some intentional properties, mainly
    117 execution cost, that are inferred from the target program. The main issue
    118 in doing so is to preserve compositionality of compilation: while the source
    119 program undergoes several intentionally disruptive translations towards lower
    120 and lower intermediate languages, we need to keep trace of the evolution of
     117execution cost, that are inferred from the target program. The main challenge is
     118to preserve the compositionality of compilation: whilst the source program
     119undergoes several intentionally disruptive translations toward lower and lower
     120level intermediate languages, we must keep track of the evolution of
    121121sensible code fragments in order to relate source, intermediate and target
    122 code fragments to back-propagate execution costs. Hence we expect to study
    123 new more refined ways of expressing the operational semantics of programs
    124 and to give a more refined notion of operational bisimulation, with the aim
    125 of obtaining a characterization that is loose enough to capture some of the
    126 most common and effective optimizations.
     122code fragments, so that execution costs may be back-propagated. Hence we expect
     123to study new more refined ways of expressing the operational semantics of
     124programs and to give a more refined notion of operational bisimulation, with the
     125aim of obtaining a characterisation that is loose enough to capture some of the
     126most common and effective optimisations.
    127127
    128128Once we can manifest in the source program execution costs computed on the
    129 target program we will start the investigation of the exploitability of the
     129target program we will start investigating the exploitability of the
    130130cost annotations. In particular, cost annotations must be combined with
    131 extensional program invariants in order to obtain intensional program invariants
     131extensional program invariants in order to obtain intensional program invariants,
    132132and be able to formally prove intensional properties of programs. We expect
    133133this study to require a long effort and to be performed outside the project
    134134timeframe. However, we assume that a combination of interactive theorem proving
    135 and automatic formal methods (like abstract interpretation) will need to be
     135and automatated formal methods (like abstract interpretation) will need to be
    136136exploited and, in the project, we will focus on interactive theorem proving by
    137 exploiting and providing basic tools to reason on cost invariants.
    138 
    139 All the major deliverables of \cerco{} are prototypes --- either software
    140 prototypes or formal certifications --- that are later integrated at project
     137exploiting and providing basic tools to reason about cost invariants.
     138
     139All the major deliverables of \cerco{} are prototypes---either software
     140prototypes or formal certifications---that are later integrated at project
    141141milestones into major \cerco{} compiler snapshots. These snapshots are the
    142 most appropriate deliverables for dissemination in the large and different
     142most appropriate deliverables for dissemination in the large, and different
    143143target communities are associated to the snapshots. We will discuss
    144 the milestones and snapshots in details
    145 in Section~\ref{byresult} in order to identify the potential target communities
    146 and relative specific dissemination actions.
     144the milestones and snapshots in detail in Section~\ref{byresult} in order to
     145identify the potential target communities and most appropriate means of
     146dissemination.
    147147
    148148
     
    152152\begin{tabular}{|lc|}
    153153\hline
    154 milestone name & due at month \\ \hline
     154Milestone name & Month due \\ \hline
    155155Untrusted cost-annotating compiler & 12 \\
    156156Untrusted CerCo compiler & 24 \\
     
    163163
    164164\subsection{Academic exploitation}
    165  Academic partners will take great advantage from the results of CerCo mainly in terms of increased technical know-how and scientific knowledge, increased visibility in the scientific community of reference, increased expertise, exploitable for institutional academic purposes (e.g. didactic activities). We also expect that the rest of the academic community will take up the innovative ideas of the project, building on top of them code analyses at a level of accuracy that could have not been previously possible. Finally, we expect elaboration and instantiation of our methodology to other kinds of high level languages (functional, logic) and to more complex scenarios involving, for instance, a real time operating system.
     165 Academic partners will take great advantage of the \cerco{}'s results mainly in
     166terms of increased technical know-how and scientific knowledge, increased
     167visibility in the scientific community of reference, increased expertise,
     168and for institutional academic exploitation (e.g. didactic activities). We also
     169expect that the rest of the academic community will take up the innovative ideas
     170of the project, building on top of them code analyses at a level of accuracy that
     171could have not been previously possible. Finally, we expect our methodology to
     172be applied to other styles of high-level programming language (for instance,
     173functional or logic) and to more complex scenarios involving, for example, a
     174real time operating system.
    166175
    167176\subsection{Industrial exploitation}
    168  The long term industrial exploitation of the results of the CerCo project is envisaged mainly in the area of the embedded systems/software, in particular in the case of safety critical applications and time critical (realtime) applications. In the short term, software houses producing compilers for embedded systems could immediately benefit from the CerCo cost annotating technology or, more generally, by the know- how provided in the certification of compilers. It is worth noting that several of these software houses are located in Europe, such as the medium-sized System Engineer Group of Freescale, which is headquartered in Scotland, Raisonance and Cosmic Software, which are headquartered in France, the small-size Hightech, headquartered in Germany, just to name a few.
     177The long term industrial exploitation of the results of the CerCo project is
     178mainly embodied in the area of embedded systems/software, in particular in the
     179case of safety critical applications and time critical (realtime) applications.
     180In the short term, software houses producing compilers for embedded systems
     181could immediately draw benefit from the \cerco{} cost annotating technology or,
     182more generally, by the knowledge gained in the certification of compilers. It
     183is worth noting that several of these software houses are located in Europe,
     184such as the medium-scale System Engineer Group of Freescale, headquartered in
     185Scotland, Raisonance and Cosmic Software, headquartered in France, and the
     186small-scale Hightech, headquartered in Germany, amongst many others.
    169187
    170188\subsection{Management of knowledge and intellectual property}
     
    378396Compiler developers will be interested by the techniques used to trace evolution
    379397of code fragments during compilation. They should also be interested in
    380 enhancing the proposed techniques to address more optimizations.
     398enhancing the proposed techniques to address more optimisations.
    381399
    382400Developers of code invariant generators will be able to apply and extend their
Note: See TracChangeset for help on using the changeset viewer.