On Mon, May 06, 2024 at 11:00:42AM -0700, Paul E. McKenney wrote: > On Mon, May 06, 2024 at 06:30:45PM +0200, Jonas Oberhauser wrote: > > Am 5/6/2024 um 12:05 PM schrieb Jonas Oberhauser: > > > Am 5/2/2024 um 1:21 AM schrieb Paul E. McKenney: > > > > This commit adds four litmus tests showing that a failing cmpxchg() > > > > operation is unordered unless followed by an smp_mb__after_atomic() > > > > operation. > > > > > > So far, my understanding was that all RMW operations without suffix > > > (xchg(), cmpxchg(), ...) will be interpreted as F[Mb];...;F[Mb]. It's more accurate to say that RMW operations without a suffix that return a value will be interpreted that way. So for example, atomic_inc() doesn't imply any ordering, because it doesn't return a value. > > > barriers explicitly inside the cat model, instead of relying on implicit > > > conversions internal to herd. Don't the annotations in linux-kernel.def and linux-kernel.bell (like "noreturn") already make this explicit? I guess the part that is still implicit is that herd7 doesn't regard failed RMW operations as actual RMWs (they don't have a store part). Alan
