Subversion Repositories HelenOS-doc

        \label{introduction}

        \label{introduction}

        Operating systems (OSes for short) have a somewhat special position among all software.

        Operating systems (OSes for short) have a somewhat special position among all software.

        OSes are usually designed to run on bare hardware. This means that they do not require

        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

        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

        behavior of hardware. In many cases it is perfectly valid to consider the hardware

        with the specifications, etc.). This means that it is solely the OS that defines the

        with the specifications, etc.). This means that it is solely the OS that defines the

        environment for other software.

        environment for other software.

        OSes represent the lowest software layer and provide services to essentially all other

        OSes represent the lowest software layer and provide services to essentially all other

        software. Considering the principle of recursion, the properties of an OS form the

        software. Considering the principle of recursion, the properties of an OS form the

        segmentation of the desktop and server OSes market is going to change very rapidly

        segmentation of the desktop and server OSes market is going to change very rapidly

        in the near future.

        in the near future.

        The architecture of these major desktop and server OSes is monolithic, which makes

        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

        any attempts to do formal verification on them extremely challenging due to the large

        the OS research from the late 1980s and early 1990s (microkernel design, user space

        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

        file system and device drivers, etc.) are slowly emerging in these originally purely

        monolithic implementations.

        monolithic implementations.

        \medskip

        \medskip

        specifically with formal verification in mind. These design choices can be gradually

        specifically with formal verification in mind. These design choices can be gradually

        introduced (and in fact some of them have already been introduced) to mainstream

        introduced (and in fact some of them have already been introduced) to mainstream

        general-purpose OSes.

        general-purpose OSes.

        Our approach is not based on using a single ``silver-bullet'' formalism, methodology or

        Our approach is not based on using a single ``silver-bullet'' formalism, methodology or

        While the lesser formal approaches give lesser guarantees, they can complement

        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

        the formal approaches on their boundaries and increase the coverage of the set of

        all hypothetical interesting properties of the system.

        all hypothetical interesting properties of the system.

        We also demonstrate work-in-progress case study of an general-purpose research OS

        We also demonstrate work-in-progress case study of an general-purpose research OS

                \label{fig:diag}

                \label{fig:diag}

            \end{center}

            \end{center}

        \end{figure}

        \end{figure}

        In this section, we analyze the properties we would like to check in a general-purpose

        In this section, we analyze the properties we would like to check in a general-purpose

        Our approach will be mostly bottom-up, or, in other words, from the lower levels of abstraction

        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

        to the higher levels of abstraction. If the verification fails on a lower level, it usually

        does not make much sense to continue with the higher levels of abstraction until the issues

        does not make much sense to continue with the higher levels of abstraction until the issues

        are tackled. A structured overview of the formalisms, methods and tools can be seen on

        are tackled. A structured overview of the formalisms, methods and tools can be seen on

        this set).

        this set).

        \medskip

        \medskip

        Please note that the titles of the following sections do not follow any particular established

        Please note that the titles of the following sections do not follow any particular established

        \subsection{C Language Compiler and Continuous Integration Tool}

        \subsection{C Language Compiler and Continuous Integration Tool}

            \label{clang}

            \label{clang}

            The initial levels of abstraction do not go far from the C source code and common engineering

            The initial levels of abstraction do not go far from the C source code and common engineering

            approaches. First, we would certainly like to know whether our code base is compliant with the

            approaches. First, we would certainly like to know whether our code base is compliant with the

            There is one key difference between a static analyzer and a static verifier: Static verifiers

            There is one key difference between a static analyzer and a static verifier: Static verifiers

            allow the user to specify one's own properties, in terms of preconditions, postconditions and

            allow the user to specify one's own properties, in terms of preconditions, postconditions and

            invariants in the code. Many static verifiers also target true multithreaded usage patterns

            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.

            and have the capability to check proper locking order, hand-over-hand locking and even liveliness.

            \begin{description}

            \begin{description}

                \item[Consistency constrains] These properties define the correct way how data is supposed

                \item[Consistency constrains] These properties define the correct way how data is supposed

                      to be manipulated by some related set of subroutines. Checking for these

                      to be manipulated by some related set of subroutines. Checking for these

                      properties ensures that data structures and internal states will not get corrupt due

                      properties ensures that data structures and internal states will not get corrupt due

            \end{description}

            \end{description}

        \subsection{Model Checker}

        \subsection{Model Checker}

            \label{modelcheck}

            \label{modelcheck}

            On the first sight it does not seem to be reasonable to consider general model checkers as

            On the first sight it does not seem to be reasonable to consider general model checkers as

            system created by hand seems to be infeasible both in the sense of time required for the model

            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

            creation and resources required by the checker to finish the exhaustive traversal of the model's

            address space.

            address space.

            Nevertheless, model checkers on their own can still serve a good job verifying abstract

            Nevertheless, model checkers on their own can still serve a good job verifying abstract

            interfaces), composite components (an architectural compositions of primitive components) and the

            interfaces), composite components (an architectural compositions of primitive components) and the

            bindings between the respective interfaces of the components.

            bindings between the respective interfaces of the components.

            It is extremely important to define the right role of the behavior and architecture description.

            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

            A flawed approach would be to reverse-engineer this description from the source code (either manually

            the implementation. However, different directions can give more interesting results:

            the implementation. However, different directions can give more interesting results:

            \begin{description}

            \begin{description}

                \item[Description as specification] Behavior and architecture description created independently

                \item[Description as specification] Behavior and architecture description created independently

                      on the source code serves the role of specification. This has the following primary

                      on the source code serves the role of specification. This has the following primary

            \medskip

            \medskip

            The key features of software systems with respect to behavior and architecture checkers are the granularity

            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

            of the individual primitive components, the level of isolation and complexity of the communication mechanism

            isolation of the individual components is vague and the communication between them is basically unlimited

            isolation of the individual components is vague and the communication between them is basically unlimited

            (function calls, shared resources, etc.).

            (function calls, shared resources, etc.).

            OSes with explicit component architecture and fine-grained components (such as microkernel multiserver

            OSes with explicit component architecture and fine-grained components (such as microkernel multiserver

            systems) make the feasibility of the verification much easier, since the degrees of freedom (and thus

            systems) make the feasibility of the verification much easier, since the degrees of freedom (and thus