[lock-free] Re: Relacy CAS release + acquire error?

[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

On Tuesday, December 20, 2016 at 10:25:37 AM UTC+1, Dmitry Vyukov wrote:
>
> 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  > 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 
> ? 
>
>
> > 
> > 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. 
> > 
> > 
> > On Mon, Dec 19, 2016 at 2:28 AM, Dmitry Vyukov  > wrote: 
> >> 
> >> On Mon, Dec 19, 2016 at 4:18 AM, Alex Khripin  > 
> >> 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? 
> > 
> > 
> > -- 
> > 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. 
>

-- 

--- 
You received this message because you are subscribed to the Google Groups 
"Scalable Synchronization Algorithms" group.
To unsubscribe from this group and stop receiving emails from it, send an email 

[lock-free] Re: Relacy CAS release + acquire error?

[Dmitry Vyukov]

On Mon, Dec 19, 2016 at 4:18 AM, Alex Khripin  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?

-- 

--- 
You received this message because you are subscribed to the Google Groups 
"Scalable Synchronization Algorithms" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to lock-free+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/lock-free/CAEeQi3uMEJpFPrVLLW-A9fuMiAyvq7CQJxJ-0_iT4AhsTgh_Zg%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.