Project 4:

Well, I just wasted several hours trying to come up with a directory-based cache coherence protocol that is sufficiently real to be interesting and educational, yet sufficiently small to be reasonably doable. It's hard! (No wonder people make mistakes in real life...)

Instead, I'm going to ask you to work on the Distributed List Protocol example. This is a simple example based on a real protocol problem that arose in a (you guessed it) directory-based cache coherence protocol. The basic idea is that you have several independent processors (called "cells" in the example) that can independently decide to add or delete themselves from a list. Each cell has only a next pointer, so the list is a singly-linked, circular list. The cells communicate by sending messages to each other, but the network does NOT preserve message order.

Fortunately, one cell, called the Head Cell, is always guaranteed to be in the list. So, if a cell that isn't in the list decides it wants in, it just sends a message to the Head Cell. The Head Cell points its own next pointer at the cell that wants to be added, and then sends a reply to that cell telling it what the Head Cell used to point to. When the original cell gets the reply, it points its next pointer to the cell that the Head Cell used to point to, thus splicing the new cell into the list immediately after the Head Cell.

Deletion is tricker. If a cell decides to leave the list, it must somehow tell its predecessor to point to its successor. However, since the list is singly-linked, it has no idea who its predecessor is. In the version of the protocol that I am giving you, there is a special "pred" message that circulates continuously in the list. When a cell wants to leave the list, it waits until it receives the pred message, which tells it who the predecessor cell is. It can then send the predecessor cell a message to change its next pointer to bypass the cell.

Your mission is to change the protocol so that the pred message isn't needed. You MUST keep the list singly-linked. I know of a simple solution that uses only four message types total. I hope this is an easy and fun exposure to the Murphi explicit-state verifier.

Murphi is very easy to use, but the set-up can be annoying sometimes because of C++ incompatibilities and the fact that it relies on numerous include files. Basically, the Murphi compiler converts a Murphi description into a C++ program. You then compile the C++ program, and the resulting executable is a verifier for the specific problem you started with. Feel free to install your own version of Murphi, or use mine, which should run on Columbia, Cascade, and Thor. If you want to use the version I've installed, here is a sample makefile. The Murphi description you should start from is called newlist6.m. You will probably also want to look at the Murphi User Manual, although you can probably figure out a lot, just by looking at the code. There are many other examples in my Murphi directory.