E.6.1 Running the QRCU Example

To run the QRCU example, combine the code fragments in the previous section into a single file named qrcu.spin, and place the definitions for spin_lock() and spin_unlock() into a file named lock.h. Then use the following commands to build and run the QRCU model:



spin -a qrcu.spin
cc -DSAFETY -o pan pan.c
./pan



Table: Memory Usage of QRCU Model
updaters readers # states MB
1 1 376 2.6
1 2 6,177 2.9
1 3 82,127 7.5
2 1 29,399 4.5
2 2 1,071,180 75.4
2 3 33,866,700 2,715.2
3 1 258,605 22.3
3 2 169,533,000 14,979.9


The resulting output shows that this model passes all of the cases shown in Table [*]. Now, it would be nice to run the case with three readers and three updaters, however, simple extrapolation indicates that this will require on the order of a terabyte of memory best case. So, what to do? Here are some possible approaches:

  1. See whether a smaller number of readers and updaters suffice to prove the general case.
  2. Manually construct a proof of correctness.
  3. Use a more capable tool.
  4. Divide and conquer.

The following sections discuss each of these approaches.

Paul E. McKenney 2011-12-16