From: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
To: Boqun Feng <boqun.feng@gmail.com>
Cc: paulmck@kernel.org, stern@rowland.harvard.edu,
parri.andrea@gmail.com, will@kernel.org, peterz@infradead.org,
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
Subject: Re: [PATCH] tools/memory-model: Make ppo a subrelation of po
Date: Wed, 18 Jan 2023 13:13:33 +0100 [thread overview]
Message-ID: <2aae2d62-5437-178d-8e8a-19e420ea5b60@huaweicloud.com> (raw)
In-Reply-To: <Y8czI5O2CikVlIp8@boqun-archlinux>
On 1/18/2023 12:45 AM, Boqun Feng wrote:
> On Tue, Jan 17, 2023 at 08:31:59PM +0100, Jonas Oberhauser wrote:
>> ---
>> .../Documentation/explanation.txt | 101 +++++++++++-------
>> tools/memory-model/linux-kernel.cat | 20 ++--
> I've reviewed the cat change part, and it looks good to me.
It's not the cat part that worries me! I'm worried that I made the
explanation inconsistent somewhere, or that it's not very
understandable. If you have time, please take a look at that as well.
> One more thing, do we want something in the cat file to describe our
> "internal axioms" as follow?
>
> (* Model internal invariants *)
> (* ppo is the subset of po *)
> flag ~empty (ppo \ po) as INTERNAL-ERROR-PPO
>
> Maybe it's helpful for people working on other tools to understand LKMM
> cat file?
I've thought that there should be a way to continuously test/prove
properties of LKMM so that future changes to LKMM can't silently
invalidate these properites (like what happened when this fence was
added to LKMM).
I'm not sure yet what's the best way to do this. I suppose a simple
first step could be to have an additional cat file lkmm-properties.cat
that flags all violations of the properties in the litmus tests, but I'm
not sure how much that really helps: I think many violations are not
present in any of the existing litmus tests. And some properties are
hard to state as a cat flag.
best wishes and thanks for reviewing,
jonas
next prev parent reply other threads:[~2023-01-18 12:52 UTC|newest]
Thread overview: 29+ messages / expand[flat|nested] mbox.gz Atom feed top
2023-01-17 19:31 [PATCH] tools/memory-model: Make ppo a subrelation of po Jonas Oberhauser
2023-01-17 23:45 ` Boqun Feng
2023-01-18 12:13 ` Jonas Oberhauser [this message]
2023-01-18 19:52 ` Alan Stern
2023-01-18 20:22 ` Andrea Parri
2023-01-18 21:38 ` Jonas Oberhauser
2023-01-19 3:13 ` Alan Stern
2023-01-19 15:05 ` Jonas Oberhauser
2023-01-19 20:06 ` Alan Stern
2023-01-20 11:12 ` Jonas Oberhauser
2023-01-20 16:32 ` Alan Stern
2023-01-21 0:41 ` Jonas Oberhauser
2023-01-21 20:56 ` Alan Stern
2023-01-23 13:59 ` Jonas Oberhauser
2023-01-23 17:28 ` Alan Stern
2023-01-23 19:33 ` Jonas Oberhauser
2023-01-23 21:10 ` Alan Stern
2023-01-24 13:14 ` Jonas Oberhauser
2023-01-24 17:14 ` Alan Stern
2023-01-24 20:23 ` Jonas Oberhauser
2023-01-25 2:57 ` Alan Stern
2023-01-25 13:06 ` Jonas Oberhauser
2023-01-25 15:56 ` Alan Stern
2023-01-23 18:25 ` Jonas Oberhauser
2023-01-23 20:25 ` Alan Stern
2023-01-24 12:54 ` Jonas Oberhauser
2023-01-24 16:03 ` Alan Stern
2023-01-18 21:30 ` Andrea Parri
2023-01-18 22:02 ` Jonas Oberhauser
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=2aae2d62-5437-178d-8e8a-19e420ea5b60@huaweicloud.com \
--to=jonas.oberhauser@huaweicloud.com \
--cc=akiyks@gmail.com \
--cc=boqun.feng@gmail.com \
--cc=dhowells@redhat.com \
--cc=dlustig@nvidia.com \
--cc=frederic@kernel.org \
--cc=j.alglave@ucl.ac.uk \
--cc=joel@joelfernandes.org \
--cc=linux-kernel@vger.kernel.org \
--cc=luc.maranget@inria.fr \
--cc=npiggin@gmail.com \
--cc=parri.andrea@gmail.com \
--cc=paulmck@kernel.org \
--cc=peterz@infradead.org \
--cc=quic_neeraju@quicinc.com \
--cc=stern@rowland.harvard.edu \
--cc=urezki@gmail.com \
--cc=will@kernel.org \
/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 a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).