linux-kernel - Re: Question about PB rule of LKMM

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]

Message-ID: <ZeuFQdk/zcjkILbC@andrea>
Date: Fri, 8 Mar 2024 22:38:09 +0100
From: Andrea Parri <parri.andrea@...il.com>
To: Kenneth-Lee-2012@...mail.com
Cc: Alan Stern <stern@...land.harvard.edu>, linux-kernel@...r.kernel.org,
	paulmck@...nel.org
Subject: Re: Question about PB rule of LKMM

> 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