source: Papers/jar-cerco-2017/introduction.tex @ 3622

Last change on this file since 3622 was 3620, checked in by boender, 3 years ago

Rewrote introduction to sound less futuristic/defensive

File size: 22.6 KB
Line 
1\newcommand{\All}[1]{\forall{#1}.\;}
2\newcommand{\lam}[1]{\lambda{#1}.\;}
3
4% Introduction
5%   Problem being solved, background, etc.
6%   Current state of the art (and problem with it)
7%   The `CerCo approach' (tm)
8%   Brief Matita overview
9%   Map of paper
10
11\section{Introduction}
12\label{sect.introduction}
13
14%\paragraph{Problem statement.}
15Programs can be specified using both functional constraints (what the program
16must do) and non-functional constraints (what time, space or other resources
17the program can use).  At the current state of the art, functional properties
18are verified by combining user annotations---preconditions, invariants, and so
19on---with a multitude of automated analyses---invariant generators, type
20systems, abstract interpretation, theorem proving, and so on---on the
21high-level source code of the program.
22
23By contrast, many non-functional properties are verified by analysing the
24low-level object code. Analysis on low-level object code has several problems,
25however:
26
27\begin{itemize*}
28\item
29It can be hard to deduce the high-level structure of the program after compiler
30optimisations. The object code produced by an optimising compiler may have a
31radically different control flow to the original source code program.
32\item
33Techniques that operate on object code are not useful early in the development
34process of a program, yet problems with the design or implementation of a
35program are cheaper to resolve early in the development process.
36\item
37Parametric cost analysis is very hard: how can we translate a cost that depends
38on the execution state, for example the value of a register or a carry bit, to
39a cost that the user can understand while looking at the source code?
40\item
41Performing functional analysis on object code makes it hard for the programmer
42to provide information about the program and its expected execution, leading to
43a loss of precision in the resulting analysis.
44\end{itemize*}
45
46\paragraph{Vision.}
47We want to reconcile functional and non-functional analysis: to share
48information between them and perform both at the same time on high-level source
49code.
50 
51What has previously prevented this approach from being applied is the lack of a
52uniform and precise cost model for high-level code, since each statement
53occurrence is compiled differently, optimisations may change control flow, and
54the cost of an object code instruction may depend on the runtime state of
55hardware components like pipelines and caches, none of which are visible in the
56source code.
57
58We envision a new generation of compilers that track program structure through
59compilation and optimisation and exploit this information to define a precise,
60non-uniform cost model for source code that accounts for runtime state. With
61such a cost model we can perform non-functional verification in a similar way
62to functional verification and exploit the state of the art in automated
63high-level verification~\cite{survey}.
64
65The techniques currently used by the Worst Case Execution Time (WCET) community,
66which perform analysis on object code, are still applicable but can be coupled
67with additional source-level analysis. In cases where our approach produces
68overly complex cost models, safe approximations can be used to trade complexity
69for precision.
70
71Finally, source code analysis can be used early in the development process,
72when components have been specified but not implemented, as modularity means
73that it is enough to specify the non-functional behaviour of missing components.
74
75\paragraph{Contributions.}
76We have developed \emph{the labelling approach}~\cite{labelling}, a technique
77to implement compilers that induce cost models on source programs by very
78lightweight tracking of code changes through the compilation pipeline.
79
80We have implemented a compiler from C to object binaries for the 8051
81microcontroller which uses this technique. The compiler predicts
82execution time and stack space usage. We have also verified the compile using
83an interactive theorem prover. As we are targeting an embedded microcontroller
84we have not considered dynamic memory allocation.
85
86To demonstrate source-level verification of costs we have implemented a Frama-C
87plugin~\cite{framac} that invokes the compiler on a source program and uses it
88to generate invariants on the high-level source that correctly model low-level
89costs. The plugin certifies that the program respects these costs by calling
90automated theorem provers, a new and innovative technique in the field of cost
91analysis.
92
93Finally, we have conducted several case studies, including showing that the
94plugin can automatically compute and certify the exact reaction time of
95Lustre~\cite{lustre} data flow programs compiled into C.
96
97\subsection{Project context and approach}
98
99Formal methods for verifying functional properties of programs have now reached
100such a level of maturity and automation that their adoption is slowly
101increasing in production environments.
102
103For safety critical code, it is becoming commonplace to combine rigorous
104software engineering methodologies and testing with static analyses, taking the
105strengths of each and mitigating their weaknesses. Of particular interest are
106open frameworks for the combination of different formal methods, where the
107programs can be progressively specified and enriched with new safety
108guarantees: every method contributes knowledge (e.g. new invariants) that
109can be built upon by other analysis methods.
110
111The outlook for verification of non-functional properties of programs (time
112spent, memory used, energy consumed) is bleaker. In most cases, verifying that
113real-time systems meet their deadlines is done by simply performing many runs
114of the system and timing their execution, computing the maximum time and adding
115an empirical safety margin, claiming the result to be a bound for the WCET of
116the program.
117
118Formal methods and software to statically analyse the WCET of programs exist,
119but they often produce bounds that are too pessimistic to be useful. Recent
120advances in hardware architecture have focused on improving average case
121performance, not predictability of the worst case.
122
123Execution time is becoming increasingly dependent on execution history and the
124internal state of hardware components like pipelines and caches. Multi-core
125processors and non-uniform memory models are drastically reducing the
126possibility of performing static analysis in isolation, because programs are
127less and less time-composable. Clock-precise hardware models are necessary for
128static analysis, and obtaining them is becoming harder due to the increased
129sophistication of hardware design.
130
131The need for reliable real-time systems and programs is increasing, and there
132is pressure from the research community for the introduction of hardware with
133more predictable behaviour, which would be more suitable for static analysis.
134One example, being investigated by the Proartis project~\cite{proartis}, is to
135decouple execution time from execution history by introducing randomisation.
136
137In CerCo~\cite{cerco} we do not address this problem, optimistically assuming
138that improvements in low-level timing analysis or architecture will make
139verification feasible in the longer term.
140
141Instead, the main objective of our work is to bring together static analysis of
142functional and non-functional properties, which in the current state of the art
143are independent activities with limited exchange of information: while the
144functional properties are verified on the source code, the analysis of
145non-functional properties is performed on object code to exploit clock-precise
146hardware models.
147
148\subsection{Current object-code methods}
149
150Analysis currently takes place on object code for two main reasons.
151
152Firstly, there cannot be a uniform, precise cost model for source code
153instructions (or even basic blocks). During compilation, high level
154instructions are broken up and reassembled in context-specific ways so that
155identifying a fragment of object code and a single high level instruction is
156unfeasible.
157
158Additionally, the control flow of the object and source code can be very
159different as a result of optimisations. For example, aggressive loop
160optimisations can completely transform source level loops.
161
162Despite the lack of a uniform, compilation- and program-independent cost model
163on the source language, research on the analysis of non-asymptotic execution
164time on high level languages assuming such a model is growing and gaining
165momentum.
166
167Unless such cost models are developed, the future practical impact of this
168research looks to be minimal. One existing approach is the EmBounded
169project~\cite{embounded}, which compositionally compiles high-level code to a
170byte code that is executed by an interpreter with guarantees on the maximal
171execution time spent for each byte code instruction. This provides a model
172that is uniform, though at the expense of precision (each cost is a pessimistic
173upper bound) and the performance of the executed code (the byte code is
174interpreted compositionally).
175
176The second reason to perform analysis on the object code is that bounding
177the worst case execution time of small code fragments in isolation (e.g. loop
178bodies) and then adding up the bounds yields very poor estimates as no
179knowledge of the hardware state prior to executing the fragment can be assumed.
180
181By analysing longer runs the bound obtained becomes more precise because the
182lack of information about the initial state has a relatively small impact.
183
184To calculate the cost of an execution, value and control flow analyses are
185required to bound the number of times each basic block is executed. Currently,
186state of the art WCET analysis tools, such as AbsInt's aiT
187toolset~\cite{absint}, perform these analyses on object code, where the logic
188of the program is harder to reconstruct and most information available at the
189source code level has been lost; see~\cite{stateart} for a survey.
190
191Imprecision in the analysis can lead to useless bounds. To augment precision,
192currently tools ask the user to provide constraints on the object code control
193flow, usually in the form of bounds on the number of iterations of loops or
194linear inequalities on them. This requires the user to manually link the source and object code, translating their assumptions on the source code (which may be
195wrong) to object code constraints. This task is hard and error-prone,
196especially in the presence of complex compiler optimisations.
197
198Traditional techniques for WCET that work on object code are also affected by
199another problem: they cannot be applied before the generation of the object
200code. Functional properties can be analysed in early development stages, while
201analysis of non-functional properties may come too late to avoid expensive
202changes to the program architecture.
203
204\subsection{The CerCo approach}
205
206In CerCo we propose a radically new approach to the problem: we reject the idea
207of a uniform cost model and we propose that the compiler, which knows how the
208code is translated, must return the cost model for basic blocks of high level
209instructions. It must do so by keeping track of the control flow modifications
210to reverse them and by interfacing with processor timing analysis.
211
212By embracing compilation, instead of avoiding it like EmBounded did, a CerCo
213compiler can both produce efficient code and return costs that are as precise
214as the processor timing analysis can be. Moreover, our costs can be parametric:
215the cost of a block can depend on actual program data, on a summary of the
216execution history, or on an approximated representation of the hardware state.
217
218For example, loop optimisations may assign a cost to a loop body that is a
219function of the number of iterations performed. As another example, the cost of
220a block may be a function of the vector of stalled pipeline states, which can
221be exposed in the source code and updated at each basic block exit.
222
223It is parametricity that allows one to analyse small code fragments without
224losing precision. In the analysis of the code fragment we do not have to ignore
225the initial hardware state; rather, we can assume that we know exactly which
226state (or mode, as the WCET literature calls it) we are in.
227
228The CerCo approach has the potential to dramatically improve the state of the
229art. By performing control and data flow analyses on the source code, the
230error-prone translation of invariants is avoided entirely. Instead, this work
231is done at the source code level using tools of the user's choice.
232
233Any available technique for the verification of functional properties can be
234easily reused and multiple techniques can collaborate to infer and certify cost
235invariants for the program. There are no limitations on the types of loops or
236data structures involved.
237
238Parametric cost analysis becomes the default, with non-parametric bounds used
239only as a last resort when the user decides to trade the complexity of the
240analysis for more precision.
241
242\emph{A priori}, no technique previously used in traditional WCET is obsolete:
243processor timing analysis can be used by the compiler on the object code, and
244other techniques can be applied at the source code level.
245
246Our approach also works in the early stages of development by allowing the user
247to axiomatically attach costs to unimplemented components.
248
249Software used to verify properties of programs must be as bug-free as possible.
250The trusted code base for verification consists of the code that needs to be
251trusted to believe that the property holds.
252
253The trusted code base of state-of-the-art WCET tools is very large: one needs
254to trust the control flow analyser, the linear programming libraries used, and
255also the formal models of the hardware under analysis.
256
257In CerCo we move the control flow analysis to the source code level, and we
258introduce a non-standard compiler. To reduce the size of the trusted code base,
259we have implemented a prototype compiler and static analyser in an interactive
260theorem prover, which was used to certify that the costs added to the source
261code are indeed those incurred by the hardware. We have also implemented formal models of the hardware and of the high level source language in the interactive
262theorem prover.
263
264Control flow analysis on the source code has been obtained using invariant
265generators, tools to produce proof obligations from generated invariants and
266automatic theorem provers to verify the obligations. If these tools are able to
267generate proof traces that can be independently checked, the only remaining
268component that enters the trusted code base is an off-the-shelf invariant
269generator which, in turn, can be proved correct using an interactive theorem
270prover.
271
272With these methods, we achieve the objective of allowing the use of more
273off-the-shelf components (e.g. provers and invariant generators) whilst
274reducing the trusted code base at the same time.
275
276\subsection{Introduction to Matita}
277
278Matita is a theorem prover based on a variant of the Calculus of Coinductive Constructions~\cite{asperti:user:2007}.
279The system features a full spectrum of dependent types and (co)inductive families, a system of coercions, a tactic-driven proof construction engine~\cite{sacerdoti-coen:tinycals:2007}, and paramodulation based automation~\cite{asperti:higher-order:2007}, all of which we exploit in the formalisation described herein.
280
281Matita's syntax is similar to the syntaxes of mainstream functional programming languages such as OCaml or Standard ML.
282The type theory that Matita implements is broadly akin to that of Coq~\cite{coq:2004} and Agda~\cite{bove:brief:2009}.
283Nevertheless, we provide a brief explanation of the main syntactic and type-theoretic features of Matita that will be needed to follow the body of the paper:
284\begin{itemize}
285\item
286Non-recursive functions and definitions are introduced via the \texttt{definition} keyword.
287Recursive functions are introduced with \texttt{let rec}.
288Mutually recursive functions are separated via the \texttt{and} keyword.
289Matita's termination checker ensures that all recursive functions are terminating before being admitted to maintain soundness of the system's logic.
290\item
291Matita has an infinite hierarchy of type universes.
292A single impredicative universe of types, \texttt{Prop}, exists at the base of this hierarchy.
293An infinite series of predicative universes, \texttt{Type[0]} : \texttt{Type[1]} : \texttt{Type[2]}, and so on and so forth, sits atop \texttt{Prop}.
294Matita, unlike Coq or Agda, implements no form of typical ambiguity or universe polymorphism, with explicit concrete universe levels being preferred instead.
295\item
296Matita's type theory plays host to a rich and expressive higher-order logic.
297Constants \texttt{True} and \texttt{False} represent truth and falsity in \texttt{Prop} respectively.
298Two inductive families in \texttt{Prop} encode conjunction and disjunction---$\mathtt{P \wedge Q}$ and $\mathtt{P \vee Q}$ respectively.
299
300As is usual, implication and universal quantification are identified with the dependent function space ($\Pi$ types), whereas (constructive) existential quantification is encoded as a dependent sum (a $\Sigma$-type).
301We write $\All{x : \phi}\psi$ for the dependent function space, and abbreviate this as $\phi \rightarrow \psi$ when $x \not\in fv(\psi)$ as usual.
302We use $\langle M,N \rangle$ for the pairing of $M$ and $N$.
303\item
304Inductive and coinductive families are introduced via the \texttt{inductive} and \texttt{coinductive} keywords respectively, with named constructor declarations separated by a bar.
305Mutually inductive data family declarations are separated via \texttt{with}.
306In the following declaration:
307\begin{lstlisting}[language=Grafite]
308inductive I ($P_1$ : $\tau_1$) $\ldots$ ($P_n$ : $\tau_n$) : $\phi_1 \rightarrow \ldots \rightarrow \phi_m \rightarrow \phi$ := $\ldots$
309\end{lstlisting}
310We call $P_i$ for $0 \leq i \leq n$ the \textbf{parameters} of \texttt{I} and $\phi_j$ for $0 \leq j \leq m$ the \textbf{indices} of \texttt{I}.
311Matita's positivity checker ensures that constructors have strictly-positive types before admitting an inductive family to maintain soundness of the system's logic.
312\item
313Records are introduced with the \texttt{record} keyword.
314A Matita record
315\begin{lstlisting}[language=Grafite]
316record R : Type[0] := { F1 : nat }.
317\end{lstlisting}
318may be thought of as syntactic sugar for a single-constructor inductive data type of the same name:
319\begin{lstlisting}[language=Grafite]
320inductive R : Type[0] :=
321  | mk_R : nat -> R.
322\end{lstlisting}
323A record field's type may depend on fields declared earlier in the record.
324
325Records may be decomposed with projections.
326Projections, one for each of field of a record, are registered in the global context.
327In the example record above, \texttt{F1} of type $R \rightarrow nat$ is registered as a field projection and $mk\_R$ of type $nat \rightarrow R$ is registered as a constructor.
328
329Record fields may also be marked as coercions.
330In the following example
331\begin{lstlisting}[language=Grafite]
332record S : Type[1] :=
333{
334  Carrier :> Type[0];
335  op : Carrier -> Carrier -> Carrier
336}
337\end{lstlisting}
338the field \texttt{Carrier} is declared to be a coercion with `\texttt{:>}'.with the operational effect being that the field projection \texttt{Carrier} may be omitted where it could be successfully inferred by Matita.
339Field coercions facilitate the informal but common mathematical practice of intentionally confusing a structure with its underlying carrier set.
340\item
341Terms may be freely omitted, allowing the user to write down partial types and terms.
342A question mark, \texttt{?}, denotes a single term that has been omitted by the user.
343Some omitted terms can be deduced by Matita's refinement system.
344Other, more complex goals arising from omitted terms may require user input to solve, in which case a proof obligation is opened for each term that cannot be deduced automatically.
345Three consecutive dots, \texttt{$\ldots$}, denote multiple terms or types that have been omitted.
346\item
347Data may be decomposed by pattern matching with a \texttt{match} expression.
348We may fully annotate a \texttt{match} expression with its return type.
349This is especially useful when working with indexed families of types or with invariants, expressed as types, on functions.
350In the following
351\begin{lstlisting}[language=Grafite]
352match t return $\lam{x}x = 0 \rightarrow bool$ with
353[ 0    $\Rightarrow$ $\lam{prf_1}P_1$
354| S m $\Rightarrow$ $\lam{prf_2}P_2$
355] (refl $\ldots$ t)
356\end{lstlisting}
357the \texttt{0} branch of the \texttt{match} expression returns a function from $0 = 0$ to \texttt{bool}, whereas the \texttt{S m} branch of the \texttt{match} expression returns a function from \texttt{S m = 0} to \texttt{bool}.
358In both cases the annotated return type $\lam{x}x = 0 \rightarrow bool$ has been specialised given new information about \texttt{t} revealed by the act of pattern matching.
359The entire term, with \texttt{match} expression applied to \texttt{refl $\ldots$ t}, has type \texttt{bool}.
360\item
361Matita features a liberal system of coercions (distinct from the previously mentioned record field coercions).
362It is possible to define a uniform coercion $\lam{x}\langle x, ?\rangle$ from every type $T$ to the dependent product $\Sigma{x : T}. P x$.
363The coercion opens a proof obligation that asks the user to prove that $P$ holds for $x$.
364When a coercion is to be applied to a complex term (for example, a $\lambda$-abstraction, a local definition, or a case analysis), the system automatically propagates the coercion to the sub-terms.
365For instance, to apply a coercion to force $\lam{x}M : A \rightarrow B$ to
366have type $\All{x : A}\Sigma{y : B}. P x y$, the system looks for a coercion from $M : B$ to $\Sigma{y : B}. P x y$ in a context augmented with $x : A$.
367This is significant when the coercion opens a proof obligation, as the user will be presented with multiple, but simpler proof obligations in the correct context.
368In this way, Matita supports the `Russell' proof methodology developed by Sozeau in~\cite{sozeau:subset:2007}, in a lightweight but tightly-integrated manner.
369\end{itemize}
370Throughout, for reasons of clarity, conciseness, and readability, we may choose to simplify or omit parts of Matita code.
371We will always ensure that these omissions do not mislead the reader.
372
373\subsection{Map of the paper}
374
375The rest of the paper is structured as follows.
376
377In section~\ref{sect.compiler.architecture}, we describe the architecture of the
378CerCo compiler, as well as the intermediate languages that it uses. We also
379describe the target hardware and its formal model.
380
381In section~\ref{sect.compiler.proof}, we describe the proof of correctness of
382the compiler in more detail. We explain our use of structured traces, the
383labelling approach, and discuss the assembler.
384
385In section~\ref{sect.formal.development}, we present data on the formal
386development.
387
388In section~\ref{sect.framac.plugin}, we discuss the Frama-C plugin, as well as
389some of the case studies we have performed to validate it.
390
391Finally, in section~\ref{sect.conclusions} we present conclusions, as well as
392related and future work.
Note: See TracBrowser for help on using the repository browser.