[ltt-dev] Selective wakeup formal model update

[Mathieu Desnoyers]

* 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
urcu-qsbr-selective-wakeup.

Thanks,

Mathieu

>
> Paolo

-- 
Mathieu Desnoyers
Operating System Efficiency R&D Consultant
EfficiOS Inc.
http://www.efficios.com