Subversion Repositories HelenOS-doc

Compare Revisions

Ignore whitespace Rev 182 → Rev 183

/papers/isarcs10/isarcs10.tex
34,7 → 34,7
OSes are usually designed to run on bare hardware. This means that they do not require
any special assumptions on the environment except the assumptions on the properties and
behavior of hardware. In many cases it is perfectly valid to consider the hardware
as \emph{idealized hardware} (zero mathematical probability of failure, perfect compiance
as \emph{idealized hardware} (zero mathematical probability of failure, perfect compliance
with the specifications, etc.). This means that it is solely the OS that defines the
environment for other software.
66,7 → 66,7
The architecture of these major desktop and server OSes is monolithic, which makes
any attempts to do formal verification on them extremely challenging due to the large
state space. Fortunatelly we can observe that aspects of several novel approaches from
state space. Fortunately we can observe that aspects of several novel approaches from
the OS research from the late 1980s and early 1990s (microkernel design, user space
file system and device drivers, etc.) are slowly emerging in these originally purely
monolithic implementations.
80,7 → 80,7
general-purpose OSes.
Our approach is not based on using a single ``silver-bullet'' formalism, methodology or
tool, but on combining various enginering, semi-formal and formal approaches.
tool, but on combining various engineering, semi-formal and formal approaches.
While the lesser formal approaches give lesser guarantees, they can complement
the formal approaches on their boundaries and increase the coverage of the set of
all hypothetical interesting properties of the system.
259,8 → 259,7
\end{figure}
In this section, we analyze the properties we would like to check in a general-purpose
operating system. Each set of properties usually requires a specific verification method,
tool or toolchain.
OS. Each set of properties usually requires a specific verification method, tool or toolchain.
Our approach will be mostly bottom-up, or, in other words, from the lower levels of abstraction
to the higher levels of abstraction. If the verification fails on a lower level, it usually
282,7 → 281,7
\medskip
Please note that the titles of the following sections do not follow any particular established
taxonomy. We have simply chosen the names to be intuitivelly descriptive.
taxonomy. We have simply chosen the names to be intuitively descriptive.
\subsection{C Language Compiler and Continuous Integration Tool}
\label{clang}
414,8 → 413,7
invariants in the code. Many static verifiers also target true multithreaded usage patterns
and have the capability to check proper locking order, hand-over-hand locking and even liveliness.
In the context of an operating system kernel and core libraries two kinds of properties are
common:
In the context of an OS kernel and core libraries two kinds of properties are common:
\begin{description}
\item[Consistency constrains] These properties define the correct way how data is supposed
431,8 → 429,8
\subsection{Model Checker}
\label{modelcheck}
On the first sight it does not seem to be reasonable to consider general model checkers as
relevant independent tools for formal verification of an existing operating system. While many
different tools use model checkers as their backends, verifying a complete model of the entire
relevant independent tools for formal verification of an existing OS. While many different
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.
463,7 → 461,7
It is extremely important to define the right role of the behavior and architecture description.
A flawed approach would be to reverse-engineer this description from the source code (either manually
or via some sophisticated tool) and then verify the compliance between the desciption and
or via some sophisticated tool) and then verify the compliance between the description and
the implementation. However, different directions can give more interesting results:
\begin{description}
501,7 → 499,7
The key features of software systems with respect to behavior and architecture checkers are the granularity
of the individual primitive components, the level of isolation and complexity of the communication mechanism
between them. Large monolithic OSes created in sematic-poor C present a severe challenge because the
between them. Large monolithic OSes created in semantic-poor C present a severe challenge because the
isolation of the individual components is vague and the communication between them is basically unlimited
(function calls, shared resources, etc.).