[jmm-dev] Sequential Consistency

[Paul E. McKenney]

On Sun, Feb 23, 2014 at 01:06:42PM +0400, Aleksey Shipilev wrote:
> On 02/22/2014 07:59 PM, Doug Lea wrote:
> > Other cases may be less clear cut.  For the most famous example: Can a
> > program using non-lock-based techniques (for example, using Java
> > volatile loads/stores) be "correct" if it fails some variant of the IRIW
> > test?  Is IRIW conformance an unnecessary action-at-a-distance
> > by-product of SC, or does it play some intrinsically useful role in
> > assuring correctness?
> 
> IMO, we are on a thin ice here. The absence of counter-examples how
> non-SC behaviors for IRIW-like constructions demolish the correctness at
> larger scale does not mean we wouldn't find the case where it breaks
> badly in future, when the spec solidifies. In other words, absence of
> evidence is not evidence of absence.
> 
> I, for one, would not like to wake up to another
> double-checked-locking-like calamity because we allowed a particular
> sneaky behavior in the name of performance. And yes, being the
> performance guy, I still think strong correctness wins over performance
> ten times over.
> 
> The relaxations are welcome, but only in a few very constrained places,
> where you are able to relatively easy fix/rewrite the bad usages or even
> provide stronger ad-hoc semantics. On other words, the things you allow
> in a library (e.g. Linux RCU) are not the things you want to burn into a
> language spec.

Hmmm...  On the one hand, use of SC is no substitute for carefully
designed APIs that are easy to use.  Some of my ugliest bugs in
my Linux-kernel work would not be helped by SC -- they involved
very conservative fully locked code.

On the other hand, if you are using non-SC primitives, then you had
better have a really carefully designed heavily stress-tested API.
A proof of correctness wouldn't hurt either.  ;-)

> > IRIW is not the only example of a case in which SC imposes conditions
> > that some programmers in some contexts seem not to care about.  But
> > it is most famous because it so clearly impacts the nature and cost of
> > mappings (for various modes of load, store, and CAS) on some existing
> > processors as well as potential mappings on future processors.
> 
> Being the language guy, I think the hardware not being able to provide
> the sane SC primitives should pay up the costs. The hardware which makes
> it relatively easy to implement the non-tricky language memory model
> should be in the sweet spot.

All hardware I know of has a non-trivial penalty for its SC primitives,
so there is a place for non-SC algorithms.

							Thanx, Paul