[PATCH v2 0/2] Streamlining treatment of smp_mb__after_unlock_lock

Jonas Oberhauser
2023-01-26T13:42:33Z

Hi all,

This patchset first makes smp_mb__after_unlock_lock use po-unlock-lock-po
to express its ordering property on UNLOCK+LOCK pairs in a more uniform
way with the rest of the model. This does not affect the guarantees
provided by it, but if the solution proposed here is unsatisfactory, there
are two alternatives that spring to mind:

1) one could think about rephrasing the guarantee of this fence to
more obviously match the code

2) one could redefine po-unlock-lock-po to more obviously match the
definition of UNLOCK+LOCK pair in rcupdate.h (note: I haven't
yet checked every use of po-unlock-lock-po, so that would need to
be checked)

It then makes ppo a subset of po by moving the extended fence behaviors of
this fence (which covers events of two threads) out of ppo.

I'm also not sure how to correctly credit the helpful comments of the
reviewers on the first iteration of the patch.

Changes since the last patch proposal:

1) As suggested by Andrea Parri, the patches no longer introduce a new
relation and instead rely purely on strong-fence. Unlike his
suggestion these patches do not redefine strong-fence but instead
use mb | gp directly in the case where the extended fence is to be
excluded.

2) Following another suggestion by Andrea Parri, the patches no longer
update any documentation since there are no new relations.

3) We split the patch logically into two steps as mentioned above.

4) As suggested by Alan Stern, we explain in the model why the
mismatch between the UNLOCK+LOCK definition in rcupdate.h and the
definition of the semantics of the fence in the model is not
causing any difference in behavior.

Jonas Oberhauser (2):
tools/memory-model: Unify UNLOCK+LOCK pairings to po-unlock-lock-po
tools/memory-model: Make ppo a subrelation of po

tools/memory-model/linux-kernel.cat | 22 +++++++++++++++++-----
1 file changed, 17 insertions(+), 5 deletions(-)

--
2.17.1