new futex model
authorPaolo Bonzini <pbonzini@redhat.com>
Wed, 17 Aug 2011 09:49:08 +0000 (05:49 -0400)
committerMathieu Desnoyers <mathieu.desnoyers@efficios.com>
Wed, 17 Aug 2011 09:49:08 +0000 (05:49 -0400)
commit2a8044f3493046fcc8c67016902dc7beec6f026a
tree98ab5db34d814cea3238d8eba9797761b51e1e4e
parent307daf8c9b05b394c48c069083891d6dc14ff345
new futex model

Rewrite the model to include the futex primitives and the list
move algorithm used by urcu.  The model implements a full-blown
parity-flipping RCU where grace period waits are driven exclusively
by futexes.  It runs the waker and waiter infinitely, asserting
that progress states (parity flips) are reached infinite times.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
futex-wakeup/DEFINES
futex-wakeup/futex.ltl
futex-wakeup/futex.spin
This page took 0.024499 seconds and 4 git commands to generate.