[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