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. (BTW, some students have pointed out in the past that I didn't really model the protocol in the paper accurately, which is something I always meant to go back and fix. But I've also deliberately added bugs, aside from maybe not being faithful to 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. (Caution: See below for links and advice on how to build and install CMurphi!)

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

• If you want to use the version I've installed on a CS department machine, here is a sample makefile.
• Alternatively, you might try installing your own copy of Murphi. Unfortunately, bit rot is setting in, even for CMurphi. In particular, two problems afflict the official CMurphi download: (1) there are places where the code depends on behavior that is considered illegal/undefined by modern compilers, and (2) the code depends on a tool called byacc (which is the free, Berkeley version of yacc, which was the tool we originally used for Murphi), and this is not a widely used tool anymore. To solve (1), one of your fellow students kindly tracked down this git repo, where some wonderful grad student fixed all the CMurphi code. So, that's where you should pull the sources from. For (2), on a typical Linux distribution, if you don't have byacc installed already, you should be able to install it easily with "sudo apt-get update" followed by "sudo apt-get install byacc". For me, on the departmental servers, I don't have root access, so I went to this page, which seemed legit, downloaded the sources from there, and then did "configure" followed by "make", and amzingly enough, it worked. If you do this, you'll have to modify the CMurphi makefile to use the byacc that you just built. Note that if you're using Windows or a Mac, I can't guarantee that this will build for you. On Windows under cygwin, or under Mac OS, things should be similar enough that everything should be buildable, but I haven't tested this. (If you hit insurmountable problems, try the other assignment, or you can rely on my version on the CS departmental servers.)
• If you're curious, this page at the University of Utah lists many Murphi versions and spin-off projects.

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.