[memory-model-design] (partial) recap

Adve, Sarita V sadve at illinois.edu
Mon Jun 11 20:36:01 EDT 2018


I have been traveling and just catching up, so my comments on several messages together -

(1) Doug's summary below:

Could we please add DRFrlx as a potential solution in the summary?

For the use cases (patterns) DRFrlx identifies, it addresses all of the issues - no OOTA, all optimizations allowed. I don’t believe we have yet identified a known interesting use case of memory-order-relaxed that DRFrlx does not cover – please correct me if I missed some. In any case, the approach is extensible - we can add new patterns in the future.

For cases where relaxed is used illegally in C++ (e.g., there is a quantum or other race) – the mindset should be the same as that for a data race in C++; i.e., undefined behavior. But also see below in the “For Java” paragraph.

For cases where relaxed is used legally but strange things seem to occur – e.g., for uses of quantum in things like Hans’ heck froze over example – see below in the Hans section #2.

For Java: analogous to the above except for plain accesses and relaxed races.  For these cases, there seems to be (reluctant) acceptance that type safety and memory safety is sufficient. See separate section #3 on these below.

(2) Hans’ concerns about “heck froze over” example (for C++):

Hans has made eloquent arguments that the “heck froze over” example should not be allowed even for C++. However, I’d like to step back a bit.

Recall we moved to a mindset where we accepted that data races are evil – it took a while to get there, but we are firmly there. With data races (even if it is an inadvertent bug), we have given up trying to be reasonable. (Nobody likes this, but we are well beyond that.)

Most of us (I believe Hans included) also moved to a mindset where we believed that non-SC atomics (specifically, relaxed atomics) are first cousins of evil - so while for pragmatic reasons, we allowed their use, we also understood that they needed to be used ultra-carefully. I believe Hans is on board with this philosophy - or at least he was until some point ☺

I believe that once we buy the above, it frees us up from thinking that every possible legal use of relaxed atomics needs reasonable semantics. I agree that we need formal semantics, but the nature of this first cousin of evil is that you (programmer) have to either be super disciplined in the use of relaxed atomics or be willing to deal with crazy stuff (otherwise don’t use it). We should go as far as possible in identifying the discipline that enables less crazy reasoning, but no further.

I believe DRFrlx strikes the compromise. It goes pretty far by formalizing the discipline (patterns) where you don’t need to think about crazy stuff. Now if you (programmer) want to play fast and lose beyond that, why should we take pains to make your life any simpler?

In summary, I sympathize with Hans’ concerns, but if the programmer writes crazy code like heck froze over, then they have to reason about the possibility of quantum accesses making calls to random etc. This does not seem like a problem to me (recall that if this were a data race, it wouldn’t be a problem for anyone with C++ – so a bad labeling of quantum accesses is just like a data race).

(3) Java: plain accesses and illegal relaxed atomics races (a la DRFrlx):

It is a huge breakthrough that we are willing to give up OOTA etc. in Java for what would be illegal programs in C++. When we started the JMM effort in 1999, type safety and memory safety were the first two requirements for data (plain) accesses and we discussed them for a while. I think these are so much easier, but need discussion of a different sort. Here’s an attempt at starting that discussion:

We can easily give the following guarantee: a single thread’s execution should be consistent with the single thread semantics of the language, given the value returned by a shared memory read. This may sound vague, but really shouldn’t be – it depends entirely on single thread semantics which have nothing to do with the memory model. This is already better than “catch fire” semantics.

Next we can require that a read returns the value of some write to the same address.

Now can someone give example codes that violate type safety and memory safety with the above guarantees in place. That would be a starting point to figure out what is the role of the memory model in ensuring type and memory safety. My claim is that these attributes are much broader than what the memory model can deliver, and we need to be clear about this separation before we start digging deeper. (In my view, what happened with the JMM was that nobody knew what security meant, and over-assigned the role of the memory model for delivering security, which led to failure. We need to avoid a similar rabbit hole for type/memory safety.)

(4) Doug’s, Dmitry’s, and Paul’s examples:

Doug, Dmitry, and Paul in various ways have also argued for a DRFrlx approach (I know, I know, when I have a hammer …). For example, the idempotent example of Doug is exactly the kind of pattern that DRFrlx identifies as safe with great semantics and optimizations – at first glance, it seems to be a subset of the commutative pattern. When we did the DRFrlx paper, we went through Dmitry’s list of benign races - thanks Dmitry, although it was much shorter then ☺ - and had a reaction similar to Dmitry’s. That is, we can’t check everything one by one – we need to glean and formalize the common patterns that tools can hopefully check (it is how DRFrlx came about).

I have said this many times, but once again – I don’t believe DRFrlx is elegant or complete or perfect or what I would choose if I had to reinvent the world – far from it - all I am saying is that it seems to deliver for the moment… (along with some small add ons for illegal codes for type safety and memory safety for Java).

Any thoughts?

Thanks!

Sarita




> -----Original Message-----
> From: memory-model-design <memory-model-design-bounces at cs.oswego.edu> On
> Behalf Of Doug Lea
> Sent: Tuesday, May 29, 2018 6:58 AM
> To: memory-model-design at cs.oswego.edu
> Subject: [memory-model-design] (partial) recap
>
>
> Here's a probably-biased summary of (some) discussions:
>
> 1. We have more examples of anomalies preventable if C++
> memory_order_relaxed and Java9+ Opaque mode require acyclic(po U rf).
>
> 2. We have more empirical evidence that the average performance impact of
> requiring this is in the 1% range, although still high enough to be a
> concern in particular cases, possibly including those in which Linux uses
> READ/WRITE_ONCE but would like to see covered by relaxed mode.
>
> 3. We seem to have a majority of people agreeing that acyclic(po U rf) is
> a good policy for C++-relaxed and Java-opaque, only if there is also some
> sub-relaxed mode available. In Java, this must be "plain" mode.
> Possibly also in C++, but no one has made a detailed proposal.
>
> 4. For Java plain mode, no one has disagreed about guaranteeing only
> global invariants about type and memory safety that are always preserved
> in the presences of races (even in "thin air" cases). Which ought to be
> easier than addressing OOTA issues, but is not yet fleshed out.
>
> -Doug
>
> _______________________________________________
> memory-model-design mailing list
> memory-model-design at cs.oswego.edu<mailto:memory-model-design at cs.oswego.edu>
> http://altair.cs.oswego.edu/mailman/listinfo/memory-model-design

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://altair.cs.oswego.edu/pipermail/memory-model-design/attachments/20180612/9df94189/attachment-0001.html>


More information about the memory-model-design mailing list