Suzanne Wood <[email protected]> wrote:
> Do you mean to formalize preconditions on the value of Y and contents of A
> and consider postconditions after the execution of the three statements of
> the example where the value of X is the prior content of A and A contains and
> Z equals the value of Y.
Something like that, yes.
How about the attached instead? My explanation didn't give a write/write
example, so I've added that in too.
> Sorry to be unclear. I was just asking about the explanation of the
> self-consistent CPU example. The other ideas in the document are more
> difficult, so thought this part might be simplified.
The whole subject is fraught with unclarity:-)
David
However, it is guaranteed that a CPU will be self-consistent: it will see its
_own_ accesses appear to be correctly ordered, without the need for a memory
barrier. For instance with the following code:
U = *A;
*A = V;
*A = W;
X = *A;
*A = Y;
Z = *A;
and assuming no intervention by an external influence, it can be taken that the
final result will appear to be:
U == the original value of *A
X == W
Z == Y
*A == Y
The code above may cause the CPU to generate the full sequence of memory
accesses:
U=LOAD *A, STORE *A=V, STORE *A=W, X=LOAD *A, STORE *A=Y, Z=LOAD *A
But, without intervention, the sequence may have almost any combination of
elements barring the load of *A into U and the store of Y into *A discarded as
the CPU may combine or discard memory accesses as it sees fit, provided _its_
view of the world is consistent. This leads to the following possible other
sequences:
U=LOAD *A, STORE *A=V, STORE *A=W, X=LOAD *A, STORE *A=Y
U=LOAD *A, STORE *A=V, STORE *A=W, STORE *A=Y, Z=LOAD *A
U=LOAD *A, STORE *A=V, STORE *A=W, STORE *A=Y
U=LOAD *A, STORE *A=V, STORE *A=Y, Z=LOAD *A
U=LOAD *A, STORE *A=V, STORE *A=Y
U=LOAD *A, STORE *A=W, X=LOAD *A, STORE *A=Y
U=LOAD *A, STORE *A=W, STORE *A=Y, Z=LOAD *A
U=LOAD *A, STORE *A=W, STORE *A=Y
U=LOAD *A, STORE *A=Y, Z=LOAD *A
U=LOAD *A, STORE *A=Y
Note:
(*) STORE *A=W can only be dispensed with if X=LOAD *A is also dispensed with,
otherwise X would be given the original value of *A or the value assigned
there from V, and not the value assigned there from W.
(*) STORE *A=V would probably be discarded entirely by the CPU - if not the
compiler - as it's effect is overridden by STORE *A=W without anything
seeing it.
(*) STORE *A=Y may be deferred indefinitely until the CPU has some reason to
perform it or discard it.
(*) Even the two 'fixed' operations can be dispensed with if they can be
combined or discarded with respect to the surrounding code.
(*) The compiler may also combine, discard or defer elements of the sequence
-
To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
the body of a message to [email protected]
More majordomo info at http://vger.kernel.org/majordomo-info.html
Please read the FAQ at http://www.tux.org/lkml/
[Index of Archives]
[Kernel Newbies]
[Netfilter]
[Bugtraq]
[Photo]
[Stuff]
[Gimp]
[Yosemite News]
[MIPS Linux]
[ARM Linux]
[Linux Security]
[Linux RAID]
[Video 4 Linux]
[Linux for the blind]
[Linux Resources]
