linux-kernel - Re: Some observations (results) on BPF acquire and release

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: <ecb585c5-7f56-4249-b525-66d9757a6f2f@huaweicloud.com>
Date: Thu, 24 Oct 2024 14:21:15 +0200
From: Jonas Oberhauser <jonas.oberhauser@...weicloud.com>
To: Puranjay Mohan <puranjay@...nel.org>,
 Andrea Parri <parri.andrea@...il.com>, 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/24/2024 um 2:11 PM schrieb Puranjay Mohan:
> Jonas Oberhauser <jonas.oberhauser@...weicloud.com> writes:
> 
>> 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.
> 

Thanks Puranjay for your response!


 > BPF memory model is an instruction level memory model

You mean BPF has no optimizing byte code compiler?
Is it guaranteed to stay this way?
WASM does JIT optimizations as far as I know, which would bring back a 
lot of the complexity of software models like LKMM.

 > much simpler than LKMM

LKMM has a simple core, roughly like this:

ppo = ... (* all the ppo related rules that are relevant to you -- some 
fences don't matter and you can just remove them *)
prop = (coe | fre) (* remove reflexive closure *) ; ...
hb = [Marked] ; (ppo | rfe | prop & int | prop ; strong-sync) ; [Marked]

acyclic hb
(* ... also add the atomicity & sc-per-loc axioms *)

If you can exclude compiler optimizations, you can remove the Marked bits.


Best wishes,

   jonas