[lkml]   [2020]   [Feb]   [13]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
Messages in this thread
SubjectRe: [PATCH 7/7] microblaze: Do atomic operations by using exclusive ops

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
Thu 13 Feb 2020 02:21:52 PM CET
Compilation command: klitmus7 -o mymodules atomicity.litmus
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;

Positive: 0, Negative: 4000000
Condition exists (0:r0=0 /\ x=1) is NOT validated
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:


 \ /
  Last update: 2020-02-13 14:52    [W:0.060 / U:0.056 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site