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

[Hans Boehm]

I'd like to have more of an intuition for how this differs (aside from the
difference in formalism) from the current Java memory model.  I'd really
like to understand if and how we're solving the original problems.

What happens in Alan's model with Sevcik and Aspinall's examples, for
example

(everything initially zero)

Thread 1:
y = x;

Thread 2:
r2 = y; x=(r2==1)?y:1;

In practice, as Jaroslav points out (
http://www.dagstuhl.de/mat/Files/11/11011/11011.SevcikJaroslav.Slides.pdf)
this can currently result in r2 = x = y = 1, by eliminating the second read
of y in thread 2, and noting that the right side is always 1.

Hans

On Fri, Oct 3, 2014 at 1:57 PM, Brian Demsky <bdemsky at uci.edu> wrote:

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