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

[Brian Demsky]

Hi Alan,

How does this work with the JMM causality test case 3?  ( http://www.cs.umd.edu/~pugh/java/memoryModel/CausalityTestCases.html )

My naive reading of the definitions would seem to imply that y=1 would depend the loads r1=x and r2=x and thus forbid the execution.

Brian

BrianOn Oct 3, 2014, at 6:15 AM, Alan Jeffrey <ajeffrey at bell-labs.com> wrote:

> 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.
>