Verifying Fluke IPC

This is a project completed for Ganesh Gopalakrishnan's CS 611 course offered in the Fall of 1996, here at the U of U.

Patrick Tulmann, John McCorquodale, Ajay Chitturi, Godmar Back, and Jeff Turner worked on it real hard.

Our goal was to develop a model of Fluke's IPC mechanism in Promela and verify freedom from deadlock, avoidance of livelock, and other features with SPIN.

Our paper, published in the proceedings of HotOS-VI is now available from the Flux paper server (Full paper, gzip'd postscript) (Abstract, html). Our project report in postscript, is also available.

A tarball (122K) of our sources (including the HotOS paper, .tex source to all our documentation, and project reports) is also available. This has some good generic stuff that might be good for other SPIN verification efforts. But, much of it won't make any sense without access to the Fluke source (latest estimate is late two months from any given day).

So far, three presentations on this project have been given. One is a short 15 minute overview. (PowerPoint, HTML) The second is a longer 1 hour review. (Color Postscript, B&W Postscript, PowerPoint, HTML) The third is the HotOS presentataion (10 minutes plus some backup slides.) (PowerPoint, HTML)

In the process of using SPIN to model our system, we developed several tools. (Well, tools is a strong word, perhaps hacks is a better word.)

For more information on Fluke, see the Flux Project home page.

For more information on SPIN, see the NetLib SPIN archive.

Patrick Tullmann <>