Axiomatic validation of memory barriers and atomic instructions [LWN.net]

Axiomatic validation of memory barriers and atomic instructions

Posted Aug 24, 2014 11:47 UTC (Sun) by meyert (subscriber, #32097)
Parent article: Axiomatic validation of memory barriers and atomic instructions

Why can R5 be 0 for P2 and P3 in the PPC IRIW litmus test? Both CPUs executed a sync, so ŵhy can R5 be 0 as the 15 states in the herd output suggests? Doesn't make the sync operation make these reads dependent to the writes?

So the only assertion to make from this test seems to be that "P2 and P3 doesn't see the two stores from P0 and P1 happening in different orders." How can this assertion be useful at all? Say I want to make a decision based on R5 in P2 and P3, to only execute some code when P0 or P1 did set the value to 1?

to post comments

Axiomatic validation of memory barriers and atomic instructions

Posted Aug 25, 2014 7:50 UTC (Mon) by jzbiciak (guest, #5246) [Link] (2 responses)

Including the IRIW litmus test here for convenience:

 1 PPC IRIW.litmus
 2 ""
 3 (* Traditional IRIW. *)
 4 {
 5 0:r1=1; 0:r2=x;
 6 1:r1=1;         1:r4=y;
 7         2:r2=x; 2:r4=y;
 8         3:r2=x; 3:r4=y;
 9 }
10  P0           | P1           | P2                 | P3                 ;
11  stw r1,0(r2) | stw r1,0(r4) | lwz r3,0(r2)       | lwz r3,0(r4)       ;
12               |              | sync               | sync               ;
13               |              | lwz r5,0(r4)       | lwz r5,0(r2)       ;
14 
15 exists
16 (2:r3=1 /\ 2:r5=0 /\ 3:r3=1 /\ 3:r5=0)

So, you ask how R5 can be zero. I assume you mean to ask "How can R5 be zero for either processor when that processor's R3 is not zero," correct? The trivial answer to your question otherwise is "P2 and P3 ran before P0 and P1", which I doubt is satisfactory. :-)

Let's focus on the two most interesting states allowed by IRIW:

P2's R3=1 and R5=1, but P3's R3=1 and R5=0
P3's R3=1 and R5=1, but P2's R3=1 and R5=0

In the first case, P2 saw both writes to X and Y, but P3 only saw the write to Y. That is allowed, because P0 and P1 are not ordered with respect to each other. You could reason that P2 read strictly after P0 and P1, but P3 read after P1 but before P0.

In the second case, P3 saw both writes to X and Y, but P2 only saw the write to X. That is also allowed, because P0 and P1 are not ordered with respect to each other. You could reason that P3 read strictly after both P0 and P1, but P2 read after P0 but before P1.

So, then how about the assertion at the end?

The assertion at the end effectively says "If P2 saw X=1 and P3 saw Y=1, then either P2 also sees Y=1 or P3 sees X=1." What sync apparently does (and lwsync does not do) is provide an illusion of a global order for stores. Regardless of whether P0 wrote before P1 or vice versa, it appears that 'sync' ensures that all writes visible before the 'sync' have a consistent ordering with respect to all writes visible after the 'sync'; furthermore, this ordering is the same for all processors issuing a 'sync'.

In this example, the 'sync' on P2 and P3 has the effect of making them agree on whether P0 or P1 happened first. (In contrast, 'lwsync' apparently only locally orders their loads, which does not cause them to agree on which of P0 or P1 happened first.)

How could this assertion be useful? I'm hard pressed to say with certainty off the top of my head; however, I think some primitives such as Lamport's Bakery and certain other synchronization barriers rely on all readers seeing a consistent order of writers for multiple processors joining the primitive.

Axiomatic validation of memory barriers and atomic instructions

Posted Aug 25, 2014 18:10 UTC (Mon) by meyert (subscriber, #32097) [Link] (1 responses)

Thanks for this explanation, I think I got it now...

So the presentation in the litmus test is a bit misleading and has no information of when the given code is executed on each processor/thread. So line 10 does not execute exactly at the same time on each thread!

So, as an example, a correct usage of the sync would be:
Given a data structure that is written/created by only one thread:
One field in this data structure could be used as a indicator if this data structure is valid now, I.e. the creation is finished and reader is allowed to use this information now.

So the writer should write all necessary fields in the structure and do a sync to establishe a global ordering. Then the writer could set the "information is valid" field to true and sync again.

All readers must spin till they see the indicator field set to true. After that they can begin to use the information in the structure.
I'm not sure if the readers need to call sync in this case to establish the same view on the global ordering.

Hope above example isn't that worse :-)

Thanks again for your explanation.

Axiomatic validation of memory barriers and atomic instructions

Posted Aug 25, 2014 18:48 UTC (Mon) by jzbiciak (guest, #5246) [Link]

So the presentation in the litmus test is a bit misleading and has no information of when the given code is executed on each processor/thread. So line 10 does not execute exactly at the same time on each thread!

Precisely. There are four threads, and their relative execution timelines could vary arbitrarily, except for any ordering the architecture imposes on them (say, through sync or other architectural guarantees).

I read up a little more on the PPC sync instruction today, here. The sync instruction is a true full memory barrier, in that for the processor executing sync, all memory accesses in the system are either strictly before the barrier, or strictly after the barrier.

They also appear to speak to the situation in the example directly in the page linked above:

The first form is heavy-weight sync, or commonly just referred to as sync. This form is often needed by adapter device drivers, for ordering system memory accesses made by a driver critical section with accesses made to its I/O adapter. Executing sync ensures that all instructions preceding the sync instruction have completed before the sync instruction completes, and that no subsequent instructions are initiated until after the sync instruction completes. This does not mean that the previous storage accesses have completed before the sync instruction completes. A store access has not been performed until a subsequent load is guaranteed to see the results of the store. Similarly, a load is performed only when the value to be returned can no longer be altered by a store.

The memory barrier created by the sync instruction provides "cumulative" ordering. This means that after a program executing on processor P0 observes accesses performed by a program executing on processor P1 and then executes a sync instruction, subsequent storage accesses performed by the program executing on processor P0 will be performed with respect to other processors after the accesses it observed to have been performed by the program executing on processor P1. For example, a program executing on processor P3 will not see a sequence of storage accesses that would conflict with the order of the sequence observed and performed by the program executing on processor P0.

So calling it a global order of stores as I did in my previous comment is perhaps inaccurate. Rather, if one processor observes stores ordered in a particular way across a sync, then no other processor will view an ordering of stores inconsistent with that.

The page linked above is an interesting read, if you're curious about PPC memory ordering.