[jmm-dev] Acyclicity of rf and dependent program order
Alan Jeffrey
ajeffrey at bell-labs.com
Fri Oct 3 13:15:48 UTC 2014
Hi all,
Here are some half-baked ideas, this time about acyclicity of rf and
dependent program order.
The idea is that requiring (rf \cup po) to be acyclic is too strong.
Really what is wanted is a notion of "dependent program order" (dpo)
such that we require (rf \cup dpo) to be acyclic.
What follows is an attempt to define dpo. I'm ignoring synchronization
actions for now.
Reminder:
- A labelled event structure with alphabet Sigma is a tuple (E,<=,#,l)
where E is a set of events, <= is a partial order on E, # is a binary
relation on E, and l is a function from E to Sigma such that [...]
- Define d~e in a labelled event structure to be the "minimal conflict"
relation: d#e and for any (d => b # c <= e) we have (d = b # c = e). In
examples, d~e when they are events from "the same" read, with different
values being read.
- A memory model alphabet is (Sigma,RWC,RWJ) is a set Sigma with binary
relations RWJ \subseteq RWC on Sigma such that [...]
- A pre-configuration C is a <=-downclosed subset of E.
Write (d \simeq e) whenever (d ~ e) or (d = e). In examples, d \simeq e
when they are events from "the same" read.
Let a pre-configuration C be read-enabled whenever, for any d,e in C, if
(d,e) in RWC then there exists c \simeq e where (d,c) in RWJ. In
examples, this is saying that if (R x=0) and (W x=1) are in C, then
there must be (R x=1) in C from "the same" read.
In a pre-configuration C, e in C is guaranteed to perform a whenever,
for any e<=d in C there exists c in C such that l(c)=a and either
e<=c<=d or e<=d<=c.
In a pre-configuration C, d <= e is independent whenever for any c in C
if (c \simeq d) then c is guaranteed to perform l(e). Let ipo be the
independent program order, and dpo be the dependent program order.
So now, the proposed requirement is to find a read-enabled
pre-configuration in which (rf \cup dpo) is acyclic.
Note this handles the canonical cases, for example the TAR pit has a
cycle in (rf cup dpo) given by:
(R x=42) --dpo--> (W y=42) --rf--> (R y=42) --dpo--> (W x=42) --rf-->
whereas the version where the second thread is (r=y; x=42) has no cycle
since:
(R x=42) --dpo--> (W y=42) --rf--> (R y=42) --ipo--> (W x=42) --rf-->
This even deals with range analysis, for example if we make the second
thread (r=y; if (r < 43) { x=42; } else { x=100; }) then we get the same
pre-configuration, with no cycle:
(R x=42) --dpo--> (W y=42) --rf--> (R y=42) --ipo--> (W x=42) --rf-->
This definition seems to be in line with the thinking at the Cambridge
workshop about trying to define semantic dependency. I'm sure there is
some horror (e.g. in proving the DRF theorem, or scaling up to handle
synchronization actions).
Thoughts?
Alan.
More information about the jmm-dev
mailing list