another one of my experimental rw-mutex algorihtms; in Relacy...
Chris M. Thomasson
sometime in 2006. I have always wanted to verify its correctness, so I coded
it up in Relacy:
http://relacy.pastebin.com/faf3155c
It works! However, it can indeed starve writers under heavy read contention.
If this happens during the test, Relacy should spit out a livelock error. I
posted a fix to this starvation issue, and plan to test it in Relacy as
well.
RELACY ROCKS!!!!!!!!!!!!!
=^D
Chris M. Thomasson
"Chris M. Thomasson" <n...@spam.invalid> wrote in message
news:tR7Jl.72043$_R4....@newsfe11.iad...
> This is an experimental algorihtm that I posted a while back, I think
> sometime in 2006. I have always wanted to verify its correctness, so I
> coded it up in Relacy:
>
>
> http://relacy.pastebin.com/faf3155c
>
>
>
> It works!
The version above uses a strong compare-and-swap. C++0x does not guarentee
this property. Here is a version that uses weak compare-and-swap:
http://relacy.pastebin.com/f1c697a96
The difference between the two is that weak CAS can fail spuriously while
strong CAS cannot. I guess the C++0x guys did this to cope with CAS
emulations created with LL/SC.
Anyway, the algorihtm still works with weak CAS.
Dmitriy Vyukov
> It works! However, it can indeed starve writers under heavy read contention.
> If this happens during the test, Relacy should spit out a livelock error. I
> posted a fix to this starvation issue, and plan to test it in Relacy as
> well.
There is not so much documentation for the Relacy currently :( at
least I may try to provide some bits ad-hoc....
There are classes backoff, linear_backoff and exp_backoff. backoff has
a constant backoff value of 1. linear_backoff linearly increases it's
backoff value: 1, 2, 3... exp_backoff doubles it's backoff value: 1,
2, 4... Backoff value may be roughly treated as for how many "cycles"
thread steps out of the game.
backoff class is requiredwhen thread will unconditionally complete an
operation but just need some amount of cycles:
int x = 0;
// thread 1
while (x == 0)
;
// thread 2
x = 1
This is formally non-terminating (live-locking) program (assume only
thread 1 will always be scheduled). To fix this we must add backoff:
// thread 1
backoff b;
while (x == 0)
b.yield($);
linear_backoff and exp_backoff are reuiqred when thread will NOT
unconditionally complete an operation and need some amount of
"adjacent" cycles. Consider:
// thread 1
for (;;)
{
if (make_STM_operation())
break;
}
// thread 2
for (;;)
{
if (make_STM_operation())
break;
}
This indeed may live-lock. backoff (with constant back-off value) will
not help here (program will still live-lock), but linear_backoff will:
// thread 1
linear_backoff b;
for (;;)
{
if (make_STM_operation())
break;
else
b.yield($);
}
exp_backoff will faster achieve required amount of "adjacent" cycles,
but the larger the back-off value the more thread interleaving are
excluded from consideration. So one must prefer linear_backoff, until
it will cause too long execution histories.
One may construct own back-off policy. For example:
typedef backoff_t<1, 2> my_linear_backoff;
will produce back-off values 1, 3, 5, 7...
--
Dmitriy V'jukov
Chris M. Thomasson
news:fb6bfce5-9823-490d...@k19g2000prh.googlegroups.com...
On 27 О©╫О©╫О©╫, 05:26, "Chris M. Thomasson" <n...@spam.invalid> wrote:
> > It works! However, it can indeed starve writers under heavy read
> > contention.
> > If this happens during the test, Relacy should spit out a livelock
> > error. I
> > posted a fix to this starvation issue, and plan to test it in Relacy as
> > well.
> There is not so much documentation for the Relacy currently :(
Yeah... Creating extensive and complete documentation can be a major pain in
the as$!
;^)
So far, I think I am getting the hang of coding up algorihtms in Relacy.
> at
> least I may try to provide some bits ad-hoc....
> There are classes backoff, linear_backoff and exp_backoff. backoff has
> a constant backoff value of 1. linear_backoff linearly increases it's
> backoff value: 1, 2, 3... exp_backoff doubles it's backoff value: 1,
> 2, 4... Backoff value may be roughly treated as for how many "cycles"
> thread steps out of the game.
> backoff class is requiredwhen thread will unconditionally complete an
> operation but just need some amount of cycles:
> [...]
> One may construct own back-off policy. For example:
> typedef backoff_t<1, 2> my_linear_backoff;
> will produce back-off values 1, 3, 5, 7...
Ahhh! Thanks. That's very helpful!