On Fri, May 24, 2024 at 05:37:06PM +0200, Andrea Parri wrote: > > - While checking the information below using herd7, I've observed some > > "strange" behavior with spin_is_locked() (perhaps, unsurprisingly...); > > IAC, that's also excluded from this table/submission. > > For completeness, the behavior in question: > > $ cat T.litmus > C T > > {} > > P0(spinlock_t *x) > { > int r0; > > spin_lock(x); > spin_unlock(x); > r0 = spin_is_locked(x); > } No "exists" clause? Maybe that's your problem. Alan > > $ herd7 -conf linux-kernel.cfg T.litmus > Test T Required > States 0 > Ok > Witnesses > Positive: 0 Negative: 0 > Condition forall (true) > Observation T Never 0 0 > Time T 0.00 > Hash=6fa204e139ddddf2cb6fa963bad117c0 > > Haven't been using spin_is_locked for a while... perhaps I'm doing > something wrong? (IAC, will have a closer look next week...) > > Andrea