Re: Some observations (results) on BPF acquire and release
From: Jonas Oberhauser
Date: Thu Oct 24 2024 - 07:44:58 EST
Am 10/23/2024 um 7:47 PM schrieb Andrea Parri:
Hi Puranjay and Paul,
These remarks show that the proposed BPF formalization of acquire and
release somehow, but substantially, diverged from the corresponding
LKMM formalization. My guess is that the divergences mentioned above
were not (fully) intentional, or I'm wondering -- why not follow the
latter (the LKMM's) more closely? - This is probably the first question
I would need to clarify before trying/suggesting modifications to the
present formalizations. ;-) Thoughts?
I'm also curious why the formalization (not just in the semantics but
also how it is structured) is so completely different from LKMM's.
At first glance there are also many semantic differences, e.g., it seems
coe is much weaker in eBPF and the last axiom also seems a bit like a
tack-on that doesn't "play well" with the previous axioms.
It would make sense to me to start with the framework of LKMM and maybe
weaken it from there if it is really necessary. But maybe I don't know
enough about how eBPF atomics are intended to work...
Best wishes,
jonas