Changeset 3462 for Papers


Ignore:
Timestamp:
Feb 21, 2014, 5:51:01 PM (6 years ago)
Author:
campbell
Message:

Some final changes before submission.

Location:
Papers/fopara2013
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • Papers/fopara2013/fopara13.bib

    r3456 r3462  
    277277
    278278@misc
    279 { cerco-deliverables,
     279{ cerco-website,
    280280  url = {http://cerco.cs.unibo.it},
    281   title = {The {Certified Complexity} ({CerCo}) project papers and deliverables},
     281  title = {The {Certified Complexity} ({CerCo}) project web site},
    282282  key = {cerco}
    283283}
  • Papers/fopara2013/fopara13.tex

    r3461 r3462  
    9494% in the dependent labelling section.
    9595\begin{abstract}
    96 We provide an overview of the FET-Open Project CerCo
    97 (`Certified Complexity'). Our main achievement is
    98 the development of a technique for analysing non-functional
    99 properties of programs (time, space) at the source level with little or no loss of accuracy
    100 and a small trusted code base. We developed a C compiler, verified in Matita, that translates source code to object code, producing a copy of the source code embellished with cost annotations as an additional side-effect. These annotations expose and track precisely the actual (non-asymptotic)
    101 computational cost of the input program at
    102 the source level. Untrusted invariant generators and trusted theorem provers
    103 may then be used to compute and certify the parametric execution time of the
    104 code.
     96  We provide an overview of the FET-Open Project CerCo (`Certified
     97  Complexity'). Our main achievement is the development of a technique
     98  for analysing non-functional properties of programs (time, space) at
     99  the source level with little or no loss of accuracy and a small
     100  trusted code base. The core component is a C compiler, verified in
     101  Matita, that produces an instrumented copy of the source code in
     102  addition to generating object code.  This instrumentation exposes, and
     103  tracks precisely, the actual (non-asymptotic) computational cost of
     104  the input program at the source level. Untrusted invariant
     105  generators and trusted theorem provers may then be used to compute
     106  and certify the parametric execution time of the code.
    105107\end{abstract}
    106108
     
    139141\end{itemize*}
    140142\paragraph{Vision and approach.}
    141 We wish to reconcile functional and
     143We want to reconcile functional and
    142144non-functional analyses: to share information and perform both at the same time
    143145on high-level source code.
     
    165167very lightweight tracking of code changes through compilation. We have studied
    166168how to formally prove the correctness of compilers implementing this technique, and
    167 have implemented such a compiler from C to object binaries for the MCS-51
     169have implemented such a compiler from C to object binaries for the 8051
    168170microcontroller for predicting execution time and stack space usage,
    169171verifying it in an interactive theorem prover.  As we are targeting
     
    181183
    182184\section{Project context and approach}
    183 Formal methods for the verification of functional properties of programs are now mature enough to find increasing application in production environments. For safety critical code, it is commonplace to combine rigorous engineering methodologies and testing
     185Formal methods for verifying functional properties of programs have 
     186now reached a level of maturity and automation that their adoption is slowly
     187increasing in production environments. For safety critical code, it is
     188becoming commonplace to combine rigorous software engineering methodologies and testing
    184189with static analyses, taking the strengths of each and mitigating
    185190their weaknesses. Of particular interest are open frameworks
     
    210215
    211216Despite these problems, the need for reliable real time
    212 systems and programs is increasing, and there is a push
    213 from the research community towards the introduction of
     217systems and programs is increasing, and there is pressure
     218from the research community for the introduction of
    214219hardware with more predictable behaviour, which would be more suitable
    215 for static analysis.  One example, exemplified by the Proartis
     220for static analysis.  One example, being investigated by the Proartis
    216221project~\cite{proartis}, is to decouple execution time from execution
    217222history by introducing randomisation.
     
    232237First, there cannot be a uniform, precise cost model for source
    233238code instructions (or even basic blocks). During compilation, high level
    234 instructions are disassembled and reassembled in context-specific ways so that
     239instructions are broken up and reassembled in context-specific ways so that
    235240identifying a fragment of object code and a single high level instruction is
    236241infeasible. Even the control flow of the object and source code can be very
     
    279284\subsection{CerCo's approach}
    280285
    281 In CerCo we propose a new approach to the problem: we abandon the idea
     286In CerCo we propose a radically new approach to the problem: we reject the idea
    282287of a uniform cost model and we propose that the compiler, which knows how the
    283288code is translated, must return the cost model for basic blocks of high level
     
    285290to reverse them and by interfacing with processor timing analysis.
    286291
    287 By embracing the knowledge implicit in the compilation process, instead of avoiding it like EmBounded did, a CerCo
     292By embracing compilation, instead of avoiding it like EmBounded did, a CerCo
    288293compiler can both produce efficient code and return costs that are
    289294as precise as the processor timing analysis can be. Moreover, our costs can be
     
    299304state (or mode, as the WCET literature calls it) we are in.
    300305
    301 The CerCo approach has the potential to substantially improve upon the current state of the
     306The CerCo approach has the potential to dramatically improve the state of the
    302307art. By performing control and data flow analyses on the source code, the error
    303 prone translation of invariants is avoided. Instead, this
     308prone translation of invariants is completely avoided. Instead, this
    304309work is done at the source level using tools of the user's choice.
    305310Any available technique for the verification of functional properties
     
    316321
    317322
    318 We take as granted the position that all software used to verify properties of programs must be as bug free as
     323Software used to verify properties of programs must be as bug free as
    319324possible. The trusted code base for verification consists of the code that needs
    320325to be trusted to believe that the property holds. The trusted code base of
     
    497502char a[4] = {3, 2, 7, 14};  char threshold = 4;
    498503
    499 /*@ behaviour stack_cost:
     504/*@ behavior stack_cost:
    500505      ensures __stack_max <= __max(\old(__stack_max), 4+\old(__stack));
    501506      ensures __stack == \old(__stack);
    502     behaviour time_cost:
     507    behavior time_cost:
    503508      ensures __cost <= \old(__cost)+(178+214*__max(1+\at(len,Pre), 0));
    504509*/
     
    526531}
    527532
    528 /*@ behaviour stack_cost:
     533/*@ behavior stack_cost:
    529534      ensures __stack_max <= __max(\old(__stack_max), 6+\old(__stack));
    530535      ensures __stack == \old(__stack);
    531     behaviour time_cost:
     536    behavior time_cost:
    532537      ensures __cost <= \old(__cost)+1358;
    533538*/
     
    542547\caption{The instrumented version of the program in \autoref{test1},
    543548 with instrumentation added by the CerCo compiler in red and cost invariants
    544  added by the CerCo Frama-C plugin in blue. The \texttt{\_\_cost},
    545  \texttt{\_\_stack} and \texttt{\_\_stack\_max} variables hold the elapsed time
     549 added by the CerCo Frama-C plugin in blue. The \lstinline'__cost',
     550 \lstinline'__stack' and \lstinline'__stack_max' variables hold the elapsed time
    546551in clock cycles and the current and maximum stack usage. Their initial values
    547552hold the clock cycles spent in initialising the global data before calling
    548 \texttt{main} and the space required by global data (and thus unavailable for
     553\lstinline'main' and the space required by global data (and thus unavailable for
    549554the stack).
    550555}
     
    601606\subsection{The (basic) labelling approach}
    602607The labelling approach is the foundational insight that underlies all the developments in CerCo.
    603 It facilitates the tracking of basic block evolution during the compilation process in order to propagate the cost model from the
     608It allows the evolution of basic blocks to be tracked throughout the compilation process in order to propagate the cost model from the
    604609object code to the source code without losing precision in the process.
    605610\paragraph{Problem statement.} Given a source program $P$, we want to obtain an
     
    711716`while' language, all remaining compilers target realistic source
    712717languages---a pure higher order functional language and a large subset
    713 of C with pointers, \texttt{goto}s and all data structures---and real world
    714 target processors---MIPS and the Intel 8051/8052 processor
     718of C with pointers, \lstinline'goto's and all data structures---and real world
     719target processors---MIPS and the Intel 8051 processor
    715720family. Moreover, they achieve a level of optimisation that ranges
    716721from moderate (comparable to GCC level 1) to intermediate (including
     
    760765with both of our C compilers.
    761766
    762 The 8051/8052 microprocessor is a very simple one, with constant-cost
     767The 8051 microprocessor is a very simple one, with constant-cost
    763768instructions. It was chosen to separate the issue of exact propagation of the
    764769cost model from the orthogonal problem of low-level timing analysis of object code
     
    827832The details on the proof techniques employed
    828833and
    829 the proof sketch can be found in the CerCo deliverables and papers~\cite{cerco-deliverables}.
     834the proof sketch can be found in the CerCo deliverables and papers~\cite{cerco-website}.
    830835In this section we will only hint at the correctness statement, which turned
    831836out to be more complex than expected.
     
    10081013soundness does not depend on the cost plugin, which can in
    10091014principle produce any synthetic cost. However, in order to be able to actually
    1010 prove the WCET of a C function, we need to add correct annotations in a way that
     1015prove a WCET bound for a C function, we need to add correct annotations in a way that
    10111016Jessie and subsequent automatic provers have enough information to deduce their
    10121017validity. In practice this is not straightforward even for very simple programs
     
    10281033The cost annotations added by the CerCo compiler take the form of C instructions
    10291034that update a fresh global variable called the cost variable by a constant.
    1030 Synthesizing the WCET of a C function thus consists of statically resolving an
     1035Synthesizing a WCET bound of a C function thus consists of statically resolving an
    10311036upper bound of the difference between the value of the cost variable before and
    10321037after the execution of the function, i.e. finding the instructions
     
    10841089\section{Conclusions and future work}
    10851090
    1086 All CerCo software and deliverables may be found on the project homepage~\cite{cerco}.
     1091All CerCo software and deliverables may be found on the project homepage~\cite{cerco-website}.
    10871092
    10881093The results obtained so far are encouraging and provide evidence that
Note: See TracChangeset for help on using the changeset viewer.