[ltt-dev] Selective wakeup formal model update
mathieu.desnoyers at efficios.com
Mon Aug 29 10:26:20 EDT 2011
* Paolo Bonzini (pbonzini at redhat.com) 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
Operating System Efficiency R&D Consultant
More information about the lttng-dev