lkml.org 
[lkml]   [2023]   [Jan]   [18]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
Date
SubjectRe: [PATCH] tools/memory-model: Make ppo a subrelation of po
From


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

\
 
 \ /
  Last update: 2023-03-26 23:45    [W:0.068 / U:0.252 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site