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: Windows password security audit tool. GUI, reports in PDF.
[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]
Message-ID: <35bed95a-3203-43a7-972d-f3fd3c7da6f9@huaweicloud.com>
Date: Thu, 24 Oct 2024 13:44:24 +0200
From: Jonas Oberhauser <jonas.oberhauser@...weicloud.com>
To: Andrea Parri <parri.andrea@...il.com>, puranjay@...nel.org,
 paulmck@...nel.org
Cc: bpf@...r.kernel.org, lkmm@...ts.linux.dev, linux-kernel@...r.kernel.org
Subject: Re: Some observations (results) on BPF acquire and release



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


Powered by blists - more mailing lists

Powered by Openwall GNU/*/Linux Powered by OpenVZ