Subversion Repositories HelenOS-doc

Rev

Rev 179 | Rev 181 | Go to most recent revision | Only display areas with differences | Ignore whitespace | Details | Blame | Last modification | View Log | RSS feed

Rev 179 Rev 180
1 
\documentclass{llncs}
 1 
\documentclass{llncs}
2 
\usepackage{graphicx}
 2 
\usepackage{graphicx}
3 
 
 3 
 
4 
\title{A Road to a Formally Verified General-Purpose Operating System}
 4 
\title{A Road to a Formally Verified General-Purpose Operating System}
5 
\author{Martin D\v{e}ck\'{y}}
 5 
\author{Martin D\v{e}ck\'{y}}
6 
\institute{Department of Software Engineering\\
 6 
\institute{Department of Distributed and Dependable Systems\\
7 
        Faculty of Mathematics and Physics, Charles University\\
 7 
        Faculty of Mathematics and Physics, Charles University\\
8 
        Malostransk\'{e} n\'{a}m\v{e}st\'{i} 25, Prague 1, 118~00, Czech Republic\\
 8 
        Malostransk\'{e} n\'{a}m\v{e}st\'{i} 25, Prague 1, 118~00, Czech Republic\\
9 
        \email{martin.decky@dsrg.mff.cuni.cz}}
 9 
        \email{martin.decky@d3s.mff.cuni.cz}}
10 
 
 10 
 
11 
\begin{document}
 11 
\begin{document}
12 
    \maketitle
 12 
    \maketitle
13 
   
 13 
   
14 
    \begin{abstract}
 14 
    \begin{abstract}
15 
        Methods of formal description and verification represent a viable way for achieving
 15 
        Methods of formal description and verification represent a viable way for achieving
16 
        fundamentally bug-free software. However, in reality only a small subset of the existing operating
 16 
        fundamentally bug-free software. However, in reality only a small subset of the existing operating
17 
        systems were ever formally verified, despite the fact that an operating system is a critical part
 17 
        systems were ever formally verified, despite the fact that an operating system is a critical part
18 
        of almost any other software system. This paper summarizes the challenges involved in formal verification
 18 
        of almost any other software system. This paper points out several key design choices which
19 
        of operating systems, points out several key design choices which should make the formal verification
 19 
        should make the formal verification of an operating system easier and presents a work-in-progress
20 
        easier and presents a work-in-progress and initial experiences with formal verification of HelenOS,
 20 
        and initial experiences with formal verification of HelenOS, a state-of-the-art microkernel-based
21 
        a state-of-the-art microkernel-based operating system, which, however, was not designed specifically
 21 
        operating system, which, however, was not designed specifically with formal verification in mind,
22 
        with formal verification in mind, as this is mostly prohibitive due to time and budget constrains.
 22 
        as this is mostly prohibitive due to time and budget constrains.
23 
       
 23 
       
24 
        The contribution of this paper is the shift of focus from attempts to use a single ``silver-bullet''
 24 
        The contribution of this paper is the shift of focus from attempts to use a single ``silver-bullet''
25 
        formal verification method which would be able to verify everything to a combination of multiple
 25 
        formal verification method which would be able to verify everything to a combination of multiple
26 
        formalisms and techniques to cover various aspects of the verification process. The formally verified
 26 
        formalisms and techniques to successfully cover various aspects of the operating system.
27 
        operating system is the emerging property of the combination.
 27 
        A reliable and dependable operating system is the emerging property of the combination,
- 
 
 28 
        thanks to the suitable architecture of the operating system.
28 
    \end{abstract}
 29 
    \end{abstract}
29 
   
 30 
   
30 
    \section{Introduction}
 31 
    \section{Introduction}
31 
        \label{introduction}
 32 
        \label{introduction}
32 
        In the context of formal verification of software, it is always important to model the outer
 33 
        Operating systems (OSes for short) have a somewhat special position among all software.
33 
        environment with a proper level of abstraction. Weak assumptions on the environment make the formal
 - 
 
34 
        verification less feasible, because they yield many degrees of freedom which render
 34 
        OSes are usually designed to run on bare hardware. This means that they do not require
35 
        the properties which we want to verify overly complex. But strong assumptions on the environment are likewise
 35 
        any special assumptions on the environment except the assumptions on the properties and
36 
        not without a price: Any practical usability of the verification results depends on the question
 36 
        behavior of hardware. In many cases it is perfectly valid to consider the hardware
37 
        whether we are really able to create a physical environment which satisfies the assumptions.
 37 
        as \emph{idealized hardware} (zero mathematical probability of failure, perfect compiance
38 
       
 - 
 
39 
        There are some assumptions which are universal for any formal verification method. For the sake of
 38 
        with the specifications, etc.). This means that it is solely the OS that defines the
40 
        simplicity let us call them \emph{idealized hardware}. Let us also cover the computational model
 - 
 
41 
        and basic mathematical principles by this term.
 39 
        environment for other software.
42 
       
 40 
       
43 
        What is \emph{idealized hardware}? We usually assume that the software is executed by a ``perfect'' hardware
 41 
        OSes represent the lowest software layer and provide services to essentially all other
44 
        which works exactly according to its specification. Every divergence between the intended and actual
 42 
        software. Considering the principle of recursion, the properties of an OS form the
45 
        behavior of software counts as a software bug and never as an issue in some hardware component. We
 43 
        assumptions for the upper layers of software. Thus the dependability of end-user and
46 
        implicitly assume that the hardware is perfect in the sense of physical realization and all probabilities
 - 
 
47 
        of accidental mechanical and electrical failures are expected to be zero.
 44 
        enterprise software systems is always limited by the dependability of the OS.
48 
       
 45 
       
49 
        It is trivial to see that the \emph{idealized hardware} assumptions can never hold in real world.
 - 
 
50 
        Accidental mechanical and electrical failures are inevitable in principle and their probability can
 46 
        Finally, OSes are non-trivial software on their own. The way they are generally designed
51 
        never be a mathematical zero. Does this mean that any formal verification method is ultimately futile
 47 
        and programmed (spanning both the kernel and user mode, manipulating execution contexts
52 
        since we are unable to ensure validity of the most elementary assumptions? Probably not. We just need
 48 
        and concurrency, handling critical hardware-related operations) represent significant
53 
        to be aware about the inherent and fundamental limitations of the formal methods which result from
 - 
 
54 
        the shortcomings of the physical world.
 49 
        and interesting challenges for software analysis.
55 
       
 - 
 
56 
        The more precisely we model the software environment of the software under discussion, the more precisely
 - 
 
57 
        we can calculate or estimate the resulting impact of the imperfections of the physical world on our software
 - 
 
58 
        system. This is the most important motivation for formal reasoning about the correctness of the operating system.
 - 
 
59 
       
 50 
       
60 
        \medskip
 51 
        \medskip
61 
       
 52 
       
62 
        In more detail, operating systems have a somewhat special position among all software:
 - 
 
63 
       
 - 
 
64 
        \begin{itemize}
 - 
 
65 
            \item \emph{Operating systems are usually designed to run on bare hardware.} This means that except
 - 
 
66 
                  the \emph{idealized hardware} assumptions we do not have to take any or almost any extra assumptions
 - 
 
67 
                  into account.
 - 
 
68 
            \item \emph{Operating systems create the lowest software layer and provide services to essentially
 53 
        These are probably the most important reasons that led to several research initiatives
69 
                  all other software.} Considering the principle of recursion, the properties of the
 - 
 
70 
                  operating systems which we prove or disprove form the assumptions for the upper layers
 54 
        in the recent years which target the creation of a formally verified OSes from scratch
71 
                  of software. Thus the dependability of end-user and enterprise software systems is limited
 - 
 
72 
                  by the dependability of the operating system.
 - 
 
73 
            \item \emph{Operating systems are non-trivial software on their own.} The way
 55 
        (e.g. \cite{seL4}). Methods of formal description and verification provide fundamentally
74 
                  they are generally designed and programmed (spanning both the kernel and user mode,
 56 
        better guarantees of desirable properties than non-exhaustive engineering methods such
75 
                  manipulating execution contexts and concurrency, handling critical hardware-related
 - 
 
76 
                  operations) represent significant and interesting challenges for the formal verification
 - 
 
77 
                  methods and tools.
 - 
 
78 
        \end{itemize}
 57 
        as testing.
79 
       
 58 
       
80 
        Even in the informal understanding, the dependability of an operating system greatly determines the perceived
 59 
        However, 98~\%\footnote{98~\% of client computers connected to the Internet as of January
81 
        dependability of the entire software stack. This led to several research initiatives in the recent years
 60 
        2010~\cite{marketshare}.} of the market share of general-purpose OSes is taken
82 
        which target the creation of a formally verified operating systems from scratch~\cite{seL4}.
 - 
 
83 
       
 - 
 
84 
        However, 98~\%\footnote{98~\% of client computers connected to the Internet as of January 2010~\cite{marketshare}.} of
 - 
 
85 
        the market share of general-purpose operating systems is taken by Windows, Mac~OS~X and Linux.
 61 
        by Windows, Mac~OS~X and Linux. These systems were clearly not designed with formal
86 
        These systems were clearly not designed with formal verification in mind from the very beginning.
 62 
        verification in mind from the very beginning. The situation on the embedded, real-time
87 
        The situation on the embedded, real-time and special-purpose operating systems market is probably different,
 63 
        and special-purpose OSes market is probably different, but it is unlikely that the
88 
        but it is unlikely that the situation in the large domain of desktops and servers is going to change
 64 
        segmentation of the desktop and server OSes market is going to change very rapidly
89 
        very rapidly in the near future.
 65 
        in the near future.
90 
       
 66 
       
91 
        Therefore we need to face the challenges of applying formal methods on an existing code base in the domain
 67 
        The architecture of these major desktop and server OSes is monolithic, which makes
92 
        of general-purpose operating systems. Fortunately, the software design qualities of the general-purpose
 68 
        any attempts to do formal verification on them extremely challenging due to the large
93 
        operating systems gradually improve over time. We can see then novel approaches in the operating systems
 69 
        state space. Fortunatelly we can observe that aspects of several novel approaches from
94 
        research from the late 1980s and 1990s (microkernel design, user space file system and device drivers, etc.)
 70 
        the OS research from the late 1980s and early 1990s (microkernel design, user space
95 
        to slowly emerge in the originally monolithic operating systems. We can also see better code quality thanks
 71 
        file system and device drivers, etc.) are slowly emerging in these originally purely
96 
        to improved software engineering (code review, proper escalation management, etc.).
 72 
        monolithic implementations.
97 
       
 73 
       
98 
        \medskip
 74 
        \medskip
99 
       
 75 
       
100 
        This paper proposes an approach and presents a work-in-progress case study of formal verification
 76 
        In this paper we show how specific design choices can markedly improve the feasibility
101 
        of an general-purpose research operating system, which was also not created specifically with formal
 77 
        of verification of an OS, even if the particular OS was not designed
102 
        verification in mind from the very beginning, but it was designed according to state-of-the-art operating systems
 78 
        specifically with formal verification in mind. These design choices can be gradually
- 
 
 79 
        introduced (and in fact some of them have already been introduced) to mainstream
103 
        principles.
 80 
        general-purpose OSes.
- 
 
 81 
       
- 
 
 82 
        Our approach is not based on using a single ``silver-bullet'' formalism, methodology or
- 
 
 83 
        tool, but on combining various enginering, semi-formal and formal approaches.
- 
 
 84 
        While the lesser formal approaches give lesser guarantees, they can complement
- 
 
 85 
        the formal approaches on their boundaries and increase the coverage of the set of
- 
 
 86 
        all hypothetical interesting properties of the system.
- 
 
 87 
       
- 
 
 88 
        We also demonstrate work-in-progress case study of an general-purpose research OS
- 
 
 89 
        that was not created specifically with formal verification in mind from the very
- 
 
 90 
        beginning, but that was designed according to state-of-the-art OS principles.
104 
       
 91 
       
105 
        \medskip
 92 
        \medskip
106 
       
 93 
       
107 
        \noindent\textbf{Structure of the Paper.} In Section \ref{context} we introduce the case study in more detail and explain
 94 
        \noindent\textbf{Structure of the Paper.} In Section \ref{design} we introduce
108 
        why we believe it is relevant. In Section \ref{analysis} we discuss our proposal of the combination of formal methods
 95 
        the design choices and our case study in more detail. In Section \ref{analysis} we
109 
        and tools. In Section \ref{evaluation} we present the preliminary evaluation of our efforts and estimate the complexity
 96 
        discuss our approach of the combination of methods and tools. In Section \ref{evaluation}
110 
        of the imminent next steps we want to take according to our proposal. Finally, in Section \ref{conclusion}
 97 
        we present a preliminary evaluation of our efforts and propose the imminent next steps
111 
        we present the conclusion of the paper.
 98 
        to take. Finally, in Section \ref{conclusion} we present the conclusion of the paper.
112 
   
 99 
   
113 
    \section{Context}
 100 
    \section{Operating Systems Design}
114 
        \label{context}
 101 
        \label{design}
115 
        Two very common schemes of operating system design are \emph{monolithic design} and \emph{microkernel design}.
 102 
        Two very common schemes of OS design are \emph{monolithic design} and \emph{microkernel design}.
116 
        Without going into much detail of any specific operating system, we can define the monolithic design as
 103 
        Without going into much detail of any specific implementation, we can define the monolithic design as
117 
        a preference to put numerous aspects of the core operating system functionality into the kernel,
 104 
        a preference to put numerous aspects of the core OS functionality into the kernel, while microkernel
118 
        while microkernel design is a preference to keep the kernel small, with just a minimal set of features.
 105 
        design is a preference to keep the kernel small, with just a minimal set of features.
119 
       
 106 
       
120 
        The features which are missing from the kernel in the microkernel design are implemented in user space, usually
 107 
        The features which are missing from the kernel in the microkernel design are implemented
121 
        by means of libraries, servers and/or software components.
 108 
        in user space, usually by means of libraries, servers (e.g. processes/tasks) and/or software components.
122 
       
 109 
       
123 
        \subsection{HelenOS}
 110 
        \subsection{HelenOS}
124 
            \label{helenos}
 111 
            \label{helenos}
125 
            \emph{HelenOS} is a general-purpose research operating system which is being developed at Charles
 112 
            \emph{HelenOS} is a general-purpose research OS which is being developed at Charles
126 
            University in Prague. The source code is available under the BSD open source license and can be
 113 
            University in Prague. The source code is available under the BSD open source license and can be
127 
            freely downloaded from the project web site~\cite{helenos}. The authors of the code base are
 114 
            freely downloaded from the project web site~\cite{helenos}. The authors of the code base are
128 
            both from the academia and from the open source community (several contributors are employed
 115 
            both from the academia and from the open source community (several contributors are employed
129 
            as Solaris kernel developers and many are freelance IT professionals). We consistently strive to support
 116 
            as Solaris kernel developers and many are freelance IT professionals).
130 
            the research and also the practical motivations for developing the system.
 - 
 
131 
           
 117 
           
132 
            HelenOS uses a preemptive priority-feedback scheduler, it supports SMP hardware and it is
 118 
            HelenOS uses a preemptive priority-feedback scheduler, it supports SMP hardware and it is
133 
            designed to be highly portable. Currently it runs on 7 distinct hardware architectures, including the
 119 
            designed to be highly portable. Currently it runs on 7 distinct hardware architectures, including the
134 
            most common IA-32, x86-64 (AMD64), IA-64, SPARC~v9 and PowerPC. It also runs on ARMv7 and MIPS,
 120 
            most common IA-32, x86-64 (AMD64), IA-64, SPARC~v9 and PowerPC. It also runs on ARMv7 and MIPS,
135 
            but currently only in simulators and not on physical hardware.
 121 
            but currently only in simulators and not on physical hardware.
136 
           
 122 
           
137 
            Although HelenOS is still far from being an everyday replacement for Linux or Windows due to the lack
 123 
            Although HelenOS is still far from being an everyday replacement for Linux or Windows due to the lack
138 
            of end-user applications (whose development is extremely time-consuming, but unfortunately of
 124 
            of end-user applications (whose development is extremely time-consuming, but unfortunately of
139 
            no scientific value), the essential foundations such as file system support and TCP/IP networking
 125 
            no scientific value), the essential foundations such as file system support and TCP/IP networking
140 
            are already in place.
 126 
            are already in place.
141 
           
 127 
           
142 
            HelenOS does not currently target embedded devices (although the ARMv7 port can be easily modified to
 128 
            HelenOS does not currently target embedded devices (although the ARMv7 port can be very easily
143 
            run on various embedded boards) and does not implement real-time scheduling and synchronization.
 129 
            modified to run on various embedded boards) and does not implement real-time features.
144 
            Many development projects such as task snapshoting and migration, generic device driver
 130 
            Many development projects such as task snapshoting and migration, support for MMU-less
145 
            framework, support for MMU-less platforms and performance monitoring are currently underway.
 131 
            platforms and performance monitoring are currently underway.
146 
           
 132 
           
147 
            \medskip
 133 
            \medskip
148 
           
 134 
           
149 
            HelenOS has a microkernel multiserver design, but the guiding principles of the HelenOS design are
 135 
            HelenOS can be briefly described as microkernel multiserver design. However, the actual design
150 
            actually more elaborate:
 136 
            guiding principles of the HelenOS are more elaborate:
151 
           
 137 
           
152 
            \begin{itemize}
 138 
            \begin{description}
153 
                \item \emph{(Microkernel principle)} Every functionality of the operating system that does not
 139 
                \item[Microkernel principle] Every functionality of the OS that does not
154 
                      have to be necessary implemented in the kernel should be implemented in user space. This
 140 
                      have to be necessary implemented in the kernel should be implemented in user space. This
155 
                      implies that subsystems such as the file system, device drivers (except those which are
 141 
                      implies that subsystems such as the file system, device drivers (except those which are
156 
                      essential for the basic kernel functionality), naming and trading services, networking,
 142 
                      essential for the basic kernel functionality), naming and trading services, networking,
157 
                      human interface and similar features should be implemented in user space.
 143 
                      human interface and similar features should be implemented in user space.
158 
                \item \emph{(Full-fledged principle)} Features which need to be implemented in kernel should
 144 
                \item[Full-fledged principle] Features which need to be placed in kernel should
159 
                      be designed with full-fledged algorithms and data structures. In contrast
 145 
                      be implemented by full-fledged algorithms and data structures. In contrast
160 
                      to several other microkernel operating systems, where the authors have deliberately chosen
 146 
                      to several other microkernel OSes, where the authors have deliberately chosen
161 
                      the most simplistic approach (static memory allocation, na\"{\i}ve algorithms, simple data
 147 
                      the most simplistic approach (static memory allocation, na\"{\i}ve algorithms, simple data
162 
                      structures), HelenOS microkernel tries to use the most advanced and suitable means available.
 148 
                      structures), HelenOS microkernel tries to use the most advanced and suitable means available.
163 
                      It contains features such as AVL and B+ trees, hashing tables, SLAB memory allocator, multiple
 149 
                      It contains features such as AVL and B+ trees, hashing tables, SLAB memory allocator, multiple
164 
                      in-kernel synchronization primitives, fine-grained locking and so on.
 150 
                      in-kernel synchronization primitives, fine-grained locking and so on.
165 
                \item \emph{(Multiserver principle)} Subsystems in user space should be decomposed with the smallest
 151 
                \item[Multiserver principle] Subsystems in user space should be decomposed with the smallest
166 
                      reasonable granularity. Each unit of decomposition should be encapsulated in a separate task.
 152 
                      reasonable granularity. Each unit of decomposition should be encapsulated in a separate task.
167 
                      The tasks represent software components with isolated address spaces. From the design point of
 153 
                      The tasks represent software components with isolated address spaces. From the design point of
168 
                      view the kernel can be seen as a separate component, too.
 154 
                      view the kernel can be seen as a separate component, too.
169 
                \item \emph{(Split of mechanism and policy)} The kernel should only provide low-level mechanisms,
 155 
                \item[Split of mechanism and policy] The kernel should only provide low-level mechanisms,
170 
                      while the high-level policies which are built upon these mechanisms should be defined in
 156 
                      while the high-level policies which are built upon these mechanisms should be defined in
171 
                      user space. This also implies that the policies should be easily replaceable while keeping
 157 
                      user space. This also implies that the policies should be easily replaceable while keeping
172 
                      the low-level mechanisms intact.
 158 
                      the low-level mechanisms intact.
173 
                \item \emph{(Encapsulation principle)} The communication between the tasks/components should be
 159 
                \item[Encapsulation principle] The communication between the tasks/components should be
174 
                      implemented only via a set of well-defined interfaces. In the user-to-user case the preferred
 160 
                      implemented only via a set of well-defined interfaces. In the user-to-user case the preferred
175 
                      communication mechanism is HelenOS IPC, which provides reasonable mix of abstraction and
 161 
                      communication mechanism is HelenOS IPC, which provides reasonable mix of abstraction and
176 
                      performance (RPC-like primitives combined with implicit memory sharing for large data
 162 
                      performance (RPC-like primitives combined with implicit memory sharing for large data
177 
                      transfers). In case of synchronous user-to-kernel communication the usual syscalls are used.
 163 
                      transfers). In case of synchronous user-to-kernel communication the usual syscalls are used.
178 
                      HelenOS IPC is used again for asynchronous kernel-to-user communication.
 164 
                      HelenOS IPC is used again for asynchronous kernel-to-user communication.
179 
                \item \emph{(Portability principle)} The design and implementation should always maintain a high
 165 
                \item[Portability principle] The design and implementation should always maintain a high
180 
                      level of platform neutrality and portability. Platform-specific code in the kernel, core
 166 
                      level of platform neutrality and portability. Platform-specific code in the kernel, core
181 
                      libraries and tasks implementing low-level functionality (e.g. device drivers) should be
 167 
                      libraries and tasks implementing device drivers should be clearly separated from the
182 
                      clearly separated from the generic code (either by component decomposition, naming and trading,
 - 
 
183 
                      or at least by internal compile-time APIs).
 168 
                      generic code (either by component decomposition or at least by internal compile-time APIs).
184 
            \end{itemize}
 169 
            \end{description}
185 
           
 170 
           
186 
            As these design guiding principles suggest, the size of the HelenOS microkernel is considerably larger
 171 
            In Section \ref{analysis} we argue that several of these design principles significantly improve
187 
            compared to ``scrupulous'' microkernel implementations. The average footprint of the kernel ranges from
 - 
 
188 
            569~KiB when all logging messages, asserts, symbol resolution and debugging kernel console are compiled
 - 
 
189 
            in, down to 198~KiB for a non-debugging production build. We do not believe that the raw size
 172 
            the feasibility of formal verification of the entire system. On the other hand, other design principles
190 
            of the microkernel is a relevant quality criterion per se, without taking the actual feature set
 173 
            induce new interesting challenges for formal description and verification.
191 
            into account.
 - 
 
192 
           
 - 
 
193 
            \medskip
 - 
 
194 
           
 174 
           
195 
            The run-time architecture of HelenOS is inherently dynamic. The bindings between the components are
 175 
            The run-time architecture of HelenOS is inherently dynamic. The bindings between the components are
196 
            not created at compile-time, but during the bootstrap process and can be modified to a large degree
 176 
            not created at compile-time, but during bootstrap and can be modified to a large degree also during
197 
            also during normal operation mode of the system (via human interaction and external events). This
 177 
            normal operation mode of the system (via human interaction and external events).
198 
            creates particularly interesting challenges for describing the design of the system by many formalisms.
 - 
 
199 
           
 178 
           
200 
            \medskip
 - 
 
201 
           
 - 
 
202 
            Yet another set of obstacles for reasoning about the properties of HelenOS lies in the design of
 179 
            The design of the ubiquitous HelenOS IPC mechanism and the associated threading model present
203 
            the ubiquitous HelenOS IPC mechanism and the associated threading model. The IPC is inherently
 180 
            the possibility to significantly reduce the size of the state space which needs to be explored
- 
 
 181 
            by formal verification tools, but at the same time it is quite hard to express these
204 
            asynchronous with constant message buffers in the kernel and dynamic buffers in user space.
 182 
            constrains in many formalisms. The IPC is inherently asynchronous with constant message buffers
- 
 
 183 
            in the kernel and dynamic buffers in user space. It uses the notions of uni-directional bindings,
205 
            It uses the notions of uni-directional bindings, mandatory pairing of requests and replies,
 184 
            mandatory pairing of requests and replies, binding establishment and abolishment handshakes,
206 
            binding establishment and abolishment handshakes, memory sharing and fast message forwarding.
 185 
            memory sharing and fast message forwarding.
207 
           
 186 
           
208 
            For easier management of the asynchronous messages and the possibility to process multiple
 187 
            For easier management of the asynchronous messages and the possibility to process multiple
209 
            messages from different peers without the usual kernel threading overhead, the core user space
 188 
            messages from different peers without the usual kernel threading overhead, the core user space
210 
            library manages the execution flow by so-called \emph{fibrils}. A fibril is a user-space-managed thread with
 189 
            library manages the execution flow by so-called \emph{fibrils}. A fibril is a user-space-managed
211 
            cooperative scheduling. A different fibril is scheduled every time the current fibril is
 190 
            thread with cooperative scheduling. A different fibril is scheduled every time the current fibril
212 
            about to be blocked while sending out IPC requests (because the kernel buffers of the addressee
 191 
            is about to be blocked while sending out IPC requests (because the kernel buffers of the addressee
213 
            are full) or while waiting on an IPC reply. This allows different execution flows within the
 192 
            are full) or while waiting on an IPC reply. This allows different execution flows within the
214 
            same thread to process multiple requests and replies. To safeguard proper sequencing
 193 
            same thread to process multiple requests and replies. To safeguard proper sequencing of IPC
215 
            of IPC messages and provide synchronization, special fibril-aware synchronization primitives
 194 
            messages and provide synchronization, special fibril-aware synchronization primitives
216 
            (mutexes, condition variables, etc.) are available.
 195 
            (mutexes, condition variables, etc.) are available.
217 
           
 196 
           
218 
            Because of the cooperative nature of fibrils, they might cause severe performance under-utilization
 197 
            Because of the cooperative nature of fibrils, they might cause severe performance under-utilization
219 
            in SMP configurations and system-wide bottlenecks. As multicore processors are more and more
 198 
            in SMP configurations and system-wide bottlenecks. As multicore processors are more and more
220 
            common nowadays, that would be a substantial design flaw. Therefore the fibrils can be also freely
 199 
            common nowadays, that would be a substantial design flaw. Therefore the fibrils can be also freely
221 
            (and to some degree even automatically) combined with the usual kernel threads, which provide
 200 
            (and to some degree even automatically) combined with the usual kernel threads, which provide
222 
            preemptive scheduling and true parallelism on SMP machines. Needless to say, this combination is
 201 
            preemptive scheduling and true parallelism on SMP machines. Needless to say, this combination is
223 
            also a grand challenge for the formal reasoning.
 202 
            also a grand challenge for the formal reasoning.
224 
           
 203 
           
225 
            \medskip
 204 
            \medskip
226 
           
 205 
           
- 
 
 206 
            Incidentally, the \emph{full-fledged principle} causes that the size of the HelenOS microkernel is
- 
 
 207 
            considerably larger compared to other ``scrupulous'' microkernel implementations. The average
- 
 
 208 
            footprint of the kernel on IA-32 ranges from 569~KiB when all logging messages, asserts, symbol
- 
 
 209 
            resolution and the debugging kernel console are compiled in, down to 198~KiB for a non-debugging
- 
 
 210 
            production build. But we do not believe that the raw size of the microkernel is a relevant quality
- 
 
 211 
            criterion per se, without taking the actual feature set into account.
- 
 
 212 
           
- 
 
 213 
            \medskip
- 
 
 214 
           
227 
            To sum up, the choice of HelenOS as our case study is based on the fact that it was not designed
 215 
            To sum up, the choice of HelenOS as our case study is based on the fact that it was not designed
228 
            in advance with formal verification in mind. This is similar to most general-purpose operating
 216 
            in advance with formal verification in mind (some of the design principles might be beneficial,
229 
            systems in common use. At the same time, it does not have an obsolete design and is non-trivial.
 217 
            but others might be disadvantageous), but the design of HelenOS is also non-trivial and not obsolete.
230 
           
 218 
           
231 
        \subsection{The C Programming Language}
 219 
        \subsection{The C Programming Language}
232 
            A large majority of operating systems is coded in the C programming language. HelenOS is no exception
 220 
            A large majority of OSes is coded in the C programming language (HelenOS is no exception
233 
            to this. The choice of C in the case of kernel is usually well-motivated -- the language was designed
 221 
            to this). The choice of C in the case of kernel is usually well-motivated, since the C language was designed
234 
            specifically for implementing system software~\cite{c}. It is reasonably low-level in the sense that it allows
 222 
            specifically for implementing system software~\cite{c}: It is reasonably low-level in the sense that it allows
235 
            to access the memory and other hardware resources with similar effectiveness as from assembler.
 223 
            to access the memory and other hardware resources with similar effectiveness as from assembler;
236 
            It also requires almost no run-time support and it exports many features of the von Neumann hardware
 224 
            It also requires almost no run-time support and it exports many features of the von Neumann hardware
237 
            architecture to the programmer in a very straightforward, but still relatively portable way.
 225 
            architecture to the programmer in a very straightforward, but still relatively portable way.
238 
           
 226 
           
239 
            However, what is the biggest advantage of C in terms of run-time performance is also the biggest weakness
 227 
            However, what is the biggest advantage of C in terms of run-time performance is also the biggest weakness
240 
            for formal reasoning. The permissive memory access model of C, the lack of any reference safety
 228 
            for formal reasoning. The permissive memory access model of C, the lack of any reference safety
241 
            enforcement, the weak type system and generally little semantic information in the code -- all these
 229 
            enforcement, the weak type system and generally little semantic information in the code -- all these
242 
            properties do not allow to make many general assumptions about the code.
 230 
            properties that do not allow to make many general assumptions about the code.
243 
           
 231 
           
244 
            Programming languages which target controlled environments such as Java or C\(\sharp\) are
 232 
            Programming languages which target controlled environments such as Java or C\(\sharp\) are
245 
            generally easier for formal reasoning because they provide a well-known set of primitives
 233 
            generally easier for formal reasoning because they provide a well-known set of primitives
246 
            and language constructs for object ownership, threading and synchronization. Many non-imperative
 234 
            and language constructs for object ownership, threading and synchronization. Many non-imperative
247 
            programming languages can be even considered to be a form of ``executable specification'' and thus
 235 
            programming languages can be even considered to be a form of ``executable specification'' and thus
248 
            very suitable for formal reasoning. In C, almost everything is left to the programmer who
 236 
            very suitable for formal reasoning. In C, almost everything is left to the programmer who
249 
            is free to set the rules.
 237 
            is free to set the rules.
250 
           
 238 
           
251 
            \medskip
 239 
            \medskip
252 
           
 240 
           
253 
            The reasons for using C in the user space of HelenOS (and other established operating systems) is
 241 
            The reasons for frequent use of C in the user space of many established OSes (and HelenOS) is
254 
            probably much more questionable. Except for the core libraries and services (such as device drivers),
 242 
            probably much more questionable. In the case of HelenOS, except for the core libraries and tasks
255 
            C might be easily replaced by any high-level and perhaps even non-imperative programming language.
 243 
            (such as device drivers), C might be easily replaced by any high-level and perhaps even
256 
            The reasons for using C in this context is mostly historical.
 244 
            non-imperative programming language. The reasons for using C in this context are mostly historical.
257 
           
 245 
           
258 
            However, as we have stated in Section \ref{introduction}, the way general-purpose operating systems
 246 
            However, as we have stated in Section \ref{introduction}, the way general-purpose OSes
259 
            are implemented changes only slowly and therefore any propositions which require radical modification
 247 
            are implemented changes only slowly and therefore any propositions which require radical modification
260 
            of the existing code base before committing to the formal verification are not realistic.
 248 
            of the existing code base before committing to the formal verification are not realistic.
261 
       
 249 
       
262 
    \section{Analysis}
 250 
    \section{Analysis}
263 
        \label{analysis}
 251 
        \label{analysis}
264 
       
 252 
       
265 
        \begin{figure}[t]
 253 
        \begin{figure}[t]
266 
            \begin{center}
 254 
            \begin{center}
267 
                \resizebox*{120mm}{!}{\includegraphics{diag}}
 255 
                \resizebox*{120mm}{!}{\includegraphics{diag}}
268 
                \caption{Overview of the formalisms and tools proposed.}
 256 
                \caption{Overview of the formalisms and tools proposed.}
269 
                \label{fig:diag}
 257 
                \label{fig:diag}
270 
            \end{center}
 258 
            \end{center}
271 
        \end{figure}
 259 
        \end{figure}
272 
       
 260 
       
273 
        In this section, we analyze the properties we would like to check in a general-purpose
 261 
        In this section, we analyze the properties we would like to check in a general-purpose
274 
        operating system. Each set of properties usually requires a specific verification method,
 262 
        operating system. Each set of properties usually requires a specific verification method,
275 
        tool or toolchain.
 263 
        tool or toolchain.
276 
       
 264 
       
277 
        Our approach will be mostly bottom-to-top, or, in other words, from the lower levels of abstraction
 265 
        Our approach will be mostly bottom-up, or, in other words, from the lower levels of abstraction
278 
        to the higher levels of abstraction. If the verification fails on a lower level, it usually
 266 
        to the higher levels of abstraction. If the verification fails on a lower level, it usually
279 
        does not make much sense to continue with the higher levels of abstraction until the issues
 267 
        does not make much sense to continue with the higher levels of abstraction until the issues
280 
        are tackled. A structured overview of the formalisms and tools can be seen on Figure \ref{fig:diag}.
 268 
        are tackled. A structured overview of the formalisms, methods and tools can be seen on
- 
 
 269 
        Figure \ref{fig:diag}.
- 
 
 270 
       
- 
 
 271 
        \medskip
- 
 
 272 
       
- 
 
 273 
        Some of the proposed methods cannot be called ``formal methods'' in the rigorous understanding
- 
 
 274 
        of the term. However, even methods which are based on semi-formal reasoning and non-exhaustive
- 
 
 275 
        testing provide some limited guarantees in their specific context. A valued property
- 
 
 276 
        of the formal methods is to preserve these limited guarantees even on the higher levels
- 
 
 277 
        of abstraction, thus complementing the formal guarantees where the formal methods do not provide
- 
 
 278 
        any feasible verification so far. This increases the coverage of the set of all hypothetical
- 
 
 279 
        interesting properties of the system (although it is probably impossible to formally define
- 
 
 280 
        this set).
- 
 
 281 
       
- 
 
 282 
        \medskip
281 
       
 283 
       
282 
        Please note that the titles of the following sections do not follow any particular established
 284 
        Please note that the titles of the following sections do not follow any particular established
283 
        taxonomy of verification methods. We have simply chosen the names to be descriptive.
 285 
        taxonomy. We have simply chosen the names to be intuitivelly descriptive.
284 
       
 286 
       
285 
        \subsection{C Language Compiler and Continuous Integration Tool}
 287 
        \subsection{C Language Compiler and Continuous Integration Tool}
286 
            \label{clang}
 288 
            \label{clang}
287 
            The initial levels of abstraction do not go far from the C source code. First, we would certainly like to
 289 
            The initial levels of abstraction do not go far from the C source code. First, we would certainly like to
288 
            know whether our code base is compliant with the programming language specification and passes
 290 
            know whether our code base is compliant with the programming language specification and passes
289 
            only the basic semantic checks (proper number and types of arguments passed to functions, etc.).
 291 
            only the basic semantic checks (proper number and types of arguments passed to functions, etc.).
290 
            It is perhaps not very surprising that these decisions can be make by any plain C compiler.
 292 
            It is perhaps not very surprising that these decisions can be make by any plain C compiler.
291 
            However, with the current implementation of HelenOS even this is not quite trivial.
 293 
            However, with the current implementation of HelenOS even this is not quite trivial.
292 
            Besides the requirement to support 7 hardware platforms, the system's compile-time configuration
 294 
            Besides the requirement to support 7 hardware platforms, the system's compile-time configuration
293 
            can be also affected by approximately 65 configuration options, most of which are booleans, the rest
 295 
            can be also affected by approximately 65 configuration options, most of which are booleans, the rest
294 
            are enumerated types.
 296 
            are enumerated types.
295 
           
 297 
           
296 
            These configuration options are bound by logical propositions in conjunctive or disjunctive
 298 
            These configuration options are bound by logical propositions in conjunctive or disjunctive
297 
            normal forms and while some options are freely configurable, the value of others gets inferred
 299 
            normal forms and while some options are freely configurable, the value of others gets inferred
298 
            by the build system of HelenOS. Thus, the overall number of distinct configurations in which
 300 
            by the build system of HelenOS. Thus, the overall number of distinct configurations in which
299 
            HelenOS can be compiled is at least one order of magnitude larger than the plain number
 301 
            HelenOS can be compiled is at least one order of magnitude larger than the plain number
300 
            of supported hardware platforms.
 302 
            of supported hardware platforms.
301 
           
 303 
           
302 
            Various configuration options affect conditional compilation and linking. The programmers
 304 
            Various configuration options affect conditional compilation and linking. The programmers
303 
            are used to make sure that the source code compiles and links fine with respect to the
 305 
            are used to make sure that the source code compiles and links fine with respect to the
304 
            most common and obvious configurations, but the unforeseen interaction of the less common
 306 
            most common and obvious configurations, but the unforeseen interaction of the less common
305 
            configuration options might cause linking or even compilation errors.
 307 
            configuration options might cause linking or even compilation errors.
306 
           
 308 
           
307 
            \medskip
 309 
            \medskip
308 
           
 310 
           
309 
            A straightforward solution is to generate all distinct configurations, starting from the
 311 
            A straightforward solution is to generate all distinct configurations, starting from the
310 
            open variables and inferring the others. This can be part of the continuous integration
 312 
            open variables and inferring the others. This can be part of the continuous integration
311 
            process which would try to compile and link the sources in all distinct configurations.
 313 
            process which would try to compile and link the sources in all distinct configurations.
312 
           
 314 
           
313 
            If we want to be really pedantic, we should also make sure that we run all the relevant higher
 315 
            If we want to be really pedantic, we should also make sure that we run all the relevant higher
314 
            level verification methods on all configurations generated by this step. That would certainly
 316 
            level verification methods on all configurations generated by this step. That would certainly
315 
            require to multiply the time required by the verification methods at least by the number
 317 
            require to multiply the time required by the verification methods at least by the number
316 
            of the distinct configurations. Constraining the set of configurations to just the most
 318 
            of the distinct configurations. Constraining the set of configurations to just the most
317 
            representative ones is perhaps a reasonable compromise.
 319 
            representative ones is perhaps a reasonable compromise.
318 
       
 320 
       
319 
        \subsection{Regression and Unit Tests}
 321 
        \subsection{Regression and Unit Tests}
320 
            Although some people would argue whether testing is a formal verification method, we still include
 322 
            Although some people would argue whether testing is a formal verification method, we still include
321 
            it into the big picture. Running regression and unit tests which are part of HelenOS code base
 323 
            it into the big picture. Running regression and unit tests which are part of HelenOS code base
322 
            in the continuous integration process is fairly easy. The only complication lies in the technicalities:
 324 
            in the continuous integration process is fairly easy. The only complication lies in the technicalities:
323 
            We need to setup an automated network of physical machines and simulators which can run the
 325 
            We need to setup an automated network of physical machines and simulators which can run the
324 
            appropriate compilation outputs for the specific platforms. We need to be able to reboot
 326 
            appropriate compilation outputs for the specific platforms. We need to be able to reboot
325 
            them remotely and distribute the boot images to them. And last but not least, we need to be
 327 
            them remotely and distribute the boot images to them. And last but not least, we need to be
326 
            able to gather the results from them.
 328 
            able to gather the results from them.
327 
       
 329 
       
328 
        \subsection{Instrumentation}
 330 
        \subsection{Instrumentation}
329 
            Instrumentation tools for detecting memory leaks, performance bottlenecks and soft-deadlocks
 331 
            Instrumentation tools for detecting memory leaks, performance bottlenecks and soft-deadlocks
330 
            are also not usually considered to be formal verification tools. They are also rarely utilized
 332 
            are also not usually considered to be formal verification tools. They are also rarely utilized
331 
            on regular basis as part of the continuous integration process. But again, it might be helpful
 333 
            on regular basis as part of the continuous integration process. But again, it might be helpful
332 
            to just mention them in the context of regression and unit tests.
 334 
            to just mention them in the context of regression and unit tests.
333 
           
 335 
           
334 
            If some regression or unit tests fail, they sometimes do not give sufficient information to
 336 
            If some regression or unit tests fail, they sometimes do not give sufficient information to
335 
            tell immediately what is the root cause of the issue. In that case running the faulting tests
 337 
            tell immediately what is the root cause of the issue. In that case running the faulting tests
336 
            on manually or automatically instrumented executable code might provide more data and point
 338 
            on manually or automatically instrumented executable code might provide more data and point
337 
            more directly to the actual bug.
 339 
            more directly to the actual bug.
338 
       
 340 
       
339 
        \subsection{Verifying C Language Compiler}
 341 
        \subsection{Verifying C Language Compiler}
340 
            C language compilers are traditionally not considered to be formal verification tools. Many people
 342 
            C language compilers are traditionally not considered to be formal verification tools. Many people
341 
            just say that C compilers are good at generating executable code, but do not care much about the semantics
 343 
            just say that C compilers are good at generating executable code, but do not care much about the semantics
342 
            of the source code (on the other hand, formal verification tools usually do not generate any executable code
 344 
            of the source code (on the other hand, formal verification tools usually do not generate any executable code
343 
            at all). However, with recent development in the compiler domain, the old paradigms are shifting.
 345 
            at all). However, with recent development in the compiler domain, the old paradigms are shifting.
344 
           
 346 
           
345 
            As the optimization passes and general maturity of the compilers improve over time,
 347 
            As the optimization passes and general maturity of the compilers improve over time,
346 
            the compilers try to extract and use more and more semantic information from the source code.
 348 
            the compilers try to extract and use more and more semantic information from the source code.
347 
            The C language is quite poor on explicit semantic information, but the verifying compilers
 349 
            The C language is quite poor on explicit semantic information, but the verifying compilers
348 
            try to rely on vendor-specific language extensions and on the fact that some semantic information
 350 
            try to rely on vendor-specific language extensions and on the fact that some semantic information
349 
            can be added to the source code without changing the resulting executable code.
 351 
            can be added to the source code without changing the resulting executable code.
350 
           
 352 
           
351 
            The checks done by the verifying compilers cannot result in fatal errors in the usual cases (they
 353 
            The checks done by the verifying compilers cannot result in fatal errors in the usual cases (they
352 
            are just warnings). Firstly, the compilers still need to successfully compile a well-formed C source
 354 
            are just warnings). Firstly, the compilers still need to successfully compile a well-formed C source
353 
            code compliant to some older standard (e.g. C89) even when it is not up with the current quality
 355 
            code compliant to some older standard (e.g. C89) even when it is not up with the current quality
354 
            expectations. Old legacy source code should still pass the compilation as it did decades ago.
 356 
            expectations. Old legacy source code should still pass the compilation as it did decades ago.
355 
           
 357 
           
356 
            Secondly, the checks run by the verifying compilers are usually not based on abstract interpretation
 358 
            Secondly, the checks run by the verifying compilers are usually not based on abstract interpretation
357 
            or exhaustive traversal of a model state space. They are mostly realized as abstract syntax tree
 359 
            or exhaustive traversal of a model state space. They are mostly realized as abstract syntax tree
358 
            transformations much in the line with the supporting routines of the compilation process (data
 360 
            transformations much in the line with the supporting routines of the compilation process (data
359 
            and control flow graph analysis, dead code elimination, register allocation, etc.) and the evaluation
 361 
            and control flow graph analysis, dead code elimination, register allocation, etc.) and the evaluation
360 
            function is basically the matching of antipatterns of common programming bugs.
 362 
            function is basically the matching of antipatterns of common programming bugs.
361 
           
 363 
           
362 
            The checks are usually conservative. The verifying compilers identify code constructs which are suspicious,
 364 
            The checks are usually conservative. The verifying compilers identify code constructs which are suspicious,
363 
            which might arise out of programmer's bad intuition and so on, but even these code snippets cannot be
 365 
            which might arise out of programmer's bad intuition and so on, but even these code snippets cannot be
364 
            tagged as definitive bugs (since the programmer can be simply in a position where he/she really wants to
 366 
            tagged as definitive bugs (since the programmer can be simply in a position where he/she really wants to
365 
            do something very strange, but nevertheless legitimate). It is upon the programmer
 367 
            do something very strange, but nevertheless legitimate). It is upon the programmer
366 
            to examine the root cause of the compiler warning, tell whether it is really a bug or just a false
 368 
            to examine the root cause of the compiler warning, tell whether it is really a bug or just a false
367 
            positive and fix the issue by either amending some additional semantic information (e.g. adding an
 369 
            positive and fix the issue by either amending some additional semantic information (e.g. adding an
368 
            explicit typecast or a vendor-specific language extension) or rewriting the code.
 370 
            explicit typecast or a vendor-specific language extension) or rewriting the code.
369 
       
 371 
       
370 
        \subsection{Static Analyzer}
 372 
        \subsection{Static Analyzer}
371 
            Static analyzers try to go deeper than verifying compilers. Besides detecting common antipatterns of
 373 
            Static analyzers try to go deeper than verifying compilers. Besides detecting common antipatterns of
372 
            bugs, they also use techniques such as abstract interpretation to check for more complex properties.
 374 
            bugs, they also use techniques such as abstract interpretation to check for more complex properties.
373 
           
 375 
           
374 
            Most commercial static analyzers come with a predefined set of properties which cannot be easily changed.
 376 
            Most commercial static analyzers come with a predefined set of properties which cannot be easily changed.
375 
            They are coupled with the commonly used semantics of the environment and generate domain-specific models
 377 
            They are coupled with the commonly used semantics of the environment and generate domain-specific models
376 
            of the software based not only on the syntax of the source code, but also based on the assumptions derived
 378 
            of the software based not only on the syntax of the source code, but also based on the assumptions derived
377 
            from the memory access model, allocation and deallocation rules, tracking of references and tracking of
 379 
            from the memory access model, allocation and deallocation rules, tracking of references and tracking of
378 
            concurrency locks.
 380 
            concurrency locks.
379 
           
 381 
           
380 
            The biggest advantage of static analyzers is that they can be easily included in the development or
 382 
            The biggest advantage of static analyzers is that they can be easily included in the development or
381 
            continuous integration process as an additional automated step, very similar to the verifying compilers.
 383 
            continuous integration process as an additional automated step, very similar to the verifying compilers.
382 
            No definition of properties is needed and false positives can be relatively easily eliminated by amending
 384 
            No definition of properties is needed and false positives can be relatively easily eliminated by amending
383 
            some explicit additional information to the source code within the boundaries of the programming language.
 385 
            some explicit additional information to the source code within the boundaries of the programming language.
384 
           
 386 
           
385 
            The authors of static analyzers claim large quantities of bugs detected or prevented~\cite{billion}, but static
 387 
            The authors of static analyzers claim large quantities of bugs detected or prevented~\cite{billion}, but static
386 
            analyzers are still relatively limited by the kind of bugs they are designed to detect. They
 388 
            analyzers are still relatively limited by the kind of bugs they are designed to detect. They
387 
            are usually good at pointing out common issues with security implications (specific types of buffer
 389 
            are usually good at pointing out common issues with security implications (specific types of buffer
388 
            and stack overruns, usage of well-known functions in an unsafe way, clear cases of forgotten
 390 
            and stack overruns, usage of well-known functions in an unsafe way, clear cases of forgotten
389 
            deallocation of resources and release of locks, etc.). Unfortunately, many static analyzers
 391 
            deallocation of resources and release of locks, etc.). Unfortunately, many static analyzers
390 
            only analyze a single-threaded control flow and are thus unable to detect concurrency issues
 392 
            only analyze a single-threaded control flow and are thus unable to detect concurrency issues
391 
            such as deadlocks.
 393 
            such as deadlocks.
392 
       
 394 
       
393 
        \subsection{Static Verifier}
 395 
        \subsection{Static Verifier}
394 
            There is one key difference between a static analyzer and a static verifier: Static verifiers
 396 
            There is one key difference between a static analyzer and a static verifier: Static verifiers
395 
            allow the user to specify one's own properties, in terms of preconditions, postconditions and
 397 
            allow the user to specify one's own properties, in terms of preconditions, postconditions and
396 
            invariants in the code. Many static verifiers also target true multithreaded usage patterns
 398 
            invariants in the code. Many static verifiers also target true multithreaded usage patterns
397 
            and have the capability to check proper locking order, hand-over-hand locking and even liveliness.
 399 
            and have the capability to check proper locking order, hand-over-hand locking and even liveliness.
398 
           
 400 
           
399 
            In the context of an operating system kernel and core libraries two kinds of properties are
 401 
            In the context of an operating system kernel and core libraries two kinds of properties are
400 
            common:
 402 
            common:
401 
           
 403 
           
402 
            \begin{itemize}
 404 
            \begin{itemize}
403 
                \item \emph{Consistency constrains:} These properties define the correct way how data is supposed
 405 
                \item \emph{Consistency constrains:} These properties define the correct way how data is supposed
404 
                      to be manipulated by some related set of subroutines. Checking for these
 406 
                      to be manipulated by some related set of subroutines. Checking for these
405 
                      properties ensures that data structures and internal states will not get corrupt due
 407 
                      properties ensures that data structures and internal states will not get corrupt due
406 
                      to bugs in the functions and methods which are designed to manipulate them.
 408 
                      to bugs in the functions and methods which are designed to manipulate them.
407 
                \item \emph{Interface enforcement:} These properties define the correct semantics by which
 409 
                \item \emph{Interface enforcement:} These properties define the correct semantics by which
408 
                      a set of subroutines should be used by the rest of the code. Checking for these properties
 410 
                      a set of subroutines should be used by the rest of the code. Checking for these properties
409 
                      ensures that some API is always used by the rest of the code in a specified way
 411 
                      ensures that some API is always used by the rest of the code in a specified way
410 
                      and all possible error states are detected and reported.
 412 
                      and all possible error states are detected and reported.
411 
            \end{itemize}
 413 
            \end{itemize}
412 
       
 414 
       
413 
        \subsection{Model Checker}
 415 
        \subsection{Model Checker}
414 
            \label{modelcheck}
 416 
            \label{modelcheck}
415 
            On the first sight it does not seem to be reasonable to consider general model checkers as
 417 
            On the first sight it does not seem to be reasonable to consider general model checkers as
416 
            relevant independent tools for formal verification of an existing operating system. While many
 418 
            relevant independent tools for formal verification of an existing operating system. While many
417 
            different tools use model checkers as their backends, verifying a complete model of the entire
 419 
            different tools use model checkers as their backends, verifying a complete model of the entire
418 
            system created by hand seems to be infeasible both in the sense of time required for the model
 420 
            system created by hand seems to be infeasible both in the sense of time required for the model
419 
            creation and resources required by the checker to finish the exhaustive traversal of the model's
 421 
            creation and resources required by the checker to finish the exhaustive traversal of the model's
420 
            address space.
 422 
            address space.
421 
           
 423 
           
422 
            Nevertheless, model checkers on their own can still serve a good job verifying abstract
 424 
            Nevertheless, model checkers on their own can still serve a good job verifying abstract
423 
            properties of key algorithms without dealing with the technical details of the implementation.
 425 
            properties of key algorithms without dealing with the technical details of the implementation.
424 
            Various properties of synchronization algorithms, data structures and communication protocols
 426 
            Various properties of synchronization algorithms, data structures and communication protocols
425 
            can be verified in the most generic conditions by model checkers, answering the
 427 
            can be verified in the most generic conditions by model checkers, answering the
426 
            question whether they are designed properly in theory.
 428 
            question whether they are designed properly in theory.
427 
           
 429 
           
428 
            If the implementation of these algorithms and protocols do not behave correctly, we can be sure
 430 
            If the implementation of these algorithms and protocols do not behave correctly, we can be sure
429 
            that the root cause is in the non-compliance between the design and implementation and not a
 431 
            that the root cause is in the non-compliance between the design and implementation and not a
430 
            fundamental flaw of the design itself.
 432 
            fundamental flaw of the design itself.
431 
       
 433 
       
432 
        \subsection{Behavior Checker}
 434 
        \subsection{Behavior Checker}
433 
            All previously mentioned verification methods were targeting internal properties of the operating system
 435 
            All previously mentioned verification methods were targeting internal properties of the operating system
434 
            components. If we are moving to a higher-level abstraction in order to specify correct interaction of the encapsulated
 436 
            components. If we are moving to a higher-level abstraction in order to specify correct interaction of the encapsulated
435 
            components in terms of interface compatibility and communication, we can utilize \emph{Behavior Protocols}~\cite{bp}.
 437 
            components in terms of interface compatibility and communication, we can utilize \emph{Behavior Protocols}~\cite{bp}.
436 
           
 438 
           
437 
            To gain the knowledge about the architecture of the whole operating system in terms of software
 439 
            To gain the knowledge about the architecture of the whole operating system in terms of software
438 
            component composition and bindings, we can use \emph{Architecture Description Language}~\cite{adl}.
 440 
            component composition and bindings, we can use \emph{Architecture Description Language}~\cite{adl}.
439 
            This language has the possibility to capture interface types (with method signatures), primitive
 441 
            This language has the possibility to capture interface types (with method signatures), primitive
440 
            components (in terms of provided and required interfaces), composite components (an architectural
 442 
            components (in terms of provided and required interfaces), composite components (an architectural
441 
            compositions of primitive components) and the bindings between the respective interfaces of the
 443 
            compositions of primitive components) and the bindings between the respective interfaces of the
442 
            components.
 444 
            components.
443 
           
 445 
           
444 
            Unfortunately, the description is usually static, which is not quite suitable for the dynamic
 446 
            Unfortunately, the description is usually static, which is not quite suitable for the dynamic
445 
            nature of HelenOS and other operating systems. This limitation can be circumvented by considering a relevant
 447 
            nature of HelenOS and other operating systems. This limitation can be circumvented by considering a relevant
446 
            snapshot of the dynamic run-time architecture. This snapshot fixed in time is equivalent to
 448 
            snapshot of the dynamic run-time architecture. This snapshot fixed in time is equivalent to
447 
            a statically defined architecture.
 449 
            a statically defined architecture.
448 
           
 450 
           
449 
            Behavior Protocol checkers can target three main goals:
 451 
            Behavior Protocol checkers can target three main goals:
450 
           
 452 
           
451 
            \begin{itemize}
 453 
            \begin{itemize}
452 
                \item \emph{Horizontal compliance:} Also called \emph{compatibility}. The goal is to check
 454 
                \item \emph{Horizontal compliance:} Also called \emph{compatibility}. The goal is to check
453 
                      whether the specifications of components that are bound together are semantically
 455 
                      whether the specifications of components that are bound together are semantically
454 
                      compatible. All required interfaces need to be bound to provided interfaces and
 456 
                      compatible. All required interfaces need to be bound to provided interfaces and
455 
                      the communication between the components cannot lead to \emph{no activity} (a deadlock)
 457 
                      the communication between the components cannot lead to \emph{no activity} (a deadlock)
456 
                      or a \emph{bad activity} (a livelock).
 458 
                      or a \emph{bad activity} (a livelock).
457 
                \item \emph{Vertical compliance:} Also called \emph{substituability}. The goal is to check whether
 459 
                \item \emph{Vertical compliance:} Also called \emph{substituability}. The goal is to check whether
458 
                      it is possible to replace a set of primitive components that are nested inside a composite
 460 
                      it is possible to replace a set of primitive components that are nested inside a composite
459 
                      component by the composite component itself. In other words, this compliance can answer the
 461 
                      component by the composite component itself. In other words, this compliance can answer the
460 
                      questions whether the architecture description of the system is sound with respect to the hierarchical
 462 
                      questions whether the architecture description of the system is sound with respect to the hierarchical
461 
                      composition of the components.
 463 
                      composition of the components.
462 
                \item \emph{Compliance between the specification and the implementation:} Using various means
 464 
                \item \emph{Compliance between the specification and the implementation:} Using various means
463 
                      for generating artificial environments for an isolated component the checker is able to
 465 
                      for generating artificial environments for an isolated component the checker is able to
464 
                      partially answer the question whether the implementation of the component is an instantiation
 466 
                      partially answer the question whether the implementation of the component is an instantiation
465 
                      of the component specification.
 467 
                      of the component specification.
466 
            \end{itemize}
 468 
            \end{itemize}
467 
           
 469 
           
468 
            Horizontal and vertical compliance checking can be done exhaustively. This is a fundamental property
 470 
            Horizontal and vertical compliance checking can be done exhaustively. This is a fundamental property
469 
            which allows the reasoning about the dependability of the entire component-based operating system.
 471 
            which allows the reasoning about the dependability of the entire component-based operating system.
470 
            Assuming that the lower-level verification methods (described in Sections \ref{clang} to \ref{modelcheck})
 472 
            Assuming that the lower-level verification methods (described in Sections \ref{clang} to \ref{modelcheck})
471 
            prove some specific properties of the primitive components, we can be sure that the composition of
 473 
            prove some specific properties of the primitive components, we can be sure that the composition of
472 
            the primitive components into composite components and ultimately into the whole operating system
 474 
            the primitive components into composite components and ultimately into the whole operating system
473 
            does not break these properties.
 475 
            does not break these properties.
474 
           
 476 
           
475 
            The feasibility of many lower-level verification methods from Sections \ref{clang} to \ref{modelcheck}
 477 
            The feasibility of many lower-level verification methods from Sections \ref{clang} to \ref{modelcheck}
476 
            depends largely on the size and complexity of the code under verification. If the entire operating
 478 
            depends largely on the size and complexity of the code under verification. If the entire operating
477 
            system is decomposed into primitive components with a reasonable granularity, it is more likely that the
 479 
            system is decomposed into primitive components with a reasonable granularity, it is more likely that the
478 
            individual primitive components can be verified against a large number of properties. Thanks to the
 480 
            individual primitive components can be verified against a large number of properties. Thanks to the
479 
            recursive component composition we can then be sure that these properties also hold for the entire system.
 481 
            recursive component composition we can then be sure that these properties also hold for the entire system.
480 
            In monolithic operating systems without a clear decomposition we cannot do this inference and we
 482 
            In monolithic operating systems without a clear decomposition we cannot do this inference and we
481 
            need to verify the lower-level properties over a much larger code base (e.g. the whole monolithic kernel).
 483 
            need to verify the lower-level properties over a much larger code base (e.g. the whole monolithic kernel).
482 
           
 484 
           
483 
            \medskip
 485 
            \medskip
484 
           
 486 
           
485 
            The compliance between the behavior specification and the actual behavior of the implementation is, unfortunately,
 487 
            The compliance between the behavior specification and the actual behavior of the implementation is, unfortunately,
486 
            the missing link in the chain. This compliance cannot be easily verified in an exhaustive manner. If there is
 488 
            the missing link in the chain. This compliance cannot be easily verified in an exhaustive manner. If there is
487 
            a discrepancy between the specified and the actual behavior of the components, we cannot conclude anything about
 489 
            a discrepancy between the specified and the actual behavior of the components, we cannot conclude anything about
488 
            the properties holding in the entire system.
 490 
            the properties holding in the entire system.
489 
           
 491 
           
490 
            However, there is one way how to improve the situation: \emph{code generation}. If we generate implementation
 492 
            However, there is one way how to improve the situation: \emph{code generation}. If we generate implementation
491 
            from the specification, the compliance between them is axiomatic. If we are able to generate enough
 493 
            from the specification, the compliance between them is axiomatic. If we are able to generate enough
492 
            code from the specification to run into the hand-written ``business code'' where we check for
 494 
            code from the specification to run into the hand-written ``business code'' where we check for
493 
            the lower-level properties, the conclusions about the component composition are going to hold.
 495 
            the lower-level properties, the conclusions about the component composition are going to hold.
494 
       
 496 
       
495 
        \subsection{Behavior Description Generator}
 497 
        \subsection{Behavior Description Generator}
496 
            To conclude our path towards higher abstractions we can utilize tools that can
 498 
            To conclude our path towards higher abstractions we can utilize tools that can
497 
            generate the behavior descriptions from \emph{textual use cases} written in a domain-constrained English.
 499 
            generate the behavior descriptions from \emph{textual use cases} written in a domain-constrained English.
498 
            These generated artifacts can be then compared (e.g. via vertical compliance checking) with the formal
 500 
            These generated artifacts can be then compared (e.g. via vertical compliance checking) with the formal
499 
            specification. Although the comparison might not provide clean-cut results, it can still be
 501 
            specification. Although the comparison might not provide clean-cut results, it can still be
500 
            helpful to confront the more-or-less informal user expectations on the system with the exact formal description.
 502 
            helpful to confront the more-or-less informal user expectations on the system with the exact formal description.
501 
       
 503 
       
502 
        \subsection{Summary}
 504 
        \subsection{Summary}
503 
            \label{missing}
 505 
            \label{missing}
504 
            So far, we have proposed a compact combination of formal methods which start at the level of C programming
 506 
            So far, we have proposed a compact combination of formal methods which start at the level of C programming
505 
            language, offer the possibility to check for the presence of various common antipatterns, to check for generic
 507 
            language, offer the possibility to check for the presence of various common antipatterns, to check for generic
506 
            algorithm-related properties, consistency constrains, interface enforcements and conclude with a framework
 508 
            algorithm-related properties, consistency constrains, interface enforcements and conclude with a framework
507 
            to make these properties hold even in the case of a large operating system composed from many
 509 
            to make these properties hold even in the case of a large operating system composed from many
508 
            components of compliant behavior.
 510 
            components of compliant behavior.
509 
           
 511 
           
510 
            We are also able to fill in some of the missing pieces by other software engineering approaches
 512 
            We are also able to fill in some of the missing pieces by other software engineering approaches
511 
            such as regression and unit testing and instrumentation.
 513 
            such as regression and unit testing and instrumentation.
512 
           
 514 
           
513 
            \medskip
 515 
            \medskip
514 
           
 516 
           
515 
            We have spoken only about the functional properties. In general, we cannot apply the same formalisms
 517 
            We have spoken only about the functional properties. In general, we cannot apply the same formalisms
516 
            and methods on extra-functional properties (e.g. timing properties, performance properties, etc.).
 518 
            and methods on extra-functional properties (e.g. timing properties, performance properties, etc.).
517 
            And although it probably does make a good sense to reason about component composition for the extra-functional
 519 
            And although it probably does make a good sense to reason about component composition for the extra-functional
518 
            properties, the exact relation might be different compared to the functional properties.
 520 
            properties, the exact relation might be different compared to the functional properties.
519 
           
 521 
           
520 
            The extra-functional properties need to be tackled by our future work.
 522 
            The extra-functional properties need to be tackled by our future work.
521 
       
 523 
       
522 
    \section{Evaluation}
 524 
    \section{Evaluation}
523 
        \label{evaluation}
 525 
        \label{evaluation}
524 
        This section copies the structure of the previous Section \ref{analysis} and adds HelenOS-specific
 526 
        This section copies the structure of the previous Section \ref{analysis} and adds HelenOS-specific
525 
        evaluation of the the proposed formalisms and tools. As this is still largely a work-in-progress,
 527 
        evaluation of the the proposed formalisms and tools. As this is still largely a work-in-progress,
526 
        in many cases just the initial observations can be made.
 528 
        in many cases just the initial observations can be made.
527 
       
 529 
       
528 
        \subsection{Verifying C Language Compiler and Continuous Integration Tool}
 530 
        \subsection{Verifying C Language Compiler and Continuous Integration Tool}
529 
            The primary C compiler used by HelenOS is \emph{GNU GCC 4.4.3} (all platforms)~\cite{gcc} and \emph{Clang 2.6.0}
 531 
            The primary C compiler used by HelenOS is \emph{GNU GCC 4.4.3} (all platforms)~\cite{gcc} and \emph{Clang 2.6.0}
530 
            (IA-32)~\cite{clang}. We have taken some effort to support also \emph{ICC} and \emph{Sun Studio} C compilers,
 532 
            (IA-32)~\cite{clang}. We have taken some effort to support also \emph{ICC} and \emph{Sun Studio} C compilers,
531 
            but the compatibility with these compilers in not guaranteed.
 533 
            but the compatibility with these compilers in not guaranteed.
532 
           
 534 
           
533 
            The whole code base is compiled with the \texttt{-Wall} and \texttt{-Wextra} compilation options. These options turn on
 535 
            The whole code base is compiled with the \texttt{-Wall} and \texttt{-Wextra} compilation options. These options turn on
534 
            most of the verification checks of the compilers. The compilers trip on common bug antipatterns such
 536 
            most of the verification checks of the compilers. The compilers trip on common bug antipatterns such
535 
            as implicit typecasting of pointer types, comparison of signed and unsigned integer values (danger
 537 
            as implicit typecasting of pointer types, comparison of signed and unsigned integer values (danger
536 
            of unchecked overflows), the usage of uninitialized variables, the presence of unused local variables,
 538 
            of unchecked overflows), the usage of uninitialized variables, the presence of unused local variables,
537 
            NULL-pointer dereferencing (determined by conservative local control flow analysis), functions
 539 
            NULL-pointer dereferencing (determined by conservative local control flow analysis), functions
538 
            with non-void return typed that do not return any value and so on. We treat all compilation warnings
 540 
            with non-void return typed that do not return any value and so on. We treat all compilation warnings
539 
            as fatal errors, thus the code base must pass without any warnings.
 541 
            as fatal errors, thus the code base must pass without any warnings.
540 
           
 542 
           
541 
            We also turn on several more specific and strict checks. These checks helped to discover several
 543 
            We also turn on several more specific and strict checks. These checks helped to discover several
542 
            latent bugs in the source code:
 544 
            latent bugs in the source code:
543 
           
 545 
           
544 
            \begin{itemize}
 546 
            \begin{itemize}
545 
                \item \texttt{-Wfloat-equal} Check for exact equality comparison between floating point values. The
 547 
                \item \texttt{-Wfloat-equal} Check for exact equality comparison between floating point values. The
546 
                      usage of equal comparator on floats is usually misguided due to the inherent computational errors
 548 
                      usage of equal comparator on floats is usually misguided due to the inherent computational errors
547 
                      of floats.
 549 
                      of floats.
548 
                \item \texttt{-Wcast-align} Check for code which casts pointers to a type with a stricter alignment
 550 
                \item \texttt{-Wcast-align} Check for code which casts pointers to a type with a stricter alignment
549 
                      requirement. On many RISC-based platforms this can cause run-time unaligned access exceptions.
 551 
                      requirement. On many RISC-based platforms this can cause run-time unaligned access exceptions.
550 
                \item \texttt{-Wconversion} Check for code where the implicit type conversion (e.g. from float to integer,
 552 
                \item \texttt{-Wconversion} Check for code where the implicit type conversion (e.g. from float to integer,
551 
                      between signed and unsigned integers or between integers with different number of bits) can
 553 
                      between signed and unsigned integers or between integers with different number of bits) can
552 
                      cause the actual value to change.
 554 
                      cause the actual value to change.
553 
            \end{itemize}
 555 
            \end{itemize}
554 
           
 556 
           
555 
            To enhance the semantic information in the source code, we use GCC-specific language extensions to annotate
 557 
            To enhance the semantic information in the source code, we use GCC-specific language extensions to annotate
556 
            some particular kernel and core library routines:
 558 
            some particular kernel and core library routines:
557 
           
 559 
           
558 
            \begin{itemize}
 560 
            \begin{itemize}
559 
                \item \texttt{\_\_attribute\_\_((noreturn))} Functions marked in this way never finish from the point of view
 561 
                \item \texttt{\_\_attribute\_\_((noreturn))} Functions marked in this way never finish from the point of view
560 
                      of the current sequential execution flow. The most common case are the routines which restore previously saved
 562 
                      of the current sequential execution flow. The most common case are the routines which restore previously saved
561 
                      execution context.
 563 
                      execution context.
562 
                \item \texttt{\_\_attribute\_\_((returns\_twice))} Functions marked in this way may return multiple times from
 564 
                \item \texttt{\_\_attribute\_\_((returns\_twice))} Functions marked in this way may return multiple times from
563 
                      the point of view of the current sequential execution flow. This is the case of routines which save the current
 565 
                      the point of view of the current sequential execution flow. This is the case of routines which save the current
564 
                      execution context (first the function returns as usual, but the function can eventually ``return again''
 566 
                      execution context (first the function returns as usual, but the function can eventually ``return again''
565 
                      when the context is being restored).
 567 
                      when the context is being restored).
566 
            \end{itemize}
 568 
            \end{itemize}
567 
           
 569 
           
568 
            The use of these extensions has pointed out to several hard-to-debug bugs on the IA-64 platform.
 570 
            The use of these extensions has pointed out to several hard-to-debug bugs on the IA-64 platform.
569 
           
 571 
           
570 
            \medskip
 572 
            \medskip
571 
           
 573 
           
572 
            The automated continuous integration building system is currently work-in-progress. Thus, we do not
 574 
            The automated continuous integration building system is currently work-in-progress. Thus, we do not
573 
            test all possible configurations of HelenOS with each changeset yet. Currently only
 575 
            test all possible configurations of HelenOS with each changeset yet. Currently only
574 
            a representative set of 14 configurations (at least one for each supported platform) is tested by hand
 576 
            a representative set of 14 configurations (at least one for each supported platform) is tested by hand
575 
            by the developers before committing any non-trivial changeset.
 577 
            by the developers before committing any non-trivial changeset.
576 
           
 578 
           
577 
            From occasional tests of other configurations by hand and the frequency of compilation, linkage and
 579 
            From occasional tests of other configurations by hand and the frequency of compilation, linkage and
578 
            even run-time problems we conclude that the automated testing of all feasible configurations will
 580 
            even run-time problems we conclude that the automated testing of all feasible configurations will
579 
            be very beneficial.
 581 
            be very beneficial.
580 
           
 582 
           
581 
        \subsection{Regression and Unit Tests}
 583 
        \subsection{Regression and Unit Tests}
582 
            As already stated in the previous section, the continuous integration building system has not been finished
 584 
            As already stated in the previous section, the continuous integration building system has not been finished
583 
            yet. Therefore regression and unit tests are executed occasionally by hand, which is time consuming
 585 
            yet. Therefore regression and unit tests are executed occasionally by hand, which is time consuming
584 
            and prone to human omissions. An automated approach is definitively going to be very helpful.
 586 
            and prone to human omissions. An automated approach is definitively going to be very helpful.
585 
       
 587 
       
586 
        \subsection{Instrumentation}
 588 
        \subsection{Instrumentation}
587 
            We are in the process of implementing our own code instrumentation framework which is motivated mainly
 589 
            We are in the process of implementing our own code instrumentation framework which is motivated mainly
588 
            by the need to support MMU-less architectures in the future. But this framework might be also very helpful
 590 
            by the need to support MMU-less architectures in the future. But this framework might be also very helpful
589 
            in detecting memory and generic resource leaks. We have not tried \emph{Valgrind}~\cite{valgrind} or any similar existing tool
 591 
            in detecting memory and generic resource leaks. We have not tried \emph{Valgrind}~\cite{valgrind} or any similar existing tool
590 
            because of the estimated complexity to adopt it for the usage in HelenOS.
 592 
            because of the estimated complexity to adopt it for the usage in HelenOS.
591 
           
 593 
           
592 
            HelenOS was also scanned by \emph{Coverity}~\cite{coverity} in 2006 when no errors were detected. However, since that
 594 
            HelenOS was also scanned by \emph{Coverity}~\cite{coverity} in 2006 when no errors were detected. However, since that
593 
            time the code base has not been analyzed by Coverity.
 595 
            time the code base has not been analyzed by Coverity.
594 
       
 596 
       
595 
        \subsection{Static Analyzer}
 597 
        \subsection{Static Analyzer}
596 
            The integration of various static analyzers into the HelenOS continuous integration process is underway.
 598 
            The integration of various static analyzers into the HelenOS continuous integration process is underway.
597 
            For the initial evaluation we have used \emph{Stanse}~\cite{stanse} and \emph{Clang Analyzer}~\cite{clanganalyzer}.
 599 
            For the initial evaluation we have used \emph{Stanse}~\cite{stanse} and \emph{Clang Analyzer}~\cite{clanganalyzer}.
598 
            Both of them showed to be moderately helpful to point out instances of unreachable dead code, use of language
 600 
            Both of them showed to be moderately helpful to point out instances of unreachable dead code, use of language
599 
            constructs which have ambiguous semantics in C and one case of possible NULL-pointer dereference.
 601 
            constructs which have ambiguous semantics in C and one case of possible NULL-pointer dereference.
600 
           
 602 
           
601 
            The open framework of Clang seems to be very promising for implementing domain-specific checks (and at
 603 
            The open framework of Clang seems to be very promising for implementing domain-specific checks (and at
602 
            the same time it is also a very promising compiler framework). Our mid-term goal is to incorporate some of the features
 604 
            the same time it is also a very promising compiler framework). Our mid-term goal is to incorporate some of the features
603 
            of Stanse and VCC (see Section \ref{staticverifier2}) into Clang Analyzer.
 605 
            of Stanse and VCC (see Section \ref{staticverifier2}) into Clang Analyzer.
604 
       
 606 
       
605 
        \subsection{Static Verifier}
 607 
        \subsection{Static Verifier}
606 
            \label{staticverifier2}
 608 
            \label{staticverifier2}
607 
            We have started to extend the source code of HelenOS kernel with annotations understood
 609 
            We have started to extend the source code of HelenOS kernel with annotations understood
608 
            by \emph{Frama-C}~\cite{framac} and \emph{VCC}~\cite{vcc}. Initially we have targeted simple kernel data structures
 610 
            by \emph{Frama-C}~\cite{framac} and \emph{VCC}~\cite{vcc}. Initially we have targeted simple kernel data structures
609 
            (doubly-linked circular lists) and basic locking operations. Currently we are evaluating the initial experiences
 611 
            (doubly-linked circular lists) and basic locking operations. Currently we are evaluating the initial experiences
610 
            and we are trying to identify the most suitable methodology, but we expect quite promising results.
 612 
            and we are trying to identify the most suitable methodology, but we expect quite promising results.
611 
           
 613 
           
612 
            As the VCC is based on the Microsoft C++ Compiler, which does not support many GCC extensions, we have been
 614 
            As the VCC is based on the Microsoft C++ Compiler, which does not support many GCC extensions, we have been
613 
            faced with the requirement to preprocess the source code to be syntactically accepted by VCC. This turned out
 615 
            faced with the requirement to preprocess the source code to be syntactically accepted by VCC. This turned out
614 
            to be feasible.
 616 
            to be feasible.
615 
       
 617 
       
616 
        \subsection{Model Checker}
 618 
        \subsection{Model Checker}
617 
            We are in the process of creating models of kernel wait queues (basic HelenOS kernel synchronization
 619 
            We are in the process of creating models of kernel wait queues (basic HelenOS kernel synchronization
618 
            primitive) and futexes (basic user space thread synchronization primitive) using \emph{Promela} and
 620 
            primitive) and futexes (basic user space thread synchronization primitive) using \emph{Promela} and
619 
            verify several formal properties (deadlock freedom, fairness) in \emph{Spin}~\cite{spin}. As both the Promela language
 621 
            verify several formal properties (deadlock freedom, fairness) in \emph{Spin}~\cite{spin}. As both the Promela language
620 
            and the Spin model checker are mature and commonly used tools for such purposes, we expect no major problems
 622 
            and the Spin model checker are mature and commonly used tools for such purposes, we expect no major problems
621 
            with this approach. Because both synchronization primitives are relatively complex, utilizing a model checker
 623 
            with this approach. Because both synchronization primitives are relatively complex, utilizing a model checker
622 
            should provide a much more trustworthy proof of the required properties than ``paper and pencil''.
 624 
            should provide a much more trustworthy proof of the required properties than ``paper and pencil''.
623 
       
 625 
       
624 
        \subsection{Behavior Checker}
 626 
        \subsection{Behavior Checker}
625 
            We have created an architecture description in ADL language similar to SOFA ADL~\cite{adl} for the majority of the
 627 
            We have created an architecture description in ADL language similar to SOFA ADL~\cite{adl} for the majority of the
626 
            HelenOS components and created the Behavior Protocol specification of these components. The architecture
 628 
            HelenOS components and created the Behavior Protocol specification of these components. The architecture
627 
            is a snapshot of the dynamic architecture just after a successful bootstrap.
 629 
            is a snapshot of the dynamic architecture just after a successful bootstrap.
628 
           
 630 
           
629 
            Both the architecture and behavior description is readily available as part of the source code repository
 631 
            Both the architecture and behavior description is readily available as part of the source code repository
630 
            of HelenOS, including tools which can preprocess the Behavior Protocols according to the architecture description
 632 
            of HelenOS, including tools which can preprocess the Behavior Protocols according to the architecture description
631 
            and create an output suitable for \emph{bp2promela} checker~\cite{bp}.
 633 
            and create an output suitable for \emph{bp2promela} checker~\cite{bp}.
632 
           
 634 
           
633 
            As the resulting complexity of the description is larger than any of the previously published case studies
 635 
            As the resulting complexity of the description is larger than any of the previously published case studies
634 
            on Behavior Protocols (compare to~\cite{cocome}), our current work-in-progress is to optimize and fine-tune the bp2promela
 636 
            on Behavior Protocols (compare to~\cite{cocome}), our current work-in-progress is to optimize and fine-tune the bp2promela
635 
            checker to process the input.
 637 
            checker to process the input.
636 
           
 638 
           
637 
            \medskip
 639 
            \medskip
638 
           
 640 
           
639 
            We have not started to generate code from the architecture description so far because of time constrains. However,
 641 
            We have not started to generate code from the architecture description so far because of time constrains. However,
640 
            we believe that this is a very promising way to go.
 642 
            we believe that this is a very promising way to go.
641 
       
 643 
       
642 
        \subsection{Behavior Description Generator}
 644 
        \subsection{Behavior Description Generator}
643 
            We have not tackled the issue of behavior description generation yet, although tools such as \emph{Procasor}~\cite{procasor} are readily
 645 
            We have not tackled the issue of behavior description generation yet, although tools such as \emph{Procasor}~\cite{procasor} are readily
644 
            available. We do not consider it our priority at this time.
 646 
            available. We do not consider it our priority at this time.
645 
   
 647 
   
646 
    \section{Conclusion}
 648 
    \section{Conclusion}
647 
        \label{conclusion}
 649 
        \label{conclusion}
648 
        In this paper we propose a complex combination of various formal verification methods and tools
 650 
        In this paper we propose a complex combination of various formal verification methods and tools
649 
        to achieve the verification of an entire general-purpose operating system. The proposed approach generally follows
 651 
        to achieve the verification of an entire general-purpose operating system. The proposed approach generally follows
650 
        a bottom-to-top path, starting with low-level checks using state-of-the-art verifying C language compilers,
 652 
        a bottom-to-top path, starting with low-level checks using state-of-the-art verifying C language compilers,
651 
        following by static analyzers and static verifiers. In specific contexts regression and unit tests,
 653 
        following by static analyzers and static verifiers. In specific contexts regression and unit tests,
652 
        code instrumentation and model checkers for the sake of verification of key algorithms
 654 
        code instrumentation and model checkers for the sake of verification of key algorithms
653 
        are utilized.
 655 
        are utilized.
654 
       
 656 
       
655 
        Thanks to the properties of state-of-the-art microkernel multiserver operating
 657 
        Thanks to the properties of state-of-the-art microkernel multiserver operating
656 
        system design (e.g. software component encapsulation and composition), we demonstrate
 658 
        system design (e.g. software component encapsulation and composition), we demonstrate
657 
        that it should be feasible to successfully verify larger and more complex operating systems than
 659 
        that it should be feasible to successfully verify larger and more complex operating systems than
658 
        in the case of monolithic designs. We use formal component architecture and behavior
 660 
        in the case of monolithic designs. We use formal component architecture and behavior
659 
        description for the closure. The final goal -- a formally verified operating system -- is the
 661 
        description for the closure. The final goal -- a formally verified operating system -- is the
660 
        emerging property of the combination of the various methods.
 662 
        emerging property of the combination of the various methods.
661 
       
 663 
       
662 
        \medskip
 664 
        \medskip
663 
       
 665 
       
664 
        The contribution of this paper is the shift of focus from attempts to use a single ``silver-bullet''
 666 
        The contribution of this paper is the shift of focus from attempts to use a single ``silver-bullet''
665 
        method for formal verification of an operating system to a combination of multiple methods supported
 667 
        method for formal verification of an operating system to a combination of multiple methods supported
666 
        by a suitable architecture of the operating system.
 668 
        by a suitable architecture of the operating system.
667 
       
 669 
       
668 
        We also argue that the approach should be suitable for the mainstream
 670 
        We also argue that the approach should be suitable for the mainstream
669 
        general-purpose operating systems in the near future, because they are gradually
 671 
        general-purpose operating systems in the near future, because they are gradually
670 
        incorporating more microkernel-based features and fine-grained software components.
 672 
        incorporating more microkernel-based features and fine-grained software components.
671 
       
 673 
       
672 
        Although the evaluation of the proposed approach on HelenOS is still work-in-progress, the
 674 
        Although the evaluation of the proposed approach on HelenOS is still work-in-progress, the
673 
        preliminary results and estimates are promising.
 675 
        preliminary results and estimates are promising.
674 
       
 676 
       
675 
        \medskip
 677 
        \medskip
676 
       
 678 
       
677 
        \noindent\textbf{Acknowledgments.} The author would like to express his gratitude to all contributors of the HelenOS
 679 
        \noindent\textbf{Acknowledgments.} The author would like to express his gratitude to all contributors of the HelenOS
678 
        project. Without their vision and dedication the work on this paper would be almost impossible
 680 
        project. Without their vision and dedication the work on this paper would be almost impossible
679 
       
 681 
       
680 
        This work was partially supported by the Ministry of Education of the Czech Republic
 682 
        This work was partially supported by the Ministry of Education of the Czech Republic
681 
        (grant MSM\-0021620838).
 683 
        (grant MSM\-0021620838).
682 
   
 684 
   
683 
    \begin{thebibliography}{99}
 685 
    \begin{thebibliography}{99}
684 
        \bibitem{billion}Bessey A., Block K., Chelf B., Chou A., Fulton B., Hallem S., Henri-Gros C., Kamsky A., McPeak S., Engler D.: \emph{A Few Billion Lines of Code Later: Using Static Analysis to Find Bugs in the Real World}, Communications of the ACM, Vol. 53 No. 2, pp 66-75, 2010
 686 
        \bibitem{billion}Bessey A., Block K., Chelf B., Chou A., Fulton B., Hallem S., Henri-Gros C., Kamsky A., McPeak S., Engler D.: \emph{A Few Billion Lines of Code Later: Using Static Analysis to Find Bugs in the Real World}, Communications of the ACM, Vol. 53 No. 2, pp 66-75, 2010
685 
        \bibitem{bp}Kofron J.: \emph{Checking Software Component Behavior Using Behavior Protocols and Spin}, in proceedings of Applied Computing 2007, Seoul, Korea, pp. 1513-1517, 2007
 687 
        \bibitem{bp}Kofron J.: \emph{Checking Software Component Behavior Using Behavior Protocols and Spin}, in proceedings of Applied Computing 2007, Seoul, Korea, pp. 1513-1517, 2007
686 
        \bibitem{gcc}GCC, the GNU Compiler Collection, \texttt{http://gcc.gnu.org/}
 688 
        \bibitem{gcc}GCC, the GNU Compiler Collection, \texttt{http://gcc.gnu.org/}
687 
        \bibitem{clang}Clang: a C language family frontend for LLVM, \texttt{http://clang.llvm.org/}
 689 
        \bibitem{clang}Clang: a C language family frontend for LLVM, \texttt{http://clang.llvm.org/}
688 
        \bibitem{clanganalyzer}Clang Static Analyzer, \texttt{http://clang-analyzer.llvm.org/}
 690 
        \bibitem{clanganalyzer}Clang Static Analyzer, \texttt{http://clang-analyzer.llvm.org/}
689 
        \bibitem{cocome}Bulej L., Bures T., Coupaye T., Decky M., Jezek P., Parizek P., Plasil F., Poch T., Rivierre N., Sery O., Tuma P.: \emph{CoCoME in Fractal}, chapter in The Common Component Modeling Example: Comparing Software Component Models, Springer-Verlag, LNCS 5153, 2008
 691 
        \bibitem{cocome}Bulej L., Bures T., Coupaye T., Decky M., Jezek P., Parizek P., Plasil F., Poch T., Rivierre N., Sery O., Tuma P.: \emph{CoCoME in Fractal}, chapter in The Common Component Modeling Example: Comparing Software Component Models, Springer-Verlag, LNCS 5153, 2008
690 
        \bibitem{coverity}Coverity, \texttt{http://scan.coverity.com/}
 692 
        \bibitem{coverity}Coverity, \texttt{http://scan.coverity.com/}
691 
        \bibitem{procasor}Mencl V.: \emph{Deriving Behavior Specifications from Textual Use Cases}, in Proceedings of Workshop on Intelligent Technologies for Software Engineering (WITSE04, Sep 21, 2004, part of ASE 2004), Linz, Austria, pp. 331 - 341, Oesterreichische Computer Gesellschaft, 2004
 693 
        \bibitem{procasor}Mencl V.: \emph{Deriving Behavior Specifications from Textual Use Cases}, in Proceedings of Workshop on Intelligent Technologies for Software Engineering (WITSE04, Sep 21, 2004, part of ASE 2004), Linz, Austria, pp. 331 - 341, Oesterreichische Computer Gesellschaft, 2004
692 
        \bibitem{framac}Frama-C, \texttt{http://frama-c.cea.fr/}
 694 
        \bibitem{framac}Frama-C, \texttt{http://frama-c.cea.fr/}
693 
        \bibitem{c}Lawlis P. K: \emph{Guidelines for Choosing a Computer Language: Support for the Visionary Organization}, Ada Information Clearinghouse, \texttt{http://archive.adaic.com/docs/reports/lawlis/k.htm}, 1998
 695 
        \bibitem{c}Lawlis P. K: \emph{Guidelines for Choosing a Computer Language: Support for the Visionary Organization}, Ada Information Clearinghouse, \texttt{http://archive.adaic.com/docs/reports/lawlis/k.htm}, 1998
694 
        \bibitem{helenos}HelenOS Project, \texttt{http://www.helenos.org/}
 696 
        \bibitem{helenos}HelenOS Project, \texttt{http://www.helenos.org/}
695 
        \bibitem{adl}Oplustil T.: \emph{Inheritance in Architecture Description Languages}, reviewed section of Proceedings of the Week of Doctoral Students 2003 conference (WDS 2003), Charles University, Prague, Czech Republic, 2003, pp. 124 - 131, 2003
 697 
        \bibitem{adl}Oplustil T.: \emph{Inheritance in Architecture Description Languages}, reviewed section of Proceedings of the Week of Doctoral Students 2003 conference (WDS 2003), Charles University, Prague, Czech Republic, 2003, pp. 124 - 131, 2003
696 
        \bibitem{marketshare}Operating System Market Share, \texttt{http://marketshare.hitslink.com/report\-.aspx?qprid=8\&qptimeframe=M\&qpsp=132}, retrieved on 2010-02-28
 698 
        \bibitem{marketshare}Operating System Market Share, \texttt{http://marketshare.hitslink.com/report\-.aspx?qprid=8\&qptimeframe=M\&qpsp=132}, retrieved on 2010-02-28
697 
        \bibitem{seL4}Klein G., Elphinstone K., Heiser G., Andronick J., Cock D., Derrin P., Elkaduwe D., Engelhardt K., Kolanski R., Norrish M., Sewell T., Tuch H., Winwood S.: \emph{seL4: Formal verification of an OS kernel}, Proceedings of the 22nd ACM Symposium on Operating Systems Principles, Big Sky, MT, USA, 2009
 699 
        \bibitem{seL4}Klein G., Elphinstone K., Heiser G., Andronick J., Cock D., Derrin P., Elkaduwe D., Engelhardt K., Kolanski R., Norrish M., Sewell T., Tuch H., Winwood S.: \emph{seL4: Formal verification of an OS kernel}, Proceedings of the 22nd ACM Symposium on Operating Systems Principles, Big Sky, MT, USA, 2009
698 
        \bibitem{spin}Spin, \texttt{http://spinroot.com/}
 700 
        \bibitem{spin}Spin, \texttt{http://spinroot.com/}
699 
        \bibitem{stanse}Stanse: Static Analysis Framework for C code, \texttt{http://stanse.fi.muni.cz/}
 701 
        \bibitem{stanse}Stanse: Static Analysis Framework for C code, \texttt{http://stanse.fi.muni.cz/}
700 
        \bibitem{valgrind}Valgrind, \texttt{http://valgrind.org/}
 702 
        \bibitem{valgrind}Valgrind, \texttt{http://valgrind.org/}
701 
        \bibitem{vcc}VCC, \texttt{http://vcc.codeplex.com/}
 703 
        \bibitem{vcc}VCC, \texttt{http://vcc.codeplex.com/}
702 
    \end{thebibliography}
 704 
    \end{thebibliography}
703 
\end{document}
 705 
\end{document}
704 
 
 706