Received-SPF: pass (google.com: domain of linux-kernel+bounces-188835-linux.lists.archive=gmail.com@vger.kernel.org designates 2604:1380:40f1:3f00::1 as permitted sender) client-ip=2604:1380:40f1:3f00::1;
From: Andrea Parri <parri.andrea@gmail.com>
To: stern@rowland.harvard.edu,
	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,
	paulmck@kernel.org,
	akiyks@gmail.com,
	dlustig@nvidia.com,
	joel@joelfernandes.org
Cc: linux-kernel@vger.kernel.org,
	linux-arch@vger.kernel.org,
	hernan.poncedeleon@huaweicloud.com,
	jonas.oberhauser@huaweicloud.com,
	Andrea Parri <parri.andrea@gmail.com>
Subject: [PATCH] tools/memory-model: Document herd7 (internal) representation
Date: Fri, 24 May 2024 17:13:56 +0200
Message-Id: <20240524151356.236071-1-parri.andrea@gmail.com>
Precedence: bulk
MIME-Version: 1.0
Content-Transfer-Encoding: 8bit

tools/memory-model/ and herdtool7 are closely linked: the latter is
responsible for (pre)processing each C-like macro of a litmus test,
and for providing the LKMM with a set of events, or "representation",
corresponding to the given macro.  Provide herd-representation.txt
to document the representation of synchronization macros, following
their "classification" in Documentation/atomic_t.txt.

Suggested-by: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com>
Signed-off-by: Andrea Parri <parri.andrea@gmail.com>
---
- Leaving srcu_{up,down}_read() and smp_mb__after_srcu_read_unlock() for
  the next version.

- Limiting to "add" and "and" ops (skipping similar/same representations
  for "sub", "inc", "dec", "or", "xor", "andnot").

- While preparing this submission, I recalled that atomic_add_unless()
  is not listed in the .def file.  I can't remember the reason for this
  omission though.

- 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.


 .../Documentation/herd-representation.txt     | 81 +++++++++++++++++++
 1 file changed, 81 insertions(+)
 create mode 100644 tools/memory-model/Documentation/herd-representation.txt

diff --git a/tools/memory-model/Documentation/herd-representation.txt b/tools/memory-model/Documentation/herd-representation.txt
new file mode 100644
index 0000000000000..94d0d0a9eee50
--- /dev/null
+++ b/tools/memory-model/Documentation/herd-representation.txt
@@ -0,0 +1,81 @@
+    ---------------------------------------------------------------------------
+    |                     C macro | Events                                    |
+    ---------------------------------------------------------------------------
+    |                 Non-RMW ops |                                           |
+    ---------------------------------------------------------------------------
+    |                   READ_ONCE | R[once]                                   |
+    |                 atomic_read | (as in the previous row)                  |
+    |                  WRITE_ONCE | W[once]                                   |
+    |                  atomic_set |                                           |
+    |            smp_load_acquire | R[acquire]                                |
+    |         atomic_read_acquire |                                           |
+    |           smp_store_release | W[release]                                |
+    |          atomic_set_release |                                           |
+    |                smp_store_mb | W[once] ->po F[mb]                        |
+    |                      smp_mb | F[mb]                                     |
+    |                     smp_rmb | F[rmb]                                    |
+    |                     smp_wmb | F[wmb]                                    |
+    |       smp_mb__before_atomic | F[before-atomic]                          |
+    |        smp_mb__after_atomic | F[after-atomic]                           |
+    |                 spin_unlock | UL                                        |
+    |      smp_mb__after_spinlock | F[after-spinlock]                         |
+    |   smp_mb__after_unlock_lock | F[after-unlock-lock]                      |
+    |               rcu_read_lock | F[rcu-lock]                               |
+    |             rcu_read_unlock | F[rcu-unlock]                             |
+    |             synchronize_rcu | F[sync-rcu]                               |
+    |             rcu_dereference | R[once]                                   |
+    |          rcu_assign_pointer | W[release]                                |
+    |              srcu_read_lock | R[srcu-lock]                              |
+    |            srcu_read_unlock | W[srcu-unlock]                            |
+    |            synchronize_srcu | SRCU[sync-srcu]                           |
+    ---------------------------------------------------------------------------
+    |    RMW ops w/o return value |                                           |
+    ---------------------------------------------------------------------------
+    |                  atomic_add | R*[noreturn] ->rmw W*[once]               |
+    |                  atomic_and |                                           |
+    |                   spin_lock | LKR ->lk-rmw LKW                          |
+    ---------------------------------------------------------------------------
+    |     RMW ops w/ return value |                                           |
+    ---------------------------------------------------------------------------
+    |           atomic_add_return | F[mb] ->po R*[once]                       |
+    |                             |     ->rmw W*[once] ->po F[mb]             |
+    |            atomic_fetch_add |                                           |
+    |            atomic_fetch_and |                                           |
+    |                 atomic_xchg |                                           |
+    |                        xchg |                                           |
+    |         atomic_add_negative |                                           |
+    |   atomic_add_return_relaxed | R*[once] ->rmw W*[once]                   |
+    |    atomic_fetch_add_relaxed |                                           |
+    |    atomic_fetch_and_relaxed |                                           |
+    |         atomic_xchg_relaxed |                                           |
+    |                xchg_relaxed |                                           |
+    | atomic_add_negative_relaxed |                                           |
+    |   atomic_add_return_acquire | R*[acquire] ->rmw W*[once]                |
+    |    atomic_fetch_add_acquire |                                           |
+    |    atomic_fetch_and_acquire |                                           |
+    |         atomic_xchg_acquire |                                           |
+    |                xchg_acquire |                                           |
+    | atomic_add_negative_acquire |                                           |
+    |   atomic_add_return_release | R*[once] ->rmw W*[release]                |
+    |    atomic_fetch_add_release |                                           |
+    |    atomic_fetch_and_release |                                           |
+    |         atomic_xchg_release |                                           |
+    |                xchg_release |                                           |
+    | atomic_add_negative_release |                                           |
+    ---------------------------------------------------------------------------
+    |         Conditional RMW ops |                                           |
+    ---------------------------------------------------------------------------
+    |              atomic_cmpxchg | On success: F[mb] ->po R*[once]           |
+    |                             |                 ->rmw W*[once] ->po F[mb] |
+    |                             |     On failure: R*[once]                  |
+    |                     cmpxchg |                                           |
+    |           atomic_add_unless |                                           |
+    |      atomic_cmpxchg_relaxed | On success: R*[once] ->rmw W*[once]       |
+    |                             |     On failure: R*[once]                  |
+    |      atomic_cmpxchg_acquire | On success: R*[acquire] ->rmw W*[once]    |
+    |                             |     On failure: R*[once]                  |
+    |      atomic_cmpxchg_release | On success: R*[once] ->rmw W*[release]    |
+    |                             |     On failure: R*[once]                  |
+    |                spin_trylock | On success: LKR ->lk-rmw LKW              |
+    |                             |     On failure: LF                        |
+    ---------------------------------------------------------------------------
-- 
2.34.1