linux-kernel - Re: Internal vs. external barriers (was: Re: Interesting LKMM litmus test)

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: <736020be-de00-3cd8-2325-c3efb87e03b6@huaweicloud.com>
Date:   Sat, 21 Jan 2023 01:03:50 +0100
From:   Jonas Oberhauser <jonas.oberhauser@...weicloud.com>
To:     paulmck@...nel.org
Cc:     Alan Stern <stern@...land.harvard.edu>,
        Andrea Parri <parri.andrea@...il.com>,
        Jonas Oberhauser <jonas.oberhauser@...wei.com>,
        Peter Zijlstra <peterz@...radead.org>, will <will@...nel.org>,
        "boqun.feng" <boqun.feng@...il.com>, npiggin <npiggin@...il.com>,
        dhowells <dhowells@...hat.com>,
        "j.alglave" <j.alglave@....ac.uk>,
        "luc.maranget" <luc.maranget@...ia.fr>, akiyks <akiyks@...il.com>,
        dlustig <dlustig@...dia.com>, joel <joel@...lfernandes.org>,
        urezki <urezki@...il.com>,
        quic_neeraju <quic_neeraju@...cinc.com>,
        frederic <frederic@...nel.org>,
        Kernel development list <linux-kernel@...r.kernel.org>
Subject: Re: Internal vs. external barriers (was: Re: Interesting LKMM litmus
 test)



On 1/21/2023 12:19 AM, Paul E. McKenney wrote:
> On Fri, Jan 20, 2023 at 11:36:15PM +0100, Jonas Oberhauser wrote:
>>
>> On 1/20/2023 10:37 PM, Paul E. McKenney wrote:
>>> Just out of curiosity, are you [set] up to run LKMM locally at your end?
>> I don't know what exactly that means. I generally run it on wetware.
>> But I sometimes ask Hernan to run Dat3M (on his machine) over all the litmus
>> tests in your repo to spot any obvious problems with variations I consider.
>> I don't think Dat3M is feature-complete with herd at the moment, just
>> unbelievably faster. For example I think it ignores all flags in the cat
>> files.
>> Oh, I just remembered that I also installed herd7 recently to make sure that
>> any patches I might send in satisfy herd7 syntax requirements (I think you
>> called this diagnostic driven development?), but I haven't used it to really
>> run anything.
>>
>> Is it too obvious that my words usually aren't backed by cold machine logic?
> Well, there was this in one of your messages from earlier today: "I'm not
> going to get it right today, am I?"  And I freely confess that this led
> me to suspect that you might not have been availing yourself of herd7's
> opinion before posting.  ;-)
The main reason I might usually not consult herd7's opinion is that it 
often takes a while to write a test case in a way herd7 accepts and 
treats as intended, but then even so the fact that some tests pass may 
just give some false confidence when some tricky case is being missed.
So I find the investment/increased confidence ratio to not yet be at the 
right point to do this when communicating somewhat informally on the 
mailing list, which is already taking quite a bit of my time (but at 
least I'm learning a lot during that time about stuff like RCU/SRCU, 
history of LKMM, etc.).
If I need to be more confident I'll use herd7 to make sure the syntax is 
correct and as a sanity check, and some paper or Coq proofs to be 
confident in the logic.

If you feel that I'm wasting the lists' time too much by making these 
kind of mistakes, let me know and I'll reconsider.

Best wishes, jonas