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: <Zedd18wiAkK68Lzr@andrea>
Date: Tue, 5 Mar 2024 19:00:55 +0100
From: Andrea Parri <parri.andrea@...il.com>
To: Kenneth-Lee-2012@...mail.com
Cc: linux-kernel@...r.kernel.org, stern@...land.harvard.edu,
	paulmck@...nel.org
Subject: Re: Question about PB rule of LKMM

(Expanding Cc:,)

> In the LKMM document, it said the pb link:
> 
>    E ->coe W ->cumul-fence* X ->rfe? Y ->strong-fence Z ->hb* F
> 
> can make sure E execute before F. But the cat file define pb as follow:
> 
>   let pb = prop ; strong-fence ; hb* ; [Marked]
>   acyclic pb as propagation
> 
> So the acyclic rule is only on pb relationshit itself. So it won't
> forbid F -rfe-> E, will it? It only forgit F -pb-> E. So how can
> propagation rule ensure E execute before F?

With regard to your first question, the propagation rule does indeed forbid
F ->rfe E.  To see why, suppose that F ->rfe E (in particular, E is a load
and the first link in your sequence is fre instead of coe).  Then

   E ->fre W ->cumul-fence* X ->rfe? Y ->strong-fence Z ->hb* F ->rfe E.

Since any rfe-link is an hb-link (by definition of the hb-relation), the
previous expression can be written as follows:

   E ->fre W ->cumul-fence* X ->rfe? Y ->strong-fence Z ->hb* F ->hb E,

that is, given that hb* is the reflexive transitive closure of hb,

   E ->fre W ->cumul-fence* X ->rfe? Y ->strong-fence Z ->hb* E,

contradicting the fact that pb is acyclic.  An argument similar to the one
reported above can show that the propagation rule forbids F ->hb E.

To address the second question, I'd start by first remarking that the CAT
file doesn't define an "execute-before" relation currently.  This file does
however include the following comment:

(*
 * The happens-before, propagation, and rcu constraints are all
 * expressions of temporal ordering.  They could be replaced by
 * a single constraint on an "executes-before" relation, xb:
 *
 * let xb = hb | pb | rb
 * acyclic xb as executes-before
 *)

In this sense, the propagation rule (like other "acyclicity"-constraints of
the LKMM) expresses "temporal ordering", and any pb-link is (by definition)
an "execute-before"-link.  The file explanation.txt can provide additional
context/information, based on the (informal) operational model described in
that file, about this matter.

Notice that, as examples in tools/memory-model/litmus-tests/ can illustrate,
none of the three components of the xb-relation is redundant.  Specifically,
there do exist pb-links/cycles which are not hb-link/cycles (and viceversa).

Maintaining three distinct/separate constraints (happens-before, propagation,
and rcu) instead of a single "executes-before" constraint, although formally
unnecessary, highlights the modularity and eases the debugging of the LKMM.