Quick Quiz 1:
Why is there an unreached statement in
locker? After all, isn't this a full
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
Answer: There are several:
- The declaration of "sum" should be moved to within
the init block, since it is not used anywhere else.
- 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?).
- 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
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"
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
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
Answer: Yes. To see this, delete these lines and run the model.
Alternatively, consider the following sequence of steps:
- One process is within its RCU read-side critical
section, so that the value of ctr is zero and
the value of ctr is two.
- 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.
- A second updater starts executing, and fetches the value
of ctr, which is zero.
- The first updater adds one to ctr, flips
the index (which now becomes zero), then subtracts
one from ctr (which now becomes one).
- The second updater fetches the value of ctr,
which is now one.
- 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.
to post comments)