[ltt-dev] Selective wakeup formal model update

[Mathieu Desnoyers]

Hi Paolo,

I had to update your formal model for the selective wakeup model:

commit fda9aff00dcdf7cb49892d79f861d0acfb475514
Author: Mathieu Desnoyers <mathieu.desnoyers at efficios.com>
Date:   Sat Aug 27 11:59:42 2011 -0400

    Update nto1 selective model
    
    The nto1 selective wakeup model introduced by Paolo was:
    
    a) too complex (tried to model the full-blown RCU rather than a simple
       queue system)
    b) did not model progress with wakers running for a limited amount of
       iterations, only with wakers running infinitely often (which
       therefore does not prove anything).
    
    What we really want to model here is what happens if we have wakers
    running a few times, and then not running for a very long time: can we
    end up with a missed wakeup, and therefore end up with an enqueued entry
    but with the waiter waiting forever ?

See

http://git.lttng.org/?p=userspace-rcu.git;a=blob;f=futex-wakeup/nto1-selective/futex.spin;h=6f854fceefba73dfbc3781d04734b75590175159;hb=refs/heads/formal-model

Thanks!

Mathieu

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