From:   Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
To:     paulmck@kernel.org
Cc:     stern@rowland.harvard.edu, parri.andrea@gmail.com, will@kernel.org,
        peterz@infradead.org, boqun.feng@gmail.com, npiggin@gmail.com,
        dhowells@redhat.com, j.alglave@ucl.ac.uk, luc.maranget@inria.fr,
        akiyks@gmail.com, dlustig@nvidia.com, joel@joelfernandes.org,
        urezki@gmail.com, quic_neeraju@quicinc.com, frederic@kernel.org,
        linux-kernel@vger.kernel.org,
        Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
Subject: [PATCH v2 0/2] Streamlining treatment of smp_mb__after_unlock_lock
Date:   Thu, 26 Jan 2023 14:46:02 +0100
Message-Id: <20230126134604.2160-1-jonas.oberhauser@huaweicloud.com>
Precedence: bulk

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