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

[Jonas Oberhauser]

Am 1/16/2025 um 7:40 PM schrieb Paul E. McKenney:
> 	o	If a value is read in the seqlock reader and used
> 		across a "you need to retry" indication, that
> 		flags a seqlock data race.


This too is insufficient, you also need to prevent dereferencing or 
having control dependency inside the seqlock. Otherwise you could 
derefence a torn pointer and...

At this point your definition of data race becomes pretty much the same 
as we have.

https://github.com/open-s4c/libvsync/blob/main/vmm/vmm.cat#L150


(also this rule should only concern reads that are actually "data-racy" 
- if the read is synchronized by some other writes, then you can read & 
use it just fine across the seqlock data race)

I also noticed that in my previous e-mail I had overlooked the reads 
inside the CS in the failure case, but you are of course right, there 
needs to be some mechanism to prevent them from being data racy unless 
abused.

But I am not sure how to formalize that in a way that is simpler than 
just re-defining data races in general, without adding some special 
support to herd7 for it.

What do you think?


  jonas