Received-SPF: pass (google.com: best guess record for domain of linux-kernel-owner@vger.kernel.org designates 209.132.180.67 as permitted sender) client-ip=209.132.180.67;
Date:   Thu, 13 Feb 2020 14:51:38 +0100
From:   Andrea Parri <parri.andrea@gmail.com>
To:     Boqun Feng <boqun.feng@gmail.com>
Cc:     Peter Zijlstra <peterz@infradead.org>,
        Michal Simek <michal.simek@xilinx.com>,
        linux-kernel@vger.kernel.org, monstr@monstr.eu, git@xilinx.com,
        arnd@arndb.de,
        Stefan Asserhall load and store 
        <stefan.asserhall@xilinx.com>, Will Deacon <will@kernel.org>,
        paulmck@kernel.org
Subject: Re: [PATCH 7/7] microblaze: Do atomic operations by using exclusive
 ops
Message-ID: <20200213135138.GA5843@andrea>
References: <cover.1581522136.git.michal.simek@xilinx.com>
 <ba3047649af07dadecf1a52e7d815db8f068eb24.1581522136.git.michal.simek@xilinx.com>
 <20200212155500.GB14973@hirez.programming.kicks-ass.net>
 <4b46b33e-14ad-7097-f0db-2915ac772f15@xilinx.com>
 <20200213085849.GL14897@hirez.programming.kicks-ass.net>
 <20200213113432.GF69108@debian-boqun.qqnc3lrjykvubdpftowmye0fmh.lx.internal.cloudapp.net>
 <20200213113812.GG69108@debian-boqun.qqnc3lrjykvubdpftowmye0fmh.lx.internal.cloudapp.net>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <20200213113812.GG69108@debian-boqun.qqnc3lrjykvubdpftowmye0fmh.lx.internal.cloudapp.net>
User-Agent: Mutt/1.10.1 (2018-07-13)
Sender: linux-kernel-owner@vger.kernel.org
Precedence: bulk

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@andrea:~$ 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

Thanks,
  Andrea