linux-kernel - Re: [RFC] tools/memory-model: Rule out OOTA

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: <329f1d75-1d4f-42dc-8d28-9674def6f27f@rowland.harvard.edu>
Date: Fri, 17 Jan 2025 14:02:32 -0500
From: Alan Stern <stern@...land.harvard.edu>
To: Jonas Oberhauser <jonas.oberhauser@...weicloud.com>
Cc: paulmck@...nel.org, parri.andrea@...il.com, will@...nel.org,
	peterz@...radead.org, boqun.feng@...il.com, npiggin@...il.com,
	dhowells@...hat.com, j.alglave@....ac.uk, luc.maranget@...ia.fr,
	akiyks@...il.com, dlustig@...dia.com, joel@...lfernandes.org,
	urezki@...il.com, quic_neeraju@...cinc.com, frederic@...nel.org,
	linux-kernel@...r.kernel.org, lkmm@...ts.linux.dev,
	hernan.poncedeleon@...weicloud.com
Subject: Re: [RFC] tools/memory-model: Rule out OOTA

On Fri, Jan 17, 2025 at 05:45:50PM +0100, Jonas Oberhauser wrote:
> 
> 
> Am 1/17/2025 um 4:52 PM schrieb Alan Stern:
> > On Thu, Jan 16, 2025 at 06:02:18PM -0500, Alan Stern wrote:
> > > On Thu, Jan 16, 2025 at 08:08:22PM +0100, Jonas Oberhauser wrote:
> > This is a slight variation of the example on page 19 (section 4.3) of
> > the paper.  (Pretend this is actually C++ code, the shared variables are
> > all atomic, and their accesses are all relaxed.)
> > 
> > bool x, y, z;
> > 
> > void P0(bool *x, bool *y, bool *z) {
> > 	bool r1, r2;
> > 
> > 	r1 = *x;
> > 	r2 = *y;
> > 
> > 	*z = (r1 != r2);
> > }
> > 
> > The paper points out that although there is an apparent semantic
> > dependency from the load of x to the store to z, if the compiler is
> > allowed not to handle atomics as quasi volatile then the dependency
> > can be broken.  Nevertheless, I am not able to think of a program that
> > could exhibit OOTA as a result of breaking the semantic dependency.  The
> > best I can come up with is this:
> > 
> > [P0 as above]
> > 
> > void P1(bool *x, bool *y, bool *z) {
> > 	bool r3;
> > 
> > 	r3 = z;
> > 	x = r3;
> > }
> > 
> > void P2(bool *x, bool *y, bool *z) {
> > 	y = true;
> > }
> > 
> > exists (x=true /\ z=true)
> > 
> > If P2 were not present, this result could not occur in any physical
> > execution, even if the dependency in P0 is broken.  With P2 this result
> > isn't OOTA, even in executions where P0 ends up storing z before loading
> > x, because P2 could have executed first, then P0, then P1.
> > 
> > So perhaps this is an example of what you were talking about -- a
> > dependency which may or may not be semantic, but either way cannot lead
> > to OOTA.
> 
> Yes, that looks like an example of what I have in mind.
> 
> If at the model level we just say "yes there is a dependency, but no it does
> not give any ordering guarantee", then the compiler is still free to break
> the dependency like in your example.
> 
> A thread P3 { r1 = z; atomic_thread_fence(); r2 = y; }
> could still observe r2 == false, r1 == true, "showing" that the dependency
> was broken.

That wouldn't prove anything unless P0 had its own memory barrier 
somewhere before it stored z.

At any rate, I don't have any ideas on how to characterize semantic 
dependencies that can be broken without risking OOTA.  (Some people 
would say that if a dependency can be broken at all, that demonstrates 
it wasn't semantic to begin with.)

Alan