[jmm-dev] DRF theorem for event structures model of relaxed memory

[Alan Jeffrey]

On 03/28/2014 08:07 AM, Doug Lea wrote:
> On 03/26/2014 01:41 PM, Alan Jeffrey wrote:
>> Another update on where we are with modeling relaxed memory...
>
> A couple of questions about decoding it ...

I'm not surprised it's a bit dense, it's a bit of a brain-dump!

>> * An element initialize of Sigma
>> * A subset Sync of Sigma
>
> ("Sync" is not used below? I can guess intent, but it would
> be more comforting to know.)

Indeed, it's not needed in defining the relaxed memory model, it's there 
for use later on when we come to define the semantics of programs. The 
idea is that <= will form a total order on synchronization actions.

>> Define past-time LTL over E* as per usual, in particular (writing <=
>> on strings
>> for prefix order):
>
> Is there a good tutorial reference on the "per usual" techniques?

The wikipedia article 
(http://en.wikipedia.org/wiki/Linear_temporal_logic) is surprisingly 
good. If you're OK reading slides, then Mads Dam's course on temporal 
logic is a good one 
(http://www.csc.kth.se/~mfd/Courses/Temporal_logic/course_description.php). 
For more detail than you probably want, there's Emerson's Handbook of 
Theoretical CS chapter 
(http://www.cs.utexas.edu/users/emerson/Pubs/1990-00.Em.HANDBK-TCS.tl-survey.ps). 
Be warned: most work on LTL is about future-time rather than past-time, 
and focuses on model checking which isn't relevant here.

>>    epsilon in wkprev(phi) always
>>    se in wkprev(phi) whenever s in phi
>
> My reading was that this ("weak previous"?) allows binary relations
> to apply to the first event, by giving it an artificial empty predecessor?
> But I'm not so sure because I can't decode its use in "Relaxed" below.

Indeed, wkprev(phi) means "phi holds in the previous state". LTL is just 
being used to denote sets of strings of events, another way of writing 
wkprev would be:

   wkprev(phi) = { epsilon } union{ se | s in phi}

The reason for the name is that there's a corner case about whether you 
include the empty string or not. There's a matching strong modality, 
which doesn't include epsilon:

   stprev(phi) = { se | s in phi }

I hope this helps!

A.