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.