Department of Computer Science
CPSC 513: Integrated System Design

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 an actively maintained recreation and extension of SMV, which was the original symbolic model checker. NuSMV is mostly backward compatible with the original SMV (which is what I originally designed this assignment for), but with a lot of new features and extensions.

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, or download a pre-compiled binary, or on the CS department Linux machines, you can use the binary I built in /isd/users/software/NuSMV-2.6.0/NuSMV/build/bin/NuSMV

You'll also definitely need to browse the NuSMV manual.