linux-kernel - Re: [PATCH v3 4/5] tools/memory-model: Switch to softcoded herd7 tags

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] [day] [month] [year] [list]

Message-ID: <a333f5f9-ffc0-4dea-80de-92e275492235@gmail.com>
Date: Sat, 21 Sep 2024 20:28:04 +0900
From: Akira Yokosawa <akiyks@...il.com>
To: Jonas Oberhauser <jonas.oberhauser@...weicloud.com>, paulmck@...nel.org
Cc: stern@...land.harvard.edu, parri.andrea@...il.com, will@...nel.org,
 peterz@...radead.org, boqun.feng@...il.com, npiggin@...il.com,
 dhowells@...hat.com, j.alglave@....ac.uk, luc.maranget@...ia.fr,
 dlustig@...dia.com, joel@...lfernandes.org, urezki@...il.com,
 quic_neeraju@...cinc.com, frederic@...nel.org, linux-kernel@...r.kernel.org,
 lkmm@...ts.linux.dev, hernan.poncedeleon@...weicloud.com,
 Akira Yokosawa <akiyks@...il.com>
Subject: Re: [PATCH v3 4/5] tools/memory-model: Switch to softcoded herd7 tags

Hi,

On Sat, 21 Sep 2024 09:39:05 +0200, Jonas Oberhauser wrote:
> Thanks Akira for your continued eagle eyes!
> Will include in next revision.
> 
> One question below.
>  jonas
> 
> 
> 
> Am 9/21/2024 um 4:44 AM schrieb Akira Yokosawa:
>> This litmus test is not compatible with klitmus7, which is much
>> stricter than herd7's C parser.
>>
>> You can have only int or int* variables in the exists clause.

I should have said:

   By default, you can have only int or int* variables in the exists clause.

You can find an example where an atomic_t variable is listed in its exists
clause at:

    Documentation/litmus-tests/atomic/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus

, where the atomic_t variable is declared explicitly in the initialization
block as follows:

    {
	atomic_t v = ATOMIC_INIT(1);
    }

>> Register variables need their declarations at the top of each Pn()
>> (classic C).
>>
>> See below for klitmus7 ready code.
>>
>> And tools/memory-model/litmus-tests/README need to mention this
>> litmus test.
>>
>>          Thanks, Akira
>>
>> ---------------------------------------------
>> P0(int *x, int *y, atomic_t *z)
>> {
>>     int r0;
>>
>>     WRITE_ONCE(*x, 1);
>>     r0 = atomic_add_unless(z,1,5);
>>     WRITE_ONCE(*y, 1);
>> }
>>
>> P1(int *x, int *y)
>> {
>>     int r0;
>>
>>     r0 = READ_ONCE(*y);
>>     if (r0 == 1)
>>         WRITE_ONCE(*x, 2);
>> }
>>
>> exists (1:r0=1 /\ x=1)
>> ---------------------------------------------
>>
> 
> Should z also be changed from atomic_t to int?
>

No, it should not.
Such a change would make z incompatible with atomic_add_unless().

        Thanks, Akira