Subversion Repositories HelenOS-doc

Compare Revisions

Ignore whitespace Rev 183 → Rev 184

/papers/isarcs10/isarcs10.tex
4,9 → 4,9
\title{A Road to a Formally Verified General-Purpose Operating System}
\author{Martin D\v{e}ck\'{y}}
\institute{Department of Distributed and Dependable Systems\\
Faculty of Mathematics and Physics, Charles University\\
Malostransk\'{e} n\'{a}m\v{e}st\'{i} 25, Prague 1, 118~00, Czech Republic\\
\email{martin.decky@d3s.mff.cuni.cz}}
Faculty of Mathematics and Physics, Charles University\\
Malostransk\'{e} n\'{a}m\v{e}st\'{i} 25, Prague 1, 118~00, Czech Republic\\
\email{martin.decky@d3s.mff.cuni.cz}}
 
\begin{document}
\maketitle
132,7 → 132,7
\medskip
HelenOS can be briefly described as microkernel multiserver design. However, the actual design
HelenOS can be briefly described as microkernel multiserver OS. However, the actual design
guiding principles of the HelenOS are more elaborate:
\begin{description}
151,8 → 151,8
\item[Multiserver principle] Subsystems in user space should be decomposed with the smallest
reasonable granularity. Each unit of decomposition should be encapsulated in a separate task.
The tasks represent software components with isolated address spaces. From the design point of
view the kernel can be seen as a separate component, too.
\item[Split of mechanism and policy] The kernel should only provide low-level mechanisms,
view the kernel can be seen as a separate software component, too.
\item[Split of mechanism and policy] The kernel should only provide low-level me\-chanisms,
while the high-level policies which are built upon these mechanisms should be defined in
user space. This also implies that the policies should be easily replaceable while keeping
the low-level mechanisms intact.
227,9 → 227,9
However, what is the biggest advantage of C in terms of run-time performance is also the biggest weakness
for formal reasoning. The permissive memory access model of C, the lack of any reference safety
enforcement, the weak type system and generally little semantic information in the code -- all these
properties that do not allow to make many general assumptions about the code.
properties do not allow to make many general assumptions about the code.
Programming languages which target controlled environments such as Java or C\(\sharp\) are
Programming languages which target controlled environments such as Java and C\(\sharp\) are
generally easier for formal reasoning because they provide a well-known set of primitives
and language constructs for object ownership, threading and synchronization. Many non-imperative
programming languages can be even considered to be a form of ``executable specification'' and thus
273,10 → 273,10
of the term. However, even methods which are based on semi-formal reasoning and non-exhaustive
testing provide some limited guarantees in their specific context. A valued property
of the formal methods is to preserve these limited guarantees even on the higher levels
of abstraction, thus complementing the formal guarantees where the formal methods do not provide
any feasible verification so far. This increases the coverage of the set of all hypothetical
interesting properties of the system (although it is probably impossible to formally define
this set).
of abstraction, thus allowing the semi-formal methods to complement the big picture
where the formal methods do not provide any feasible verification so far. This increases
the coverage of the set of all hypothetical interesting properties of the system (although
it is probably impossible to formally define this entire set).
\medskip
292,7 → 292,7
these decisions can be made by any plain C compiler. However, with the current implementation
of HelenOS even this is not quite trivial.
Besides the requirement to support 7 hardware platforms, the system's compile-time configuration
Besides the requirement to support 7 hardware platforms, the system's com\-pile-time configuration
can be also affected by approximately 65 configuration options, most of which are booleans,
the rest are enumerated types.
433,7 → 433,7
tools use model checkers as their backends, verifying a complete model of the entire
system created by hand seems to be infeasible both in the sense of time required for the model
creation and resources required by the checker to finish the exhaustive traversal of the model's
address space.
state space.
Nevertheless, model checkers on their own can still serve a good job verifying abstract
properties of key algorithms without dealing with the technical details of the implementation.
474,13 → 474,13
compatible. All required interfaces need to be bound to provided interfaces and
the communication between the components cannot lead to \emph{no activity} (a deadlock),
\emph{bad activity} (a livelock) or other communication and synchronization errors.
\item[Vertical compliance] Also called \emph{substituability}. The goal is to check whether
\item[Vertical compliance] Also called \emph{substituability}. The goal is to check whe\-ther
it is possible to replace a set of primitive components that are nested inside a composite
component by the composite component itself. In other words, this compliance can answer the
questions whether the architecture description of the system is sound with respect to the hierarchical
question whether the architecture description of the system is sound with respect to the hierarchical
composition of the components.
\item[Compliance between the specification and the implementation] Using various means
for generating artificial environments for an isolated component the checker is able to
\item[Specification and implementation compliance] Using various means
of generating artificial environments for an isolated component a checker is able to
partially answer the question whether the implementation of the component is an instantiation
of the component specification.
\end{description}
491,7 → 491,7
\end{description}
Unfortunately, most of the behavior and architecture formalisms are static, which is not quite suitable
for the dynamic of most OSes. This limitation can be circumvented by considering a relevant
for the dynamic nature of most OSes. This limitation can be circumvented by considering a relevant
snapshot of the dynamic run-time architecture. This snapshot fixed in time is equivalent to
a statically defined architecture.
557,7 → 557,7
We have spoken only about the functional properties. In general, we cannot apply the same formalisms
and methods on extra-functional properties (e.g. timing properties, performance properties, etc.).
And although it probably does make a good sense to reason about component composition for the extra-functional
And although it probably does make a good sense to reason about component composition for the extra-functi\-onal
properties, the exact relation might be different compared to the functional properties.
The extra-functional properties need to be tackled by our future work.
584,7 → 584,7
of unchecked overflows), the usage of uninitialized variables, the presence of unused local variables,
NULL-pointer dereferencing (determined by conservative local control flow analysis), functions
with non-void return typed that do not return any value and so on. We treat all compilation warnings
as fatal errors, thus the code base must pass without any warnings.
as fatal errors (\texttt{-Werror}), thus the code base must pass without any warnings.
We also turn on several more specific and strict checks. These checks helped to discover several
latent bugs in the source code:
636,9 → 636,6
by the need to support MMU-less architectures in the future. But this framework might be also very helpful
in detecting memory and generic resource leaks. We have not tried \emph{Valgrind}~\cite{valgrind} or any similar
existing tool because of the estimated complexity to adopt it for the usage in HelenOS.
HelenOS was also scanned by \emph{Coverity}~\cite{coverity} in 2006 when no errors were detected. However, since
that time the code base has not been analyzed by Coverity.
\subsection{Static Analyzer}
The integration of various static analyzers into the HelenOS continuous integration process is underway.
649,6 → 646,9
The open framework of Clang seems to be very promising for implementing domain-specific checks (and at
the same time it is also a very promising compiler framework). Our mid-term goal is to incorporate some of the features
of Stanse and VCC (see Section \ref{staticverifier2}) into Clang Analyzer.
HelenOS was also scanned by \emph{Coverity}~\cite{coverity} in 2006 when no errors were detected. However, since
that time the code base has not been analyzed by Coverity.
\subsection{Static Verifier}
\label{staticverifier2}