# Changeset 3462

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

Some final changes before submission.

Location:
Papers/fopara2013
Files:
3 edited

### Legend:

Unmodified
 r3461 % in the dependent labelling section. \begin{abstract} We provide an overview of the FET-Open Project CerCo (Certified Complexity'). Our main achievement is the development of a technique for analysing non-functional properties of programs (time, space) at the source level with little or no loss of accuracy 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) computational cost of the input program at the source level. Untrusted invariant generators and trusted theorem provers may then be used to compute and certify the parametric execution time of the code. We provide an overview of the FET-Open Project CerCo (Certified Complexity'). Our main achievement is the development of a technique for analysing non-functional properties of programs (time, space) at the source level with little or no loss of accuracy and a small trusted code base. The core component is a C compiler, verified in Matita, that produces an instrumented copy of the source code in addition to generating object code.  This instrumentation exposes, and tracks precisely, the actual (non-asymptotic) computational cost of the input program at the source level. Untrusted invariant generators and trusted theorem provers may then be used to compute and certify the parametric execution time of the code. \end{abstract} \end{itemize*} \paragraph{Vision and approach.} We wish to reconcile functional and We want to reconcile functional and non-functional analyses: to share information and perform both at the same time on high-level source code. very lightweight tracking of code changes through compilation. We have studied how to formally prove the correctness of compilers implementing this technique, and have implemented such a compiler from C to object binaries for the MCS-51 have implemented such a compiler from C to object binaries for the 8051 microcontroller for predicting execution time and stack space usage, verifying it in an interactive theorem prover.  As we are targeting \section{Project context and approach} 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 Formal methods for verifying functional properties of programs have now reached a level of maturity and automation that their adoption is slowly increasing in production environments. For safety critical code, it is becoming commonplace to combine rigorous software engineering methodologies and testing with static analyses, taking the strengths of each and mitigating their weaknesses. Of particular interest are open frameworks Despite these problems, the need for reliable real time systems and programs is increasing, and there is a push from the research community towards the introduction of systems and programs is increasing, and there is pressure from the research community for the introduction of hardware with more predictable behaviour, which would be more suitable for static analysis.  One example, exemplified by the Proartis for static analysis.  One example, being investigated by the Proartis project~\cite{proartis}, is to decouple execution time from execution history by introducing randomisation. First, there cannot be a uniform, precise cost model for source code instructions (or even basic blocks). During compilation, high level instructions are disassembled and reassembled in context-specific ways so that instructions are broken up and reassembled in context-specific ways so that identifying a fragment of object code and a single high level instruction is infeasible. Even the control flow of the object and source code can be very \subsection{CerCo's approach} In CerCo we propose a new approach to the problem: we abandon the idea In CerCo we propose a radically new approach to the problem: we reject the idea of a uniform cost model and we propose that the compiler, which knows how the code is translated, must return the cost model for basic blocks of high level to reverse them and by interfacing with processor timing analysis. By embracing the knowledge implicit in the compilation process, instead of avoiding it like EmBounded did, a CerCo By embracing compilation, instead of avoiding it like EmBounded did, a CerCo compiler can both produce efficient code and return costs that are as precise as the processor timing analysis can be. Moreover, our costs can be state (or mode, as the WCET literature calls it) we are in. The CerCo approach has the potential to substantially improve upon the current state of the The CerCo approach has the potential to dramatically improve the state of the art. By performing control and data flow analyses on the source code, the error prone translation of invariants is avoided. Instead, this prone translation of invariants is completely avoided. Instead, this work is done at the source level using tools of the user's choice. Any available technique for the verification of functional properties We take as granted the position that all software used to verify properties of programs must be as bug free as Software used to verify properties of programs must be as bug free as possible. The trusted code base for verification consists of the code that needs to be trusted to believe that the property holds. The trusted code base of char a[4] = {3, 2, 7, 14};  char threshold = 4; /*@ behaviour stack_cost: /*@ behavior stack_cost: ensures __stack_max <= __max(\old(__stack_max), 4+\old(__stack)); ensures __stack == \old(__stack); behaviour time_cost: behavior time_cost: ensures __cost <= \old(__cost)+(178+214*__max(1+\at(len,Pre), 0)); */ } /*@ behaviour stack_cost: /*@ behavior stack_cost: ensures __stack_max <= __max(\old(__stack_max), 6+\old(__stack)); ensures __stack == \old(__stack); behaviour time_cost: behavior time_cost: ensures __cost <= \old(__cost)+1358; */ \caption{The instrumented version of the program in \autoref{test1}, with instrumentation added by the CerCo compiler in red and cost invariants added by the CerCo Frama-C plugin in blue. The \texttt{\_\_cost}, \texttt{\_\_stack} and \texttt{\_\_stack\_max} variables hold the elapsed time added by the CerCo Frama-C plugin in blue. The \lstinline'__cost', \lstinline'__stack' and \lstinline'__stack_max' variables hold the elapsed time in clock cycles and the current and maximum stack usage. Their initial values hold the clock cycles spent in initialising the global data before calling \texttt{main} and the space required by global data (and thus unavailable for \lstinline'main' and the space required by global data (and thus unavailable for the stack). } \subsection{The (basic) labelling approach} The labelling approach is the foundational insight that underlies all the developments in CerCo. It facilitates the tracking of basic block evolution during the compilation process in order to propagate the cost model from the It allows the evolution of basic blocks to be tracked throughout the compilation process in order to propagate the cost model from the object code to the source code without losing precision in the process. \paragraph{Problem statement.} Given a source program $P$, we want to obtain an `while' language, all remaining compilers target realistic source languages---a pure higher order functional language and a large subset of C with pointers, \texttt{goto}s and all data structures---and real world target processors---MIPS and the Intel 8051/8052 processor of C with pointers, \lstinline'goto's and all data structures---and real world target processors---MIPS and the Intel 8051 processor family. Moreover, they achieve a level of optimisation that ranges from moderate (comparable to GCC level 1) to intermediate (including with both of our C compilers. The 8051/8052 microprocessor is a very simple one, with constant-cost The 8051 microprocessor is a very simple one, with constant-cost instructions. It was chosen to separate the issue of exact propagation of the cost model from the orthogonal problem of low-level timing analysis of object code The details on the proof techniques employed and the proof sketch can be found in the CerCo deliverables and papers~\cite{cerco-deliverables}. the proof sketch can be found in the CerCo deliverables and papers~\cite{cerco-website}. In this section we will only hint at the correctness statement, which turned out to be more complex than expected. soundness does not depend on the cost plugin, which can in principle produce any synthetic cost. However, in order to be able to actually prove the WCET of a C function, we need to add correct annotations in a way that prove a WCET bound for a C function, we need to add correct annotations in a way that Jessie and subsequent automatic provers have enough information to deduce their validity. In practice this is not straightforward even for very simple programs The cost annotations added by the CerCo compiler take the form of C instructions that update a fresh global variable called the cost variable by a constant. Synthesizing the WCET of a C function thus consists of statically resolving an Synthesizing a WCET bound of a C function thus consists of statically resolving an upper bound of the difference between the value of the cost variable before and after the execution of the function, i.e. finding the instructions \section{Conclusions and future work} All CerCo software and deliverables may be found on the project homepage~\cite{cerco}. All CerCo software and deliverables may be found on the project homepage~\cite{cerco-website}. The results obtained so far are encouraging and provide evidence that