E.6.3 Alternative Approach: Proof of Correctness
An informal proof [McK07b]
follows:
- For synchronize_qrcu() to exit too early, then
by definition there must have been at least one reader
present during synchronize_qrcu()'s full
execution.
- The counter corresponding to this reader will have been
at least 1 during this time interval.
- The synchronize_qrcu() code forces at least one
of the counters to be at least 1 at all times.
- Therefore, at any given point in time, either one of the
counters will be at least 2, or both of the counters will
be at least one.
- However, the synchronize_qrcu() fastpath code
can read only one of the counters at a given time.
It is therefore possible for the fastpath code to fetch
the first counter while zero, but to race with a counter
flip so that the second counter is seen as one.
- There can be at most one reader persisting through such
a race condition, as otherwise the sum would be two or
greater, which would cause the updater to take the slowpath.
- But if the race occurs on the fastpath's first read of the
counters, and then again on its second read, there have
to have been two counter flips.
- Because a given updater flips the counter only once, and
because the update-side lock prevents a pair of updaters
from concurrently flipping the counters, the only way that
the fastpath code can race with a flip twice is if the
first updater completes.
- But the first updater will not complete until after all
pre-existing readers have completed.
- Therefore, if the fastpath races with a counter flip
twice in succession, all pre-existing readers must have
completed, so that it is safe to take the fastpath.
Of course, not all parallel algorithms have such simple proofs.
In such cases, it may be necessary to enlist more capable tools.
Paul E. McKenney
2011-12-16