[jmm-dev] Sequential Consistency

[Alan Jeffrey]

The LTL formulation of relaxed consistency does validate IRIW. The 
interesting trace is:

   (1: W x=1) (2: W y=1) (3: Rx=1) (3: Ry=0) (4: R y=1) (4: R x=0)

The reason why this trace is relaxed consistent is that each action can 
be justified by a different permutation of the actions before it. In 
particular, the action (4: x=0) can be justified by the permutation:

   (2: W y=1) (3: Rx=1) (3: Ry=0) (4: R y=1) (4: R x=0) (1: W x=1)

and the action (3: Ry=0) can be justified by the permutation:

   (1: W x=1) (3: Rx=1) (3: Ry=0) (2: W y=1)

So I there are models based on interleaved actions and reorderings that 
validate IRIW, but crucially different reorderings are used to justify 
different read actions.

I'm not going to try to claim that LTL with permutations is as easy to 
reason about as SC though!

A.

On 02/24/2014 12:52 AM, Hans Boehm wrote:
> I think it's that last comment here that needs to be emphasized: We don't
> really have a viable candidate property to replace SC, that's anywhere near
> as easy to reason about and provides significant performance advantages.
> Several people, including Doug, looked hard for such things when we were
> talking about  C++.
>
> As far as I can tell, everyone intuitively wants to reason about thread
> behavior in terms of interleaving thread actions, possibly after allowing
> some reorderings within threads.  IRIW seems inherently incompatible with
> that, which might be a partial explanation of why it's difficult to reason
> directly with consistency properties that allow it.
>
> Hans
>
>
> On Sun, Feb 23, 2014 at 5:59 AM, Doug Lea <dl at cs.oswego.edu> wrote:
>
>> On 02/22/2014 10:59 AM, Doug Lea wrote:
>>
>>> I won't yet try to summarize different positions and rationales,
>>> but for now just invite further discussion.
>>>
>>
>> That was too cowardly. Here's a shot at summarizing some of the
>> historical context.
>>
>>   PS: As a reminder, here's IRIW. Given global x, y:
>>>     Thread 1: x = 1;
>>>     Thread 2: y = 1;
>>>     Thread 3: r1 = x; r2 = y;  // sees r1 == 1, r2 == 0
>>>     Thread 4: r3 = y; r4 = x;  // sees r3 == 1, r4 == 0
>>>
>>
>> (This outcome is not allowed by SC.)
>>
>> The IRIW example is a fun one in part because it is not especially
>> intuitive.  Some people do not at first think that it is a result
>> forced by SC. I occasionally present this in courses, and most
>> students' first reaction is that you should use a common lock in all
>> threads if you want to ensure agreement about order of x and y
>> here. The fact that you don't need to strikes some (but by no means
>> all) people as a magical/spooky property of SC.
>>
>> This example (and variants of it) was also among those first driving
>> research into more efficient distributed multicast protocols in the
>> late 80's/early 90's (when I first encountered consistency policies
>> and protocols).  Maintaining this property of SC is much more
>> expensive in a distributed setting than other consistency policies
>> that are sufficient to implement most distributed algorithms.  SC
>> normally requires blocking on O(#hosts) round-trips per message in the
>> absence of failure, and heavy (and fallible) failure-recovery
>> mechanics. Other policies, including "causal broadcast" (guaranteeing
>> only transitivity of read-write happens-before in producer-consumer
>> chains) usually don't need to wait out all the round-trips (but still
>> require buffering).  While the situation is a little better for
>> multiprocessor/multicore designers, it is not surprising that they
>> occasionally propose (as did AMD and then Intel five years or so ago)
>> schemes that are by default weaker (but still with full-SC modes).
>>
>> Arguments for not giving in to the whinings of implementors include
>> those claiming that uniform SC requirements enable better tools,
>> simpler proofs of correctness, more understandable models, and the
>> reduction of counterintuitive orderings.  And that no single "natural"
>> property has emerged to replace it, despite a fair amount of trying.
>>
>> -Doug
>>
>>