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

Alan Jeffrey ajeffrey at bell-labs.com
Fri Oct 3 23:25:19 UTC 2014


Good point. I think this is fixable by changing rf so that a read can rf 
another read with the same label, and then only require read-enablement 
on reads which rf a write. But this is getting a bit hairy...

This is quite a weird test case, but it's difficult to argue with the 
optimization that causes it:

   r1 = x; r2 = x; P  -->  r1 = x; r2 = r1; P

A.

On 10/03/2014 03:57 PM, Brian Demsky 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