Home
last modified time | relevance | path

Searched hist:"9393998 e" (Results 1 – 3 of 3) sorted by relevance

/openbmc/linux/tools/memory-model/
H A Dlinux-kernel.bell9393998e Thu Dec 27 09:27:12 CST 2018 Luc Maranget <Luc.Maranget@inria.fr> tools/memory-model: Dynamically check SRCU lock-to-unlock matching

This commit checks that the return value of srcu_read_lock() is passed
to the matching srcu_read_unlock(), where "matching" is determined by
nesting. This check operates as follows:

1. srcu_read_lock() creates an integer token, which is stored into
the generated events.
2. srcu_read_unlock() records its second (token) argument into the
generated event.
3. A new herd primitive 'different-values' filters out pairs of events
with identical values from the relation passed as its argument.
4. The bell file applies the above primitive to the (srcu)
read-side-critical-section relation 'srcu-rscs' and flags non-empty
results.

BEWARE: Works only with herd version 7.51+6 and onwards.

Signed-off-by: Luc Maranget <Luc.Maranget@inria.fr>
Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
[ paulmck: Apply Andrea Parri's off-list feedback. ]
Acked-by: Alan Stern <stern@rowland.harvard.edu>
9393998e Thu Dec 27 09:27:12 CST 2018 Luc Maranget <Luc.Maranget@inria.fr> tools/memory-model: Dynamically check SRCU lock-to-unlock matching

This commit checks that the return value of srcu_read_lock() is passed
to the matching srcu_read_unlock(), where "matching" is determined by
nesting. This check operates as follows:

1. srcu_read_lock() creates an integer token, which is stored into
the generated events.
2. srcu_read_unlock() records its second (token) argument into the
generated event.
3. A new herd primitive 'different-values' filters out pairs of events
with identical values from the relation passed as its argument.
4. The bell file applies the above primitive to the (srcu)
read-side-critical-section relation 'srcu-rscs' and flags non-empty
results.

BEWARE: Works only with herd version 7.51+6 and onwards.

Signed-off-by: Luc Maranget <Luc.Maranget@inria.fr>
Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
[ paulmck: Apply Andrea Parri's off-list feedback. ]
Acked-by: Alan Stern <stern@rowland.harvard.edu>
H A Dlinux-kernel.def9393998e Thu Dec 27 09:27:12 CST 2018 Luc Maranget <Luc.Maranget@inria.fr> tools/memory-model: Dynamically check SRCU lock-to-unlock matching

This commit checks that the return value of srcu_read_lock() is passed
to the matching srcu_read_unlock(), where "matching" is determined by
nesting. This check operates as follows:

1. srcu_read_lock() creates an integer token, which is stored into
the generated events.
2. srcu_read_unlock() records its second (token) argument into the
generated event.
3. A new herd primitive 'different-values' filters out pairs of events
with identical values from the relation passed as its argument.
4. The bell file applies the above primitive to the (srcu)
read-side-critical-section relation 'srcu-rscs' and flags non-empty
results.

BEWARE: Works only with herd version 7.51+6 and onwards.

Signed-off-by: Luc Maranget <Luc.Maranget@inria.fr>
Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
[ paulmck: Apply Andrea Parri's off-list feedback. ]
Acked-by: Alan Stern <stern@rowland.harvard.edu>
9393998e Thu Dec 27 09:27:12 CST 2018 Luc Maranget <Luc.Maranget@inria.fr> tools/memory-model: Dynamically check SRCU lock-to-unlock matching

This commit checks that the return value of srcu_read_lock() is passed
to the matching srcu_read_unlock(), where "matching" is determined by
nesting. This check operates as follows:

1. srcu_read_lock() creates an integer token, which is stored into
the generated events.
2. srcu_read_unlock() records its second (token) argument into the
generated event.
3. A new herd primitive 'different-values' filters out pairs of events
with identical values from the relation passed as its argument.
4. The bell file applies the above primitive to the (srcu)
read-side-critical-section relation 'srcu-rscs' and flags non-empty
results.

BEWARE: Works only with herd version 7.51+6 and onwards.

Signed-off-by: Luc Maranget <Luc.Maranget@inria.fr>
Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
[ paulmck: Apply Andrea Parri's off-list feedback. ]
Acked-by: Alan Stern <stern@rowland.harvard.edu>
H A Dlinux-kernel.cat9393998e Thu Dec 27 09:27:12 CST 2018 Luc Maranget <Luc.Maranget@inria.fr> tools/memory-model: Dynamically check SRCU lock-to-unlock matching

This commit checks that the return value of srcu_read_lock() is passed
to the matching srcu_read_unlock(), where "matching" is determined by
nesting. This check operates as follows:

1. srcu_read_lock() creates an integer token, which is stored into
the generated events.
2. srcu_read_unlock() records its second (token) argument into the
generated event.
3. A new herd primitive 'different-values' filters out pairs of events
with identical values from the relation passed as its argument.
4. The bell file applies the above primitive to the (srcu)
read-side-critical-section relation 'srcu-rscs' and flags non-empty
results.

BEWARE: Works only with herd version 7.51+6 and onwards.

Signed-off-by: Luc Maranget <Luc.Maranget@inria.fr>
Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
[ paulmck: Apply Andrea Parri's off-list feedback. ]
Acked-by: Alan Stern <stern@rowland.harvard.edu>
9393998e Thu Dec 27 09:27:12 CST 2018 Luc Maranget <Luc.Maranget@inria.fr> tools/memory-model: Dynamically check SRCU lock-to-unlock matching

This commit checks that the return value of srcu_read_lock() is passed
to the matching srcu_read_unlock(), where "matching" is determined by
nesting. This check operates as follows:

1. srcu_read_lock() creates an integer token, which is stored into
the generated events.
2. srcu_read_unlock() records its second (token) argument into the
generated event.
3. A new herd primitive 'different-values' filters out pairs of events
with identical values from the relation passed as its argument.
4. The bell file applies the above primitive to the (srcu)
read-side-critical-section relation 'srcu-rscs' and flags non-empty
results.

BEWARE: Works only with herd version 7.51+6 and onwards.

Signed-off-by: Luc Maranget <Luc.Maranget@inria.fr>
Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
[ paulmck: Apply Andrea Parri's off-list feedback. ]
Acked-by: Alan Stern <stern@rowland.harvard.edu>