E.6.1 Running the QRCU Example
Keywords: perfbook_html

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