Using Model Checkers in a Course on Operating Systems
Background
Each year, thousands of Computer Science students are exposed to a course on operating systems.
Typically, these students study concepts, structure and mechanisms of operating systems using one of the
many good textbooks that are available (Tanenbaum, Stallings, Nutt, Silberschatz & Galvin,..).
All these textbooks contain one or more chapters on principles of concurrency, which
discuss fundamental concepts such as mutual exclusion algorithms, sempahores, monitors, message passing,
deadlock and starvation.
The concepts are introduced informally: the authors do not want to bother their readers
with formal correctness proofs since this would distract attention from the key issues they
want to get accross. Correctness proofs of of the algorithms is typically left as an exercise and
there is no mentioning of formal methods or model checking.
We think that after 20 years of research on model checking this technology has become sufficiently
mature and it is time to change the way in which we teach principles of concurrency:
-
Using the input language of model checkers it is straightforward to formalize
concurrency algorithms in terms of networks of communicating state machines.
If we explain concurrency algorithms then it is often better to use pseudo code
or text rather than logical formulas. However, it greatly help to
understand things when they know how the pseudo code and
text correspond to precise mathematical models and assertions about these models.
By specifying state transitions, we make made explicit which operations are
atomic and which operations are not, an issue that is vital to understanding the algorithms.
-
Using the (graphical) simulators provided by some modern model checkers such as Uppaal,
it becomes very easy to visualize the behavior of concurrency algorithms and certain
problematic traces in which mutual exclusion is violated, starvation occurs, etc.
-
Using the model checker students can convince themselves of the correctness of algorithms
without having to spend a lot of effort on tedious, manual correctness proofs
(which are of independent interest but belong in a course on program correctness
rather than in a course on operating systems).
Examples
Here are some examples of Uppaal models of mutual exclusion algorithms as discussed
in Chapter 5 and Appendix A of
William Stallings,
Operating Systems: Internals and Design Principles, 5th ed,
Prentice-Hall, 2005
(models constructed with help of Bart Meulenbroek):
Assignment
Build a Uppaal model for the "solution" to the mutual exclusion problem
described in Problem 5.5 in Stallings' book. Use Uppaal to exhibit
that this solution is flawed.
Instructions
You can download the latest version of Uppaal from http://www.uppaal.com.
Uppaal has also been installed on the Windows machines within the Science Faculty, and
can be started via
start->run-> type: "\\manus\xpcursus\ita\uppaal\uppaal.cmd"
When constructing your model, you may use the above examples as a source for inspiration.
Check whether you model satisfies some natural criteria
for a good model.