[jmm-dev] Jmm revision status

Jeffrey, Alan S A (Alan) alan.jeffrey at alcatel-lucent.com
Fri Jul 18 12:21:33 UTC 2014


>From our side...

Sorry about the radio silence. It's been caused by the unexpected difficulty of getting the DRF proof to go through for event structures. The solution (as with all these things) is to make some "small" changes to the definitions until the theorem is true, but I didn't want to pester the list with small deltas.

The good news is that I have a simple(ish) definition that appears to validate DRF, and also a candidate definition of refinement that a) is compositional, and b) validates a bunch of examples (some variable reorderings, thread inlining and roach motel).

More details when everything gets nailed down, but the basic idea is still the same...

A prime event structure over Sigma is a triple (E,<=,#,l) where:

* (E,<=) is a partial order (think program order)
* (E,#) is an irreflexive, down-closed relation (think conflicts caused by reads on variables, the event R(x,0) is in conflict with the event R(x,1))
* l: E -> Sigma (the labelling function on events)

A memory model laphabet (Sigma,RWJ,RWC,Sync) is a set Sigma with three binary relations:

* RWC (read-write conflict, e.g. W(x,1) in RWC(R(x,0)))
* RWJ (read-write justification, e.g. W(x,1) in RWJ(R(x,1)))
* Sync (synchronization, e.g. W(x,1) in Sync(R(x,0)) when x is volatile)

A memory model an even structure is a prime event structure over a memory model alphabet such that (er, precise conditions will go here, hopefully nothing too surprising).

A (totally ordered) configuration of an event structure is a sequence of events which is <=-down-closed, conflict-free, and repeat-free. A pre-configuration drops the conflict-free requirement.

In a sequence :

* "trace order" (s |= d <=to e) is whenever d occurs before e in s
* "program order" (s |= d <=po e) is whenever (s |= d <=to e) and d <= e
* "synchronization order" (s |= d <=so e) is whenever (s |= d <=to e) and d in Sync(e)
* "happens before order" (s |= d <=hb e) is the transitive closure of <=po and <=so
* "separated by synchronization order" (s |= d <=sso e) is <=hb <=so <=hb

A confliguration s is sequentially consistent whenever there is a function j:E->E (think "justifier") such that for any e in s other than the initial action:

* j(e) in RWJ(e)
* s |= j(e) <=to e 
* there is no d in WWC(j(e)) and in RWC(e) such that s |= j(e) <= d <= e

A confliguration s is relaxed consistent whenever it is included in a pre-configuration t and there is a function j:E->E such that for any e in s other than the initial action:

* j(e) in RWJ(e)
* s |= j(e) <=to e 
* there is no d in WWC(j(e)) and in RWC(e) such that s |= j(e) <=hb d <=hb e
* if (t |= j(e) <=sso e) and (e in s) then (j(e) in s)
* if (t |= d <=sso j(e)) then (d not in #(e))

I'm in the middle of proving the DRF theorem (that if all SC configurations are DRF then all RC configurations are DRF, and hence SC).

The model is more complex than before (due to <=po not being the same as <=sso) and results in some hairy conditions (the last two requirements of being RC are just to get DRF to fly) but not (I hope) horribly so.

Lots of work remaining, notably finishing DRF, refinement, using refinement to validate optimization, check on examples, etc. etc.

Anyway this is what we've been up to in Chicago!

A.
________________________________________
From: jmm-dev [jmm-dev-bounces at openjdk.java.net] on behalf of Francesco Zappa Nardelli [francesco.zappa_nardelli at inria.fr]
Sent: Friday, July 18, 2014 6:26 AM
To: Viktor Vafeiadis
Cc: jmm-dev at openjdk.java.net
Subject: Re: [jmm-dev] Jmm revision status

Dear all

> An update from our side: I'm attaching a draft version of the paper that Peter mentioned.

It seems that the attachment didn't made to the list.  Anyway, the draft is available from:

  http://www.di.ens.fr/~zappa/readings/c11comp.pdf

Best
-francesco


More information about the jmm-dev mailing list