linux-kernel - Re: [PATCH 7/7] microblaze: Do atomic operations by using exclusive ops

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: <20200213140117.GA16550@andrea>
Date:   Thu, 13 Feb 2020 15:01:17 +0100
From:   Andrea Parri <parri.andrea@...il.com>
To:     Boqun Feng <boqun.feng@...il.com>
Cc:     Peter Zijlstra <peterz@...radead.org>,
        Michal Simek <michal.simek@...inx.com>,
        linux-kernel@...r.kernel.org, monstr@...str.eu, git@...inx.com,
        arnd@...db.de,
        Stefan Asserhall load and store 
        <stefan.asserhall@...inx.com>, Will Deacon <will@...nel.org>,
        paulmck@...nel.org, Luc Maranget <luc.maranget@...ia.fr>,
        Jade Alglave <j.alglave@....ac.uk>
Subject: Re: [PATCH 7/7] microblaze: Do atomic operations by using exclusive
 ops

On Thu, Feb 13, 2020 at 02:51:38PM +0100, Andrea Parri wrote:
> Hi,
> 
> On Thu, Feb 13, 2020 at 07:38:12PM +0800, Boqun Feng wrote:
> > (Forget to copy Andrea in the previous email)
> > 
> > Andrea, could you tell us more about how to use klitmus to generate test
> > modules from litmus test?
> 
> The basic usage is described in "tools/memory-model/README", cf., in
> particular, the section dedicated to klitmus7 and the "REQUIREMENTS"
> section.  For example, given the test,
> 
> andrea@...rea:~$ cat atomicity.litmus
> C atomicity
> 
> {
> 	atomic_t x = ATOMIC_INIT(0);
> }
> 
> P0(atomic_t *x)
> {
> 	int r0;
> 
> 	r0 = atomic_fetch_inc_relaxed(x);
> }
> 
> P1(atomic_t *x)
> {
> 	atomic_set(x, 2);
> }
> 
> exists (0:r0=0 /\ x=1)
> 
> You should be able to do:
> 
> $ mkdir mymodules
> $ klitmus7 -o mymodules atomicity.litmus
> $ cd mymodules ; make
> [...]
> 
> $ sudo sh run.sh
> Thu 13 Feb 2020 02:21:52 PM CET
> Compilation command: klitmus7 -o mymodules atomicity.litmus
> OPT=
> uname -r=5.3.0-29-generic
> 
> Test atomicity Allowed
> Histogram (2 states)
> 1963399 :>0:r0=0; x=2;
> 2036601 :>0:r0=2; x=3;
> No
> 
> Witnesses
> Positive: 0, Negative: 4000000
> Condition exists (0:r0=0 /\ x=1) is NOT validated
> Hash=11bd2c90c4ca7a8acd9ca728a3d61d5f
> Observation atomicity Never 0 4000000
> Time atomicity 0.15
> 
> Thu 13 Feb 2020 02:21:52 PM CET
> 
> Where the "Positive: 0 Negative: 4000000" indicates that, during four
> million trials, the state specified in the test's "exists" clause was
> not reached/observed (as expected).
> 
> More information are available at:
> 
>   http://diy.inria.fr/doc/litmus.html#klitmus

And I forgot to Cc: Luc and Jade, the main developers (and current
maintainers) of the tool suite in question.

Thanks,
  Andrea