Hi Paolo, I had to update your formal model for the selective wakeup model:
commit fda9aff00dcdf7cb49892d79f861d0acfb475514 Author: Mathieu Desnoyers <[email protected]> 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 _______________________________________________ ltt-dev mailing list [email protected] http://lists.casi.polymtl.ca/cgi-bin/mailman/listinfo/ltt-dev
