[jmm-dev] Acyclicity of rf and dependent program order
Alan Jeffrey
ajeffrey at bell-labs.com
Fri Oct 3 23:35:29 UTC 2014
I think this is essentially the same example. With the definition below
the write (W x=1) is dependent on the second read (R y=1), but if you
allow reads to justify reads then they're independent.
A.
On 10/03/2014 05:18 PM, Hans Boehm wrote:
> 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
> <mailto: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 <mailto: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.
> >
>
>
More information about the jmm-dev
mailing list