Re: Uses for memory barriers

On Fri, Oct 20, 2006 at 12:54:52PM -0400, Alan Stern wrote:
On Thu, 19 Oct 2006, Paul E. McKenney wrote:

Your notion of control-dependency barriers makes sense in an intuitive
sense. Does Linux rely on it, other than for MMIO accesses?

I'm pretty sure that somewhere I saw some code which looked like it needed
a memory barrier but didn't have one. I decided it was okay because of
exactly this sort of control dependency. No way to know if it was
deliberate or merely an oversight. Don't ask me where that was; I can't
remember.

There are a number of cases where this sort of code structure is OK,
even without assuming that control dependencies have any memory-ordering
consequences. But they do have to be taken case by case...

Okay, let's change the notation. I don't like <v very much. Let's not
worry about potential confusion with implication signs, and use

1:st(A) -> 2:st(A)

Would "=>" work, or does that conflict with something else?

It's okay with me.

And the number before the colon is the CPU #, right?

No, it's an instance label (kind of like a line number). As we've been
doing before. The CPU number is still a subscript.

When I started actually doing formulas, the use of ":" conflicted with
the logic-expression operator ("for every x there exists y and z such
that...", which turns into upside-down-A x backwards-E y,z colon ...,
at least if I am remembering all this correctly).

So how about having the line number be a second subscript following the
CPU number?

to indicate that 1:st occurs earlier than 2:st in the global ordering of
all stores to A. And let's use

3:st(B) -> 4:ld(B)

to mean that 4:ld returned the value either of 3:st or of some other store
to B occuring later in the global ordering of all such stores.

OK... Though expressing your English description formally is a bit messy,
it does capture a very useful idiom.

Lastly, let's use

5:ac(A) +> 6:ac(B)

to indicate either that the two accesses are separated by a memory barrier
or that 5:ac is a load and 6:ac is a dependent store (all occurring on the
same CPU).

So the number preceding the colon is the value being loaded or stored?

No, that value goes inside the parentheses.

Got it...

Either way, the symbols seem reasonable. In a PDF, I would probably
set a symbol indicating the type of flow over a hollow arrow or something.


Hmmm. Then what about "DMA coherent" vs. "DMA consistent"?

No idea. Having worked with systems where DMA did not play particularly
nicely with the cache-coherence protocol, they both sound like good things,
though. ;-)

As near as I can tell by looking around, they are synonyms or nearly so.

I once saw someone draw a distinction between them, but I didn't
understand it at the time and now it has faded away.

I do remember some documentation mentioning this, will track it down.

Consider this example:

CPU 0 CPU 1
----- -----
A = 1; B = 2;
mb(); mb();
B = 1; X = A + 1;
...
assert(!(B==2 && X==1));

The assertion cannot fail. But to prove it in our formalism requires
writing st_0(B=1) -> st_1(B=2). In other words, CPU 1's store to B sees
(i.e., overwrites) CPU 0's store to B.

I wrote that the assertion cannot fail, but I'm not so sure any more.
Couldn't there be a system where CPU 1's statements run before any of CPU
0's writes become visible to CPU 1, but nevertheless the caching hardware
decides that CPU 1's write to B "wins"? More on this below...

The memory barriers require that if the caching hardware decides that
CPU 1's B=2 "wins", then X=A+1 must see CPU 0's A=1. Now the assertion
could legally see B==2&&X==0, or B==1&&X={0,1,2}, but it cannot legally
see B==2&&X==1 because that would violate the constraints that the
memory barriers are supposed to be enforcing.

Alternatively, we could use a notation that states that a given load gets
exactly the value from a given store, for example "st ==> ld" as opposed
to "st => ld", where there might be an intervening store.

That's a useful concept.

Especially when defining cache coherence -- need to be able to say that
only stores can change the value, and that any loads between a pair of
stores see the value from the first of the two stores. This can be done
without ==>, but it is more elaborate.

(1) B==2 -> st_1(B=2) ==> ld_0(B==2)

Because there is only one store of 2 into B.

(2) But st_0(B=1) =p> ld_0(B) -> st_0(B=1) => ld_0(B)

Here I use "=p>" to indicate program order, and rely on the
fact that a CPU must see its own accesses in order.

Right.

(3) (1) and (2) imply st_0(B=1) => st_1(B=2) ==> ld_0(B==2)

Yes. st_0(B=1) => ld_0(B) means that the load must return the value
either of the st_0 or of some later store. Since the value returned was
2, we know that the store on CPU 1 occurred later than the store on
CPU 0.

(By "later" I mean at a higher position according to the global ordering
of all stores to B. There doesn't seem to be any good way to express this
without using time-related words.)

One could say "the store on CPU 1 overwrote that of CPU 0", but this
admittedly gets cumbersome if there is a long sequence of stores.

So, yes, we do end up saying something about the order of the
stores, but only indirectly, based on other observations -- in
this case, program order and direct value sequence. In other
words, we can sometimes say things about the order of stores
even though stores are blind.

Which was my original point.

OK. I misunderstood you.

(4) By memory-barrier implication:

(a) st_0(A=1) +> st_0(B=1) &&

(b) st_1(B=2) +> ld_1(A) &&

(c) st_0(B=1) => st_1(B=2)

-> st_0(A=1) => ld_1(A)

(5) Since there is only one store to A: st_0(A=1) ==> ld_1(A==1)

(6) Therefore, X==2 and the assertion cannot fail if B==2. But
if the assertion fails, it must be true that B==2, so the
assertion cannot fail.

Is that more or less what you had in mind?

Yes it was.

But now I wonder... This approach might require too much of memory
barriers. If we have

st(A); mb(); st(B);

does the memory barrier really say anything about CPUs which never see one
or both of those stores? Or does it say only that CPUs which see both
stores will see them in the correct order?

Only that CPUs that see both stores with appropriate use of memory barriers
will see them in the correct order.

The only way to be certain a CPU sees a store is if it does a load which
returns the value of that store. In the absence of such a criterion we
don't know what really happened. For example:

CPU 0 CPU 1 CPU 2
----- ----- -----
A = 1; while (B < 1) ; while (B < 2) ;
mb(); mb(); mb();
B = 1; B = 2; assert(A==1);

I put memory barriers in for CPUs 1 and 2 even though they shouldn't be
necessary. Now look what we have:

st_0(A=1) +> st_0(B=1) ==> ld_1(B) =p>

st_1(B=2) ==> ld_2(B) +> ld_2(A).

From this we can deduce that st_0(B=1) => st_1(B=2). For if not then
st_1(B=2) => st_0(B=1) => ld_1(B) and hence st_1(B) => ld_1(B),
contradicting the requirement that CPU 1 sees it own accesses in order.

But now we can go on to deduce st_0(B=1) => ld_2(B) (not ==>), and hence
st_0(A=1) => ld_2(A). Since there are no other writes to A, we get
st_0(A=1) ==> ld_2(A), meaning that the assertion must hold.

Yep, which it must for locking to work, assuming my approach to transitivity.
If we were using your approach to transitivity, we would have a different
memory-barrier condition that required an atomic operation as the final
link in a chain of changes to a given variable -- and in that case, we
would find that the assertion could fail.

But we know that the assertion may fail on some systems!

To be determined -- the fact that we are threading the single variable B
through all three CPUs potentially makes a difference. Working on the
empirical end. I know the assert() always would succeed on POWER, and
empirical evidence agrees (fine-grained low-access-overhead synchronized
time-base registers make this easier!). I believe that the assert would
also success on Alpha.

The reason being
that CPU 0's stores might propagate slowly to CPU 2 but the paths from
CPU 0 to CPU 1 and from CPU 1 to CPU 2 might be quick. Hence CPU 0's
write to A might not be visible to CPU 2 when the assertion runs, and
CPU 0's write to B might never be visible to CPU 2.

Agreed -- if the assertion really is guaranteed to work, it is because
the cache-coherence protocol is required to explicitly make it be so.
One reason that I am not too pessimistic is that there are some popular
textbook algorithms that cannot work otherwise (e.g., the various locking
algorithms that don't use atomic instructions, possibly also some of the
NBS algorithms).

This wouldn't violate the guarantee made by CPU 0's mb(). The guarantee
wouldn't apply to CPU 2, since CPU 2 never sees the "B = 1".

Again, this depends on the form of the memory-barrier guarantee --
the presence of a "==>" vs. a "=>" is quite important! ;-)

To resolve this we need an additional notion, of a store to some variable
being visible to a subsequent access of that variable. The mere fact that
one store precedes another in the global ordering isn't enough to make it
visible.

How would you straighten this out?

My hope is that the CPUs are guaranteed to act the way that I hope they
do, so that the memory-barrier rule is given by:

st(A) -p> wmb -p> st(B) && ld(B) -p> rmb -p> ld(A) && st(B) => ld(B) ->
st(A) => ld(A)

If so, everything works nicely. In your scenario, the memory-barrier
rule would instead be something like:

st(A) -p> wmb -p> st(B) && ld(B) -p> rmb -p> ld(A) && st(B) ==> ld(B) ->
st(A) => ld(A)
st_0(A) -p> wmb -p> st(B) && ld_1(B) -p> rmb -p> ld(A) && st_0(B) => ld_1(B) &&
not-exist i: st_0(B) => st_i(B) => ld_1(B) ->
st(A) => ld(A)
st(A) -p> wmb -p> st(B) && ld(B) -p> rmb -p> ld(A) && st(B) => at(B) ->
st(A) => ld(A)

In other words, either: (1) the st(B) must immediately precede the ld(B), or
(2) there can only be loads between the st(B) and ld(B) (yes, I would have
to add other terms to exclude atomics and so on...), or (3) the access to A
by CPU 1 must be an atomic operation.

Given this set of rules, the assertion could fail. However, if the
"while (B < 2)" were replaced by (or followed by) an atomic operation
on B, as one would have with a lock, then the assertion would always
succeed.

Does this make sense?

Thanx, Paul
-
To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
the body of a message to majordomo@xxxxxxxxxxxxxxx
More majordomo info at http://vger.kernel.org/majordomo-info.html
Please read the FAQ at http://www.tux.org/lkml/

Relevant Pages

  • Re: Uses for memory barriers
    ... trying to present a high-level description of the requirements memory ... barriers must fulfill in order to support usable synchronization. ... Whichever CPU acquires the lock last had better be the one whose value ... So even though both stores are visible to CPU 0, ...
    (Linux-Kernel)
  • Re: Uses for memory barriers
    ... only in the following two cases: for MMIO and for sharing memory ... (Ceci n'est pas un CPU!) ... might disagree on the order in which given loads and stores occurred. ...
    (Linux-Kernel)
  • Re: Uses for memory barriers
    ... the action of memory barriers. ... (Ceci n'est pas un CPU!) ... might disagree on the order in which given loads and stores occurred. ...
    (Linux-Kernel)
  • Re: Uses for memory barriers
    ... The CPU number is still a subscript. ... I wrote that the assertion cannot fail, but I'm not so sure any more. ... memory barriers are supposed to be enforcing. ... stores will see them in the correct order? ...
    (Linux-Kernel)
  • Re: Uses for memory barriers
    ... The CPU number is still a subscript. ... I wrote that the assertion cannot fail, but I'm not so sure any more. ... memory barriers are supposed to be enforcing. ... stores will see them in the correct order? ...
    (Linux-Kernel)