[ltt-dev] [PATCH] urcu-qsbr: avoid useless futex wakeups and burning CPU for long grace periods

[Paolo Bonzini]

>>> @@ -136,7 +137,11 @@ extern int32_t gp_futex;
>>> */
>>> static inline void wake_up_gp(void)
>>> {
>>> - if (unlikely(uatomic_read(&gp_futex) == -1)) {
>>> + if (unlikely(_CMM_LOAD_SHARED(rcu_reader.waiting))) {
>>> + _CMM_STORE_SHARED(rcu_reader.waiting, 0);
>>
>> Commenting this memory barrier would be helpful too.
>
> Ok.

I tried updating the formal model, but I had to basically rewrite it to 
model the futex primitives and the list move algorithm used by urcu.  I 
basically model a parity-flipping RCU and run the waker and waiter 
infinitely, asserting that progress states (parity flips) are reached 
infinite times.

My ProMeLa-fu is just a few hours old, so a careful review is 
appreciated.  However, the model seems to be okay: it passes, and more 
importantly it fails if I modify it to trigger known problems (missing 
write barriers especially).

The attached patches do the following:

1) rewrite the futex.spin model to match your proposed, simpler change;

2) add the optimization to tell waker threads whether they are still 
being waited on;

3) change the futex_progress_late_dec model to trigger a different 
failure, namely the missing memory barrier in the first version I sent 
of the patch.

Please let me know what you think about them.

Thanks!

Paolo
-------------- next part --------------
A non-text attachment was scrubbed...
Name: futex-model.patch
Type: text/x-patch
Size: 8325 bytes
Desc: not available
URL: <http://lists.casi.polymtl.ca/pipermail/lttng-dev/attachments/20110815/874dbe71/attachment-0003.bin>