Messages in this thread | | | Date | Wed, 18 Jan 2023 13:13:33 +0100 | Subject | Re: [PATCH] tools/memory-model: Make ppo a subrelation of po | From | Jonas Oberhauser <> |
| |
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
| |