Re: Relacy CAS release + acquire error?

[Dmitry Vyukov]

On Mon, Dec 19, 2016 at 4:18 AM, Alex Khripin <akhr...@alum.mit.edu> wrote:
> Hi Dmitry,
> First -- relacy is great, thank you for providing this tool and all the
> other stuff on 1024cores.
>
> Second -- I ran into a hiccup. This might be something I don't properly
> understand in the C++11 spec, but, relacy does not seem to support
>
> compare_exchange_strong(foo, bar, rl::mo_release, rl::mo_acquire)
>
> When RL_VERIFY is enabled, this triggers an error:
> RELACY INTERNAL ASSERT FAILED: 'collecting_history()' at
> ../../relacy/context_base_impl.hpp:60 (exec_log)
>
> Reading the code, it looks like if the normal memory model is release, then
> the only failure model supported is relaxed.
>
> atomic.hpp line 338 in the big compare_exchange switch statement
>
> I know the specification prohibits the failure memory order from being
> stronger than the success order -- I am not 100% sure, but I think the above
> ordering (success = release, failure = acquire) does satisfy that
> requirement.
>
> This is mostly academic -- I can set the success order to acq_rel -- but it
> did take me some time to figure out what was going on. I am curious now if I
> am completely off base, or if this is a missing combination.


+relacy mailing list

Hi Alex,

The stronger requirement is somewhat vague as there are unordered memory orders.
But I always read it as relacy implements it -- failure order must be
equal or weaker. Do you have any indication that release/acquire is an
allowed combination?

[Miral Mirality]

On 19/12/2016 20:29, "Dmitry Vyukov" <dvy...@gmail.com> wrote:

The stronger requirement is somewhat vague as there are unordered memory orders.
But I always read it as relacy implements it -- failure order must be
equal or weaker. Do you have any indication that release/acquire is an
allowed combination?

I think the relevant paper is this one:

    http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2016/p0418r2.html

According to cppreference, either this or something like it is on track for inclusion in C++17.

So I think the ruling is that currently it's not legal, but in future it might be.

[Alex Khripin]

The only suggestive evidence I have is -- GCC allows release + acquire, but produces an error on relaxed + acquire

So, it does have a strength check, and release + acquire does pass it. 

Another data point is that the std::memory_order enum is written starting at relaxed going up through seq_cst -- so it looks sort of like it's in order of increasing strength. In that order, acquire is below release in that order.

This parameter set doesn't make a ton of sense, it's true -- maybe I was crazy for trying it. Looking at how compare_swap_impl is written, it doesn't seem like it would be trivial to add support for failure_mo to really be handled separately.

Maybe the right answer is just to change the RL_VERIFY(false) to an RL_ASSERT so that unsupported memory order pairs always report an error.

[Dmitry Vyukov]

If it's going to be supported by the next C++ standard, then I guess
we can just relax the constraints.

On Mon, Dec 19, 2016 at 5:15 PM, Alex Khripin <akhr...@alum.mit.edu> wrote:
> The only suggestive evidence I have is -- GCC allows release + acquire, but
> produces an error on relaxed + acquire
>
> So, it does have a strength check, and release + acquire does pass it.
>
> Another data point is that the std::memory_order enum is written starting at
> relaxed going up through seq_cst -- so it looks sort of like it's in order
> of increasing strength. In that order, acquire is below release in that
> order.
>
> This parameter set doesn't make a ton of sense, it's true -- maybe I was
> crazy for trying it. Looking at how compare_swap_impl is written, it doesn't
> seem like it would be trivial to add support for failure_mo to really be
> handled separately.

What do you mean?
compare_swap_impl accepts callback for success memory order (impl) and
for failure memory order (failure_impl).
It seems to be just a matter of removing the assert and adding new
cases to the switches.

Do you mind to send a pull request to:
https://github.com/dvyukov/relacy
?

> --
> You received this message because you are subscribed to the Google Groups
> "Relacy Race Detector" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to relacy+un...@googlegroups.com.
> To post to this group, send email to rel...@googlegroups.com.
> Visit this group at https://groups.google.com/group/relacy.
> For more options, visit https://groups.google.com/d/optout.

[Martin Krošlák]

Hi,

I could be wrong, since I'm not really a standards person, but here is how I understand orderings (ignoring seq_cst) and I have not seen anything against it yet: acquire is just tied to load operations, while release only deals with stores, meaning for RMW operations these two memory orderings are orthogonal. In CAS, success case is treated as RMW, thus valid options are acquire, release, acq_rel and relaxed. Failure case, on the other hand, is treated as just a load operation, thus only acquire and relaxed are allowed. When using release for success case, you're saying load part has relaxed memory order while store part has release memory order. Thus it should be an error to specify release for success and acquire for failure, as you're using stronger ordering on failure (acquire vs. relaxed).

Also, the documentation seems to support that: http://en.cppreference.com/w/c/atomic/atomic_compare_exchange