Please email me your completed SMV program, including your specifications and fairness constraints, as well as an intuitive description of any bugs you found.
I hope this is an easy and fun exposure to the NuSMV model checker, and CTL model checking in general. NuSMV is a fairly recent re-creation and extension of SMV, which was the original symbolic model checker. There's no an even newer NuXMV, so NuSMV appears to be no longer actively maintained, but it's open-source and NuXMV isn't. (However, you might consider using NuXMV for your project instead of NuSMV, as it's free for non-commercial use.)
Mutual exclusion is a classic problem from concurrent programming, operating systems, distributed systems, etc. The basic problem is to write code for two programs that execute at the same time, and you don't want both of them to execute a special part of the code (called the "critical section") at the same time. In practice, the critical section would be the code required to access a shared resource (shared variable, data file, printer, etc.).
One correct solution (based on Leslie Lamport's Bakery Algorithm) is as follows:
-- Global variables: n1, n2, both initialized to 0.
-- Process P1
-- 1: n1 = 1
-- 2: n1 = n2+1;
-- 3: if (n2!=0)&(n2<n1) goto 3 -- waiting for critical section
-- 4: /* this line is the critical section */
-- 5: n1 = 0
-- 6: goto 1
-- Process P2
-- 1: n2 = 1
-- 2: n2 = n1+1;
-- 3: if (n1!=0)&(n1<n2) goto 3 -- waiting for critical section
-- 4: /* this line is the critical section */
-- 5: n2 = 0
-- 6: goto 1
Each statement gets executed atomically (in one step), but you can make
no assumptions about which process gets to execute at any given moment
in time. One problem with this solution is that the global variables
can be arbitrarily large integers, which is not implementable in practice.
In an attempt to get around this problem, I've inserted an extra loop
between statements 1 and 2, which waits in case the global variables get too
large. Your job is to use SMV to determine if my attempted fix was successful
or not. (Hint: It's not!)
My SMV description of this protocol contains additional details about exactly what properties a correct solution must obey, and what assumptions you can make about the process scheduling. You will need to add CTL (or LTL) specifications to tell SMV what properties you want to check, as well as fairness constraints to eliminate vacuous error traces (e.g. P1 never gets to the critical section because it never gets to execute at all).
For the assignment, you'll need to get
the NuSMV model checker.
You can download and build it yourself. However, I'm finding that the
newest version that used to build easily on our department Linux machines
isn't building correctly anymore (apparently problems between Python 2 and 3).
Fortunately, they also have pre-compiled binaries for Linux, Windows, and
MacOS, so you all should be in good shape.
Or on the CS department Linux machines, I put the pre-compiled binary
in /isd/users/software/NuSMV-2.6.0-Linux/bin/NuSMV
You'll also definitely need to browse the NuSMV manual.