PPC
From X10Wiki
Memory Model Table of Contents
Contents |
PPCl
Formulation of 02/18/07.
PPCl is Sequentially Consistent
Memory Model Background Definitions
In this model we make the Completion Assumption:
- When a load l being executed by a processor p=p(l) completes, it has been performed with respect to all processors.
This assumption introduces a partial order on loads. Consider two loads k and l, with processor p=p(k) and q=p(l). Suppose the execution of k is completed on p, and then l is performed on p. This permits us to conclude that k is performed on q before l. (l completes on q after it is performed on all processors, including p, but it is performed on p after k completes, and k completes after it has performed on all processors, including q. Therefore, k is performed on q before l completes on q.)
See Completeness Assumption Formulations for different variations. The definition here is the weakest possible definition.
The model has the following elements:
- E -- set of elements
- <w -- a total order over S(a), for all a in A
- <p -- a total order over E, for each p in P.
We define V(p), the set of events see by processor p, as
- V(p) = {e | for some e' in E: e <p e' or e' <p e}
Note that E(p) is contained in V(p) if E(p) has at least two elements. We require that V(p) be contained in E(p) u L u S. (i.e. V(p) cannot contain fences executed by processors other than p).
It will be useful in what follows to think of events e as being local to the processor p(e), and remote or foreign to processors different from p(e).
The tuple (E, <w, <1,..., <n) is a valid execution if the conditions (C), (V1), (V2), (F1), (F2) and (C) are satisfied.
Coherence: The order in which writes are visible at any processor is consistent with the global order <w. Formally:
- (C) for any processor p, for any address a in A, stores s,s' in S(a) s<p s' implies s <w s'.
Value flow: Let us define for every store s in S(a), loads(s), the set of loads which read from s by:
- loads(s) = { l in L(a(s)) | s <l l, forall s' in S(l): s' <p(l) l implies s' <p(l) s or s'=s }
Each load gets the value of the latest preceding store to the same address that the processor observes, or the initial value if there is no such store. Further, before a load is performed at a processor it must be the case that the store whose value is being returned has been performed at that processor. Formally, we require for all processors p:
- (V1) for all loads l in L(p): v(l) = i(a(l)) or for some s in S(l): s <p l
- (V2) for all loads l in L(p), for all s in S(a(l)) intersect V(p): (for some t in S(l) s <p t <p l) or v(l)=v(s) or l <p s
Fences: Fences order memory accesses. For any fence f, and processor p=p(f) both the following conditions must hold:
- (F1) for all d in E, e in E(p): d <p f <p e implies for all q in P: d <q e
- (F2) for all d,e in E, s in S(p), l in loads(s): d <p f <p s, (l <e e or l=e) implies for all q in P: d <q e
(The formulatoin of F2 has been strengthened to include the event l in the cumulative B set.)
Completeness Assumption:
- (C) for all loads k, l: k <k l implies k <l l
- (S) for load l and store s in S(l): s <l l implies s <s l
PPCl properties
PPCl validates the Completeness Assumption, Performs Assumption but does not validate the Monotonicity Assumption.
PPCw
In this model the requirement "load must be performed wrt processor q" is interpreted as: the store whose value is returned by the load must be performed wrt processor q. It is not required that the load must be performed wrt all other processors before the load is completed (and returns a value).
The only difference with PPCl is that (CA) is dropped.
PPCw properties
[#PPC|PPCw]] validates the Completeness Assumption, Performs Assumption but does not validate the Monotonicity Assumption. [#PPC|PPCw]] is too weak to establish SC.
PPCs
In this model, the requirement load l must be performed wrt processor q is interpreted as load l must return the same value at this point as a load performed by q.
This is formalized by requiring that (V1) and (V2) in PPCw apply to all loads l in V(p) (and not just loads l in L(p)).
This model is not validated by PPC Architecture. It is included here only as a theoretical exercise.
PPCs properties
PPCl validates the Completeness Assumption, Performs Assumption and the Monotonicity Assumption.
