Received-SPF: pass (google.com: domain of linux-kernel+bounces-97609-linux.lists.archive=gmail.com@vger.kernel.org designates 147.75.80.249 as permitted sender) client-ip=147.75.80.249;
Date: Fri, 8 Mar 2024 22:38:09 +0100
From: Andrea Parri <parri.andrea@gmail.com>
To: Kenneth-Lee-2012@foxmail.com
Cc: Alan Stern <stern@rowland.harvard.edu>, linux-kernel@vger.kernel.org,
	paulmck@kernel.org
Subject: Re: Question about PB rule of LKMM
Message-ID: <ZeuFQdk/zcjkILbC@andrea>
References: <tencent_744E0AF832049C200F96FD6582D5114D7F0A@qq.com>
 <ZeipiSVLR01jmM6b@andrea>
 <e05fa6a9-c810-46cb-b033-b91ae7a5c382@rowland.harvard.edu>
 <ZejC+lutRuwXQrMz@andrea>
 <Zenip+8BDM3p+MUh@andrea>
 <eb8f2a21-d388-424d-8504-ccd7bdb53a93@rowland.harvard.edu>
 <ZeoFBkB1BeTdEQsn@andrea>
 <bde188b0-1c5b-4b3b-94de-395a52fc37ce@rowland.harvard.edu>
 <ZeoQvj3l6moF9KdQ@andrea>
 <tencent_3FCF3AA5E98BC9395F98803764A6B2F7CC07@qq.com>
Precedence: bulk
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <tencent_3FCF3AA5E98BC9395F98803764A6B2F7CC07@qq.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