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.)

• promela.el: An emacs promela mode. I developed this under Xemacs, but it should also work in FSF emacs. Its a lame hack and does little more than fontification and really poor auto-indentation. But, you do get a neat little "(Promela)" down on the modeline. Feedback is appreciated.
• prMunge: A Perl script that transforms a CPP processed promela file. It reformats its input to optimize line breaks.
• dumpMunge: A Perl script that takes the result of a spin -a dump and reformats it. It looks more like the Xspin trace after processing.

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