Messages in this thread | | | Date | Wed, 29 Mar 2006 12:51:12 -0800 (PST) | From | Suzanne Wood <> | Subject | Re: [PATCH] Document Linux's memory barriers [try #5] |
| |
Hello and thank you for your response.
> From: "David Howells" Wednesday, March 29, 2006 9:54 AM > > Suzanne Wood wrote: > > > Seems like the subject of "will never happen" is the read from memory for the > > asmt to X, but does that sentence say that? > > "asmt"?
assignment
> I agree that it doesn't make much sense, so how's this instead? > > + 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: > + > + X = *A; > + *A = Y; > + Z = *A; > + > + and assuming no intervention by an external influence, it can be taken that: > + > + (*) X will end up holding the original value of *A, as > + > + (*) the load of X from *A will never happen after the store of Y into *A, and > + thus > + > + (*) X will never be given instead the value that was assigned from Y to *A; > + and > + > + (*) Z will always be given the value in *A that was assigned there from Y, as > + > + (*) the load of Z from *A will never happen before the store, and thus > + > + (*) Z will never be given instead the value that was in *A initially. > + > + (This ignores the fact that the value initially in *A may appear to be the same > + as the value assigned to *A from Y). > > I'm not sure I want to split the points up that way, but it does make them > clearer. I'm not sure that method of linking them works, since it looks like > a bunch of incomplete statements. > > Really, this should be described mathematically, if at all.
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.
> > It seems to require more effort than necessary to understand in regard to > > all that is presented in this document. > > Are you referring to my attempt to define a self-consistent CPU? Or to the > subject in general?
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. > If the former, you may be right. I'll look at compressing the whole thing > down to a single paragraph. > > David
Thanks again. Suzanne - To unsubscribe from this list: send the line "unsubscribe linux-kernel" in the body of a message to majordomo@vger.kernel.org More majordomo info at http://vger.kernel.org/majordomo-info.html Please read the FAQ at http://www.tux.org/lkml/
| |