Received-SPF: pass (google.com: domain of linux-kernel+bounces-190573-linux.lists.archive=gmail.com@vger.kernel.org designates 2604:1380:40f1:3f00::1 as permitted sender) client-ip=2604:1380:40f1:3f00::1;
Message-ID: <1a3c892c-903e-8fd3-24a6-2454c2a55302@huaweicloud.com>
Date: Mon, 27 May 2024 14:22:47 +0200
Precedence: bulk
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:102.0) Gecko/20100101
 Thunderbird/102.13.0
Subject: Re: [PATCH] tools/memory-model: Document herd7 (internal)
 representation
To: Andrea Parri <parri.andrea@gmail.com>, 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,
 jonas.oberhauser@huaweicloud.com
References: <20240524151356.236071-1-parri.andrea@gmail.com>
Content-Language: en-US
From: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com>
In-Reply-To: <20240524151356.236071-1-parri.andrea@gmail.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit

On 5/24/2024 5:13 PM, Andrea Parri wrote:
> 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]                        |

I expect this one to be hard-coded in herd7 source code, but I cannot 
find it. Can you give me a pointer?

In fact, dartagnan uses W[Mb] ... another clear example of the need for 
documentation as this one.

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

What about spin_unlock?

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

I found the extra spaces in the failure case very hard to read. Any 
particular reason why you went with this format?

Hernan