Relacy question
Dmitriy Vyukov
First of all, I'd like to thank you for releasing Relacy, it's a great
piece of software that really made my life much easier. I no longer
have to worry that I missed some possible (but very unprobable)
scenario, big relief.
Recently, I've been testing my double-ended class (C++ version of
Herlihy's C# algorithm) and I encountered interesting Relacy messages.
It's very possible that it's not really Relacy related, it's just
invalid code and I'm missing something here, but I tried to analyze it
and can't find good explanation. Basic problem is that sometimes I get
[NOT CURRENT] error messages, ie:
[14] 1: <00983F44> atomic load, value=1 [NOT CURRENT], order=acquire,
in rde::LockFreeDEQueue<int>::PopTop, lockfreedequeue.h(52)
Is it possible to get obsolete value, when reading aligned 32-bit
value using acquire/release semantics? In this example, it looks like
(roughly):
- PushBottom:
const int32 bottom = m_bottom.load
(rl::memory_order_acquire);
m_data[bottom] = t;
m_bottom.store(bottom + 1, rl::memory_order_release);
- PopTop:
const int32 bottom = m_bottom.load
(rl::memory_order_acquire);
Relacy messages:
[12] 0: <00983F44> atomic store, value=2, (prev value=1),
order=release, in rde::LockFreeDEQueue<int>::PushBottom,
lockfreedequeue.h(44)
[13] 1: <00983F68> atomic load, value={0,0}, order=acquire, in
rde::LockFreeDEQueue<int>::PopTop, lockfreedequeue.h(49)
[14] 1: <00983F44> atomic load, value=1 [NOT CURRENT], order=acquire,
in rde::LockFreeDEQueue<int>::PopTop, lockfreedequeue.h(52)
I can 'force' it to work by using seq_cst model, however I was under
impression it shouldn't be necessary in such situation?
(side note: I also get [NOT CURRENT] messages when trying to
load_acquire data that has been stored using compare_exchange_strong &
rl::memory_order_seq_cst, but here I'll be investigating it further, I
probably should load it with seq_cst as well, not sure how acquire
load semantics works with seq_cst store).
-- Maciej
Dmitriy Vyukov
> Hello,
> First of all, I'd like to thank you for releasing Relacy, it's a great
> piece of software that really made my life much easier. I no longer
> have to worry that I missed some possible (but very unprobable)
> scenario, big relief.
> Recently, I've been testing my double-ended class (C++ version of
> Herlihy's C# algorithm) and I encountered interesting Relacy messages.
> It's very possible that it's not really Relacy related, it's just
> invalid code and I'm missing something here, but I tried to analyze it
> and can't find good explanation. Basic problem is that sometimes I get
> [NOT CURRENT] error messages, ie:
> [14] 1: <00983F44> atomic load, value=1 [NOT CURRENT], order=acquire,
> in rde::LockFreeDEQueue<int>::PopTop, lockfreedequeue.h(52)
> Is it possible to get obsolete value, when reading aligned 32-bit
> value using acquire/release semantics?
Yes, of course. The most well known example is:
//thread 1
x.store(1, std::memory_order_release);
R1 = y.load(std::memory_order_acquire);
//thread 2
y.store(1, std::memory_order_release);
R2 = x.load(std::memory_order_acquire);
The outcome R1==R2==0 is completely possible. However there is no
sequentially consistent executions in which R1==R2==0 is possible.
If you need sequential consistency (no 'non current') then you need to
use seq_cst ordering.
You can find more info on C# memory model (volatile stores/loads are
release/acquire) in Joe Duffy blog:
http://www.bluebytesoftware.com/blog/2008/07/17/LoadsCannotPassOtherLoadsIsAMyth.aspx
http://www.bluebytesoftware.com/blog/2007/11/10/CLR20MemoryModel.aspx
seq_cst ordering works IFF ALL operations are seq_cst (they are seq
consistent regarding each other only). If store is seq_cst and load is
acquire, then I think it effectively equal to store is release and
load is acquire.
--
Dmitriy V'jukov