[ltt-dev] Selective wakeup formal model update

[Paolo Bonzini]

On 08/29/2011 03:12 PM, Mathieu Desnoyers wrote:
> Hrm, thinking about it a little more, this would be an expected beahvior
> with QSBR if the reader threads are not put offline.

Yes, that's indeed what I was trying to model.  I didn't care about 
threads going offline, because I was more interested in missed wakeups 
due to memory reordering _even when the wakers going quiescent 
infinitely often_.

> So I think we need
> to represent the offline state if we really want to model progress,
> because otherwise we only really show the cases where readers report
> their quiescent state infinitely often.

Yes, I think we can do that effectively with a non-deterministic Promela 
model ("either" report a quiescent state "or" go offline forever).

> And I agree we can keep that model somewhere (when we get it to work for
> offline case), but it does not belong in the futex-wakeup/ model
> directory, more within a urcu-specific directory.

Good idea.  Can you revert it somewhere?  I'll try to add support for 
offline states as outlined above.

Paolo