linux-stable.git/tools/memory-model, branch linux-5.15.y

tools/memory-model: Fix bug in lock.cat

2024-08-19T03:45:15+00:00

commit 4c830eef806679dc243e191f962c488dd9d00708 upstream.

Andrea reported that the following innocuous litmus test:

C T

{}

P0(spinlock_t *x)
{
	int r0;

	spin_lock(x);
	spin_unlock(x);
	r0 = spin_is_locked(x);
}

gives rise to a nonsensical empty result with no executions:

$ 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

The problem is caused by a bug in the lock.cat part of the LKMM.  Its
computation of the rf relation for RU (read-unlocked) events is
faulty; it implicitly assumes that every RU event must read from
either a UL (unlock) event in another thread or from the lock's
initial state.  Neither is true in the litmus test above, so the
computation yields no possible executions.

The lock.cat code tries to make up for this deficiency by allowing RU
events outside of critical sections to read from the last po-previous
UL event.  But it does this incorrectly, trying to keep these rfi links
separate from the rfe links that might also be needed, and passing only
the latter to herd7's cross() macro.

The problem is fixed by merging the two sets of possible rf links for
RU events and using them all in the call to cross().

Signed-off-by: Alan Stern 
Reported-by: Andrea Parri 
Closes: https://lore.kernel.org/linux-arch/ZlC0IkzpQdeGj+a3@andrea/
Tested-by: Andrea Parri 
Acked-by: Andrea Parri 
Fixes: 15553dcbca06 ("tools/memory-model: Add model support for spin_is_locked()")
CC: 
Signed-off-by: Paul E. McKenney 
Signed-off-by: Greg Kroah-Hartman

tools/memory-model: Document data_race(READ_ONCE())

2021-07-27T18:48:55+00:00

It is possible to cause KCSAN to ignore marked accesses by applying
__no_kcsan to the function or applying data_race() to the marked accesses.
These approaches allow the developer to restrict compiler optimizations
while also causing KCSAN to ignore diagnostic accesses.

This commit therefore updates the documentation accordingly.

Signed-off-by: Paul E. McKenney

tools/memory-model: Heuristics using data_race() must handle all values

2021-07-27T18:48:55+00:00

Data loaded for use by some sorts of heuristics can tolerate the
occasional erroneous value.  In this case the loads may use data_race()
to give the compiler full freedom to optimize while also informing KCSAN
of the intent.  However, for this to work, the heuristic needs to be
able to tolerate any erroneous value that could possibly arise.  This
commit therefore adds a paragraph spelling this out.

Signed-off-by: Manfred Spraul 
Signed-off-by: Paul E. McKenney

tools/memory-model: Add example for heuristic lockless reads

2021-07-27T18:47:34+00:00

This commit adds example code for heuristic lockless reads, based loosely
on the sem_lock() and sem_unlock() functions.

[ paulmck: Apply Alan Stern and Manfred Spraul feedback. ]

Reported-by: Manfred Spraul 
[ paulmck: Update per Manfred Spraul and Hillf Danton feedback. ]
Signed-off-by: Paul E. McKenney

tools/memory-model: Make read_foo_diagnostic() more clearly diagnostic

2021-07-20T20:52:03+00:00

The current definition of read_foo_diagnostic() in the "Lock Protection
With Lockless Diagnostic Access" section returns a value, which could
be use for any purpose.  This could mislead people into incorrectly
using data_race() in cases where READ_ONCE() is required.  This commit
therefore makes read_foo_diagnostic() simply print the value read.

Reported-by: Manfred Spraul 
Signed-off-by: Paul E. McKenney

tools/memory-model: Fix smp_mb__after_spinlock() spelling

2021-05-10T23:27:20+00:00

A misspelled git-grep regex revealed that smp_mb__after_spinlock()
was misspelled in explanation.txt.  This commit adds the missing "_".

Fixes: 1c27b644c0fd ("Automate memory-barriers.txt; provide Linux-kernel memory model")
[ paulmck: Apply Alan Stern commit-log feedback. ]
Signed-off-by: Björn Töpel 
Signed-off-by: Paul E. McKenney

tools/memory-model: Add access-marking documentation

2021-03-15T20:59:47+00:00

This commit adapts the "Concurrency bugs should fear the big bad data-race
detector (part 2)" LWN article (https://lwn.net/Articles/816854/)
to kernel-documentation form.  This allows more easily updating the
material as needed.

Suggested-by: Thomas Gleixner 
[ paulmck: Apply Marco Elver feedback. ]
[ paulmck: Update per Akira Yokosawa feedback. ]
Reviewed-by: Marco Elver 
Signed-off-by: Paul E. McKenney

tools/memory-model: Remove reference to atomic_ops.rst

2021-03-08T22:29:22+00:00

atomic_ops.rst was removed by commit f0400a77ebdc ("atomic: Delete
obsolete documentation").
Remove the broken link in tools/memory-model/Documentation/simple.txt.

Cc: Peter Zijlstra 
Signed-off-by: Akira Yokosawa 
Signed-off-by: Paul E. McKenney

doc: Update rcu_dereference.rst reference

2021-03-08T22:29:22+00:00

Changeset b00aedf978aa ("doc: Convert to rcu_dereference.txt to rcu_dereference.rst")
renamed: Documentation/RCU/rcu_dereference.txt
to: Documentation/RCU/rcu_dereference.rst.

Update its cross-reference accordingly.

Signed-off-by: Mauro Carvalho Chehab 
Signed-off-by: Paul E. McKenney

tools/memory-model: Fix typo in klitmus7 compatibility table

2021-01-04T22:40:50+00:00

klitmus7 of herdtools7 7.48 or earlier depends on ACCESS_ONCE(),
which was removed in Linux v4.15.
Fix the obvious typo in the table.

Fixes: d075a78a5ab1 ("tools/memory-model/README: Expand dependency of klitmus7")
Signed-off-by: Akira Yokosawa 
Signed-off-by: Paul E. McKenney