Department of Computer Science
CPSC 513: Integrated System Design


Verifying Token Coherence with Murphi:

Please email me your final or best modified program (and optionally some results showing the state space savings you were able to achieve, if any), as well as a description of the properties you checked and what the bug(s) was/were in my protocol implementation. (Step-by-step instructions are in the comments in the starting Murphi model I provide you.)

For this assignment, you're going to use Murphi to verify my implementation (with two deliberate bugs inserted) of a simplified version (no persistent requests) of TokenB, a reasonably modern and particularly elegant cache coherence protocol. This paper describes the problem of cache coherence and the proposed protocol. You'll definitely want to at least skim the paper.

tokenB.m is the buggy protocol implementation I wrote for you.

Murphi is very easy to use, but it's quite an old system. (It was part of my PhD, in fact!) Fortunately, it has been popular enough that there are a variety of variants available. We're going to use a rewritten tool called CMurphi, but I'm not asking you to do anything more than use it in original Murphi mode.

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 that computes reachability for the specific problem you started with. Feel free to install your own version of Murphi, or use mine, which should run on any departmental 64-bit Linux machine (e.g., okanagan.cs.ubc.ca, begbie.cs.ubc.ca, kokanee.cs.ubc.ca).

You will probably also want to look at the Murphi User Manual, which is also located in the doc directory of the Murphi distribution. But you can probably figure out a lot just by looking at the code.

When you run your verifier, you'll probably want to use the -td option to print a trace if it finds an error. You may also need the -m option to tell the verifier to use more memory, and the -d option to tell Murphi where to store a temporary file. E.g.,
tokenB -td -m 1000 -d .
will use 1000 megabytes for the hash table, and store a temporary queue in the current directory. (Note the period after the -d ! That's the name of your current directory.) You can use the -h option to print out a list of options.