[ltt-dev] Selective wakeup formal model update

Mathieu Desnoyers 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



> Paolo

Mathieu Desnoyers
Operating System Efficiency R&D Consultant
EfficiOS Inc.

More information about the lttng-dev mailing list