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 _______________________________________________ ltt-dev mailing list [email protected] http://lists.casi.polymtl.ca/cgi-bin/mailman/listinfo/ltt-dev
