Received-SPF: pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 2620:137:e000::1:20 as permitted sender) client-ip=2620:137:e000::1:20;
Message-ID: <2aae2d62-5437-178d-8e8a-19e420ea5b60@huaweicloud.com>
Date:   Wed, 18 Jan 2023 13:13:33 +0100
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:102.0) Gecko/20100101
 Thunderbird/102.6.1
Subject: Re: [PATCH] tools/memory-model: Make ppo a subrelation of po
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
References: <20230117193159.22816-1-jonas.oberhauser@huaweicloud.com>
 <Y8czI5O2CikVlIp8@boqun-archlinux>
From:   Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
In-Reply-To: <Y8czI5O2CikVlIp8@boqun-archlinux>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Precedence: bulk


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