[jmm-dev] Acyclicity of rf and dependent program order

[Alan Jeffrey]

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.