Re: Question about PB rule of LKMM

[Andrea Parri <parri.andrea@gmail.com>]

> In the "THE HAPPENS-BEFORE RELATION: hb" section of explanation.txt,
> it uses the following example to explain the prop relation:
> 
> 	P0()
> 	{
> 		int r1;
> 
> 		WRITE_ONCE(x, 1);
> 		r1 = READ_ONCE(x);
> 	}
> 
> 	P1()
> 	{
> 		WRITE_ONCE(x, 8);
> 	}
> 
> if r1 = 8, we can deduce P0:Wx1 ->coe P1:Wx8 ->rfe P0:Rx, this can be
> explained with the operational model. But according to the definition of
> prop,
> 
>   let prop = [Marked] ; (overwrite & ext)? ; cumul-fence* ; [Marked] ; rfe? ; [Marked]
> 
> The link should contain a cumul-fence, which doesn't exist in the
> example.

Remark that, in the CAT language, the identity relation ({(e, e) : each event e})
is a subset of R* (the _reflexive_-transitive closure of R) for any relation R.

The link at stake, (P0:Wx1, P0:Rx), is the result of the following composition:

  [Marked]         ; (overwrite & ext)? ; cumul-fence*     ; [Marked]          ; rfe?            ; [Marked]
  (P0:Wx1, P0:Wx1)   (P0:Wx1, P1:Wx8)     (P1:Wx8, P1:Wx8)   (P1:Wx8, P1:Wx8))   (P1:Wx8, P0:Rx)   (P0:Rx, P0:Rx)

  Andrea