Remove useless busy-looping, useless in Promela. Same semantic as the
new code:
Quoting Michel Dagenais <email address hidden>:
> http://spinroot.com/spin/Man/condition.html
> In Promela , a standalone expression is a valid statement. Execution
> of a condition statement is blocked until the expression evaluates to
> a non-zero value (or, equivalently, to the boolean value true ).
>
> http://spinroot.com/spin/Man/separators.html
> The semicolon and the arrow are equivalent statement separators in
> Promela. The convention is to reserve the use of the arrow separator
> to follow condition statements. The arrow symbol can thus be used to
> visually identify those points in the code where execution could
> block.
The nto1 selective wakeup model introduced by Paolo was:
a) too complex (tried to model the full-blown RCU rather than a simple
queue system)
b) did not model progress with wakers running for a limited amount of
iterations, only with wakers running infinitely often (which
therefore does not prove anything).
What we really want to model here is what happens if we have wakers
running a few times, and then not running for a very long time: can we
end up with a missed wakeup, and therefore end up with an enqueued entry
but with the waiter waiting forever ?
