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, and likely some non-deliberate bugs, too) 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, and several groups have kept the system updated. (Indeed, last I checked (which admittedly was before the pandemic), Murphi was still used at a couple major computer makers when developing cache coherence protocols.) 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., newcastle.cs.ubc.ca, selkirk.cs.ubc.ca, okanagan.cs.ubc.ca, begbie.cs.ubc.ca, kokanee.cs.ubc.ca).

• If you want to install your own version on your own machine, CMurphi 5.5.0 is the current version. I was able to download and install this without problem on my home Ubuntu Linux box. Note that the download comes with a pre-built executable (in the directory src/mu) that seemed to work fine. If you just type "make", it also compiled fine on my home machine. Note, however, that if you try to do a completely clean build (or make any modifications to the mu.l or mu.y files) you will need to install a tool called byacc (which is the free, Berkeley version of yacc, which was the tool we originally used for Murphi), which is less commonly used than the more popular bison. (These tools generate the parser based on the grammer for the Murphi input language.) You'll also need flex, which is usually already installed in a lot of Linux distributions. To install these, you should be able to just do sudo apt update followed by sudo apt-get install byacc flex. If you're using Windows or a Mac, I can't guarantee that this will build for you. I will try to test this out on my new Windows machine under wsl. (Update: With Ubuntu under wsl on Windows, everything seems to work exactly like normal Ubuntu.) My Mac is so old that even if it works, that won't provide useful feedback on how well this will install on a newer Mac. Hopefully, things should be similar enough that everything should be buildable. (If you hit insurmountable problems, you can rely on my version on the CS departmental servers.)
• In prior years, using an older version of CMurphi (5.4.9), some students encountered problems with segfaults, due to code that is considered undefined by modern compilers. Hat tip to former 513 student Stuart Hoad for tracking down this git repo, where a wonderful grad student Nik Unger fixed a bunch of these problems in the CMurphi code. If you have problems with CMurphi 5.5.0, try using Nik Unger's version instead. The build process will be the same.
• If you want to use the version I've installed on a CS department machine, here is a sample makefile (that uses CMurphi 5.5.0) and here is a sample makefile (that uses Nik Unger's version).
• If you're curious, there's a nice Wikipedia page on Murphi and various spin-off projects (but as bit-rot sets in, many links are dead).

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.