[ltt-dev] Selective wakeup formal model update

[Paolo Bonzini]

On 08/27/2011 06:07 PM, Mathieu Desnoyers wrote:
>      Update nto1 selective model
>
>      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 ?
>
> See
>
> http://git.lttng.org/?p=userspace-rcu.git;a=blob;f=futex-wakeup/nto1-selective/futex.spin;h=6f854fceefba73dfbc3781d04734b75590175159;hb=refs/heads/formal-model
>
> Thanks!

Makes sense regarding the complexity.

Regarding (b), I am not sure I understand.  It is true that wakers run 
infinitely often, but they do nothing until all of them have progressed. 
  Also, since the queue state is binary, Spin should exhaust its state 
space without running wakers more than twice; it should be possible to 
add an assertion about this.

I think we are simply testing different things.  Perhaps we want to keep 
both models?

Paolo