Using Promela and Spin - Quick Quiz Answers

Quick Quiz 1: Why is there an unreached statement in locker? After all, isn't this a full state-space search???

Answer: The locker process is an infinite loop, so control never reaches the end of this process. However, since there are no monotonically increasing variables, Promela is able to model this infinite loop with a small number of states.

Quick Quiz 2: What are some Promela code-style issues with this example?

Answer: There are several:

1. The declaration of "sum" should be moved to within the init block, since it is not used anywhere else.
2. The assertion code should be moved outside of the initialization loop. The initialization loop can then be placed in an atomic block, greatly reducing the state space (by how much?).
3. The atomic block covering the assertion code should be extended to include the initialization of "sum" and "j", and also to cover the assertion. This also reduces the state space (again, by how much?).

Quick Quiz 3: Is there a more straightforward way to code the do-od statement?

Answer: Yes. Replace it with if-fi and remove the two "break" statements.

Quick Quiz 4: Why are there atomic blocks at lines 12-21 and lines 44-56, when the operations within those atomic blocks have no atomic implementation on any current production microprocessor?

Answer: Because those operations are for the benefit of the assertion only. They are not part of the algorithm itself. There is therefore no harm in marking them atomic, and so marking them greatly reduces the state space that must be searched by the Promela model.

Quick Quiz 5: Is the re-summing of the counters on lines 24-27 really necessary???

Answer: Yes. To see this, delete these lines and run the model.

Alternatively, consider the following sequence of steps:

1. One process is within its RCU read-side critical section, so that the value of ctr[0] is zero and the value of ctr[1] is two.
2. An updater starts executing, and sees that the sum of the counters is two so that the fastpath cannot be executed. It therefore acquires the lock.
3. A second updater starts executing, and fetches the value of ctr[0], which is zero.
4. The first updater adds one to ctr[0], flips the index (which now becomes zero), then subtracts one from ctr[1] (which now becomes one).
5. The second updater fetches the value of ctr[1], which is now one.
6. The second updater now incorrectly concludes that it is safe to proceed on the fastpath, despite the fact that the original reader has not yet completed.

---

(Log in to post comments)