* Paolo Bonzini ([email protected]) wrote: > 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).
Yep, sounds good. > >> 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. Sure, it's now in the formal-models branch, in urcu-qsbr-selective-wakeup. Thanks, Mathieu > > Paolo -- Mathieu Desnoyers Operating System Efficiency R&D Consultant EfficiOS Inc. http://www.efficios.com _______________________________________________ ltt-dev mailing list [email protected] http://lists.casi.polymtl.ca/cgi-bin/mailman/listinfo/ltt-dev
