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 for Android: free password hash cracker in your pocket

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

Message-ID: <a1019624-7f82-4897-a1f2-3a381794b2ad@huaweicloud.com>
Date: Fri, 17 Jan 2025 17:45:50 +0100
From: Jonas Oberhauser <jonas.oberhauser@...weicloud.com>
To: Alan Stern <stern@...land.harvard.edu>
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



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:
>>> I would say that the approach with volatile is overzealous because it tries
>>> to create a "local" order solution to the problem that only requires a
>>> "global" ordering solution. Since not every semantic dependency needs to
>>> provide order in C++ -- only the cycle of dependencies -- it is totally ok
>>> to add too many semantic dependency edges to a program, even those that are
>>> not going to be exactly maintained by every compiler, as long as we can
>>> ensure that globally, no dependency cycle occurs.
>>
>> But then how would you characterize semantic dependencies, if you want
>> to allow the definition to include some dependencies that aren't
>> semantic but not so many that you ever create a cycle?  This sounds like
>> an even worse problem than we started with!
> 
> An interesting side comment on this issue...
> 
> 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.

This would not violate such a model.

(if we consider consume, then that would need to restrict the compiler 
from eliminating the dependency like this)

That is not to say that I am 100% sure that it is possible to define 
sdep correctly to make this work.
One problem is if the compiler merges two threads (with an OOTA cycle of 
3+ threads), it can turn sdep;rfe;sdep;rfe into sdep;rfi;sdep;rfe.
If sdep is too naive then it is easy to come up with counter examples 
where this sdep;rfi;sdep no longer provides ordering, making the whole 
sdep;rfe cycle possible.

I am not sure if sdep can be formalized in a way that ensures that this 
sdep;rfi;sdep edge would still need to be preserved.

Of course one could have inter-thread semantic dependencies and only forbid
   isdep ; rf (e?)
from being reflexive...

Best wishes,
   jonas