linux-kernel - Re: [PATCH] tools/memory-model: Make ppo a subrelation of po

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite for Android: free password hash cracker in your pocket

[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]

Message-ID: <2aae2d62-5437-178d-8e8a-19e420ea5b60@huaweicloud.com>
Date:   Wed, 18 Jan 2023 13:13:33 +0100
From:   Jonas Oberhauser <jonas.oberhauser@...weicloud.com>
To:     Boqun Feng <boqun.feng@...il.com>
Cc:     paulmck@...nel.org, stern@...land.harvard.edu,
        parri.andrea@...il.com, will@...nel.org, peterz@...radead.org,
        npiggin@...il.com, dhowells@...hat.com, j.alglave@....ac.uk,
        luc.maranget@...ia.fr, akiyks@...il.com, dlustig@...dia.com,
        joel@...lfernandes.org, urezki@...il.com, quic_neeraju@...cinc.com,
        frederic@...nel.org, linux-kernel@...r.kernel.org
Subject: Re: [PATCH] tools/memory-model: Make ppo a subrelation of po

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