From: Andrea Parri <parri.andrea@gmail.com>
To: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com>
Cc: Alan Stern <stern@rowland.harvard.edu>,
Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>,
"Paul E. McKenney" <paulmck@kernel.org>,
linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org,
kernel-team@meta.com, boqun.feng@gmail.com, j.alglave@ucl.ac.uk,
luc.maranget@inria.fr, Joel Fernandes <joel@joelfernandes.org>
Subject: Re: LKMM: Making RMW barriers explicit
Date: Thu, 23 May 2024 11:04:16 +0200 [thread overview]
Message-ID: <Zk8GkFlnKeyIgYQb@andrea> (raw)
In-Reply-To: <22b9837b-16c2-5413-3cd7-4d3a47252a6a@huaweicloud.com>
> It would be much simpler if
> one could find all the information to support lkmm in tools/memory-model/
> (in the form of the model + some comments or a .txt to cover those things we
> cannot move out of the tool implementation), rather than having to dive into
> herd7 code.
Got it. And I do find that very relatable to LKMM developers who, like me,
are definitely not fluent in OCaml. :-/
Let me draft some .txt to such effect, based on but expanding and hopefully
completing my previous remarks in
https://lore.kernel.org/lkml/ZjrSm119+IfIU9eU@andrea/
Having something like that "on paper" can also help evaluate future changes
to the tool and/or model.
Thank you for the suggestion.
Andrea
next prev parent reply other threads:[~2024-05-23 9:04 UTC|newest]
Thread overview: 33+ messages / expand[flat|nested] mbox.gz Atom feed top
2024-05-16 1:43 LKMM: Making RMW barriers explicit Alan Stern
2024-05-16 8:31 ` Jonas Oberhauser
2024-05-16 8:44 ` Hernan Ponce de Leon
2024-05-18 0:31 ` Alan Stern
2024-05-21 9:57 ` Jonas Oberhauser
2024-05-21 15:36 ` Alan Stern
2024-05-22 9:20 ` Jonas Oberhauser
2024-05-22 14:20 ` Alan Stern
2024-05-22 16:54 ` Andrea Parri
2024-05-22 18:20 ` Alan Stern
2024-05-22 19:48 ` Hernan Ponce de Leon
2024-05-23 9:04 ` Andrea Parri [this message]
2024-05-23 14:27 ` Jonas Oberhauser
2024-05-23 16:35 ` Andrea Parri
2024-05-23 20:30 ` Jonas Oberhauser
2024-05-24 3:30 ` Andrea Parri
2024-05-24 8:16 ` Hernan Ponce de Leon
2024-05-23 12:54 ` Jonas Oberhauser
2024-05-23 13:35 ` Paul E. McKenney
2024-05-23 14:05 ` Alan Stern
2024-05-23 14:26 ` Hernan Ponce de Leon
2024-05-23 15:14 ` Boqun Feng
2024-05-24 1:38 ` Alan Stern
2024-05-24 2:50 ` Boqun Feng
2024-05-24 14:14 ` Alan Stern
2024-05-24 14:34 ` Boqun Feng
2024-05-24 14:53 ` Alan Stern
2024-05-24 18:09 ` Jonas Oberhauser
2024-05-24 18:47 ` Boqun Feng
2024-05-24 18:48 ` Alan Stern
2024-05-23 16:05 ` Alan Stern
2024-05-23 14:36 ` Jonas Oberhauser
2024-05-21 11:38 ` Hernan Ponce de Leon
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=Zk8GkFlnKeyIgYQb@andrea \
--to=parri.andrea@gmail.com \
--cc=boqun.feng@gmail.com \
--cc=hernan.poncedeleon@huaweicloud.com \
--cc=j.alglave@ucl.ac.uk \
--cc=joel@joelfernandes.org \
--cc=jonas.oberhauser@huaweicloud.com \
--cc=kernel-team@meta.com \
--cc=linux-arch@vger.kernel.org \
--cc=linux-kernel@vger.kernel.org \
--cc=luc.maranget@inria.fr \
--cc=paulmck@kernel.org \
--cc=stern@rowland.harvard.edu \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.