herd / herdtools7 Goto Github PK

The Herd toolsuite to deal with .cat memory models (version 7.xx)

License: Other

Shell 0.17% OCaml 73.97% C 2.20% Awk 0.01% Makefile 0.30% Python 1.53% CSS 1.12% JavaScript 1.38% HTML 1.70% Coq 4.73% ASL 1.94% Perl 0.58% Raku 0.03% TeX 10.35%

herdtools7's People

Contributors

Stargazers

Watchers

herdtools7's Issues

diy7 -eprocs <n> does not work

The following config produces only tests with 4 threads:
-arch AArch64
-safe Pod**,Rfe,Fre,Wse
-hexa true
-size 8
-eprocs 3
-num false

diyone7 produces unreachable output states

The command

% diyone7 -ua 1 -arch AArch64 "PodWRPA Amo.LdAddAL RfeLP Amo.StClrPL DMB.SYdWWLP Wse"

Produces a litmus test with an unreachable output state:

AArch64 A
"PodWRPA Amo.LdAddAL RfeLP Amo.StClrPL DMB.SYdWWLP Wse"
Generator=diyone7 (version 7.55)
Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
Com=Rf Ws
Orig=PodWRPA Amo.LdAddAL RfeLP Amo.StClrPL DMB.SYdWWLP Wse
{
0:X1=x; 0:X2=y;
1:X0=y; 1:X3=x;
}
 P0                 | P1             ;
 MOV W0,#2          | MOV W1,#2      ;
 STR W0,[X1]        | STCLRL W1,[X0] ;
 MOV W4,#1          | DMB SY         ;
 LDADDAL W4,W3,[X2] | MOV W2,#1      ;
                    | STR W2,[X3]    ;
exists
(x=2 /\ y=2 /\ 0:X3=0)

Here, y is modified by the LDADDAL in P0 and the STCLRL in P1. Regardless of the order of the LDADDAL and STCLRL, the resulting value of y is always 1:

y starts as 0, is incremented to 1 by the LDADDAL, and is unchanged by the STRCLRL
y starts as 0, is unchanged by the STRCLRL, and is incremented to 1 by the LDADDAL

I've only observed this behavior with the LDADD, LDEOR, LDSET, and LDCLR (including store variants e.g. STADD).

Some additional examples:

% diyone7 -ua 1 -arch AArch64 "PodRRAA Amo.StAdd RfiPA HatAA Amo.LdAddAL PodWWLP RfePA"

which produces

AArch64 A
"PodRRAA Amo.StAddAP RfiPA HatAA Amo.LdAddAL PodWWLP RfePA"
Generator=diyone7 (version 7.55)
Prefetch=0:x=F,0:y=T,1:y=F,1:x=W
Com=Ws Rf
Orig=PodRRAA Amo.StAddAP RfiPA HatAA Amo.LdAddAL PodWWLP RfePA
{
0:X1=x; 0:X2=y;
1:X0=y; 1:X4=x;
}
 P0            | P1                 ;
 LDAR W0,[X1]  | MOV W2,#2          ;
 MOV W3,#1     | LDADDAL W2,W1,[X0] ;
 STADD W3,[X2] | MOV W3,#1          ;
 LDAR W4,[X2]  | STR W3,[X4]        ;
exists
(y=2 /\ 0:X0=1 /\ 0:X4=1 /\ 1:X1=1)

y must be 3 because P0 atomically increments it by 1 and P1 atomically increments it by 2.

% diyone7 -ua 1 -arch AArch64 "DpAddrdW Rfi Hat Amo.StEorPL DMB.SYdWWLP Rfe"

which produces

AArch64 A
"DpAddrdW Rfi Hat Amo.StEorPL DMB.SYdWWLP Rfe"
Generator=diyone7 (version 7.55)
Prefetch=0:x=F,0:y=T,1:y=F,1:x=W
Com=Ws Rf
Orig=DpAddrdW Rfi Hat Amo.StEorPL DMB.SYdWWLP Rfe
{
0:X1=x; 0:X4=y;
1:X0=y; 1:X3=x;
}
 P0                  | P1             ;
 LDR W0,[X1]         | MOV W1,#2      ;
 EOR W2,W0,W0        | STEORL W1,[X0] ;
 MOV W3,#1           | DMB SY         ;
 STR W3,[X4,W2,SXTW] | MOV W2,#1      ;
 LDR W5,[X4]         | STR W2,[X3]    ;
exists
(y=2 /\ 0:X0=1 /\ 0:X5=1)

y must be either 1 (P0's STR occurs after P1's STEORL) or 3 (P1's STEORL occurs after P0's STR).

Unusual result of litmus testing on SC

Hi there,

I just started using herd7 tool to try out some examples given in the documentation (http://diy.inria.fr/doc/herd.html).

But on trying out the example of store buffering (SB.litmus) for Sequential Consistency, I am not getting the output as No Positive Witnesses . I have used the files provided in the documentation itself of the model and the litmus test.

Here is what I got.

Here is the sc.cat file which I downloaded from the documentation link.

I also tried it for a simple message passing example. But I am not getting the intended output of No Positive Witness.

Am I missing something here? Or have I misunderstood the output.

Thank you,
Sincerely,
jaag5678

herd7: exists clause that should be prohibited is now allowed

Hi,

Recent commit c768fc5 affected a litmus test from perfbook's CodeSamples.

C Lock-outside-across

{}

P0(int *x, int *y, spinlock_t *sp)
{
	int r1;

	WRITE_ONCE(*x, 1);
	spin_lock(sp);
	r1 = READ_ONCE(*y);
	spin_unlock(sp);
}

P1(int *x, int *y, spinlock_t *sp)
{
	int r1;

	spin_lock(sp);
	WRITE_ONCE(*y, 1);
	spin_unlock(sp);
	r1 = READ_ONCE(*x);
}

exists (0:r1=0 /\ 1:r1=0)

With herd7 7.56.2 and master branch up until commit f6de671, this litmus test
results in "Never" (in combination of linux-kernel.cfg of LKMM).
Commit c768fc5 changed the result to "Sometimes".

Can you look into this?

Note: -optace option is not specified.

Building with OCamlbuild fails

Herdtools builds fine with Dune, but breaks with Ocamlbuild:

OCaml version: 4.11.1
Ocamlbuild version: 0.14.0
Dune version: 2.7.1

Compile error of klitmus7 generated code

Hi,

Today's master (db524f6) has regression in klitmus7.
Following litmus test (of perfbook's CodeSamples) ended up in compile error:

C C-CCIRIW+o+o+o-o+o-o

{}

P0(int *x)
{
	WRITE_ONCE(*x, 1);
}

P1(int *x)
{
	WRITE_ONCE(*x, 2);
}

P2(int *x)
{
	int r1;
	int r2;

	r1 = READ_ONCE(*x);
	r2 = READ_ONCE(*x);
}

P3(int *x)
{
	int r3;
	int r4;

	r3 = READ_ONCE(*x);
	r4 = READ_ONCE(*x);
}

exists(2:r1=1 /\ 2:r2=2 /\ 3:r3=2 /\ 3:r4=1)

Compile error log from "make":

make -C /lib/modules/5.4.0-72-generic/build/ M=/home/foo/Lab/klitmus7/klitmus modules
make[1]: Entering directory '/usr/src/linux-headers-5.4.0-72-generic'
  CC [M]  /home/foo/Lab/klitmus7/klitmus/litmus000.o
/home/foo/Lab/klitmus7/klitmus/litmus000.c: In function ‘thread2’:
/home/foo/Lab/klitmus7/klitmus/litmus000.c:484:27: error: ‘ctx_t {aka struct <anonymous>}’ has no member named ‘_a’
       code2(&_a->x[_i],&_a->_a->out_2_r2[_i],&_a->_a->out_2_r1[_i]);
                           ^~
/home/foo/Lab/klitmus7/klitmus/litmus000.c:484:49: error: ‘ctx_t {aka struct <anonymous>}’ has no member named ‘_a’
       code2(&_a->x[_i],&_a->_a->out_2_r2[_i],&_a->_a->out_2_r1[_i]);
                                                 ^~
/home/foo/Lab/klitmus7/klitmus/litmus000.c: In function ‘thread3’:
/home/foo/Lab/klitmus7/klitmus/litmus000.c:518:27: error: ‘ctx_t {aka struct <anonymous>}’ has no member named ‘_a’
       code3(&_a->x[_i],&_a->_a->out_3_r4[_i],&_a->_a->out_3_r3[_i]);
                           ^~
/home/foo/Lab/klitmus7/klitmus/litmus000.c:518:49: error: ‘ctx_t {aka struct <anonymous>}’ has no member named ‘_a’
       code3(&_a->x[_i],&_a->_a->out_3_r4[_i],&_a->_a->out_3_r3[_i]);
                                                 ^~
scripts/Makefile.build:269: recipe for target '/home/foo/Lab/klitmus7/klitmus/litmus000.o' failed
make[2]: *** [/home/foo/Lab/klitmus7/klitmus/litmus000.o] Error 1
Makefile:1754: recipe for target '/home/foo/Lab/klitmus7/klitmus' failed
make[1]: *** [/home/foo/Lab/klitmus7/klitmus] Error 2
make[1]: Leaving directory '/usr/src/linux-headers-5.4.0-72-generic'
Makefile:5: recipe for target 'all' failed
make: *** [all] Error 2

It compiles successfully on the previous commit (45690d9).

This is on Ubuntu 18.04 with gcc (Ubuntu 7.5.0-3ubuntu1~18.04) 7.5.0.
uname -r: 5.4.0-72-generic

Can you look into this?

Thanks, Akira

diyone7 can produce unreachable tests with Amo and T relaxations

We're seeing an issue similar to #258, where memtag tests that use an Amo relaxation and communication relaxations annotated with T can have an "unreachable" output condition that cannot be satisfied by any ordering of events.

As an example baseline, consider

AArch64 BaselineNoT
"DMB.STdWW RfePA Amo.LdAddAL PodWWLP Coe"
Generator=diyone7 (version 7.56+02~dev)
Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
Com=Rf Co
Orig=DMB.STdWW RfePA Amo.LdAddAL PodWWLP Coe
{
0:X1=x:green; 0:X3=y:green;
1:X0=y:green; 1:X4=x:green;
}
 P0          | P1                 ;
 MOV W0,#2   | MOV W2,#2          ;
 STR W0,[X1] | LDADDAL W2,W1,[X0] ;
 DMB ST      | MOV W3,#1          ;
 MOV W2,#1   | STR W3,[X4]        ;
 STR W2,[X3] |                    ;
exists ([x]=2 /\ [y]=3 /\ 1:X1=1)

which has a correct exists clause as a result of #294. For this example, -variant memtag isn't necessary, but since it is necessary for the next examples, I've included it for consistency.

We can add a T annotation on one of the communication edges and get

AArch64 WithCoePT
"DMB.STdWWTP RfePA Amo.LdAddAL PodWWLP CoePT"
Generator=diyone7 (version 7.56+02~dev)
Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
Com=Rf Co
Orig=DMB.STdWWTP RfePA Amo.LdAddAL PodWWLP CoePT
{
0:X0=x:red; 0:X1=x:green; 0:X3=y:green;
1:X0=y:green; 1:X4=x:green;
}
 P0          | P1                 ;
 STG X0,[X1] | MOV W2,#2          ;
 DMB ST      | LDADDAL W2,W1,[X0] ;
 MOV W2,#1   | MOV W3,#1          ;
 STR W2,[X3] | STR W3,[X4]        ;
exists ([tag(x)]=:red /\ [y]=3 /\ 1:X1=1) /\ ~fault (P1,x)

which also has a correct exists clause.

However, using CoeTP produces

AArch64 WithCoeTP
"DMB.STdWWPT RfeTA Amo.LdAddAL PodWWLT CoeTP"
Generator=diyone7 (version 7.56+02~dev)
Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
Com=Rf Co
Orig=DMB.STdWWPT RfeTA Amo.LdAddAL PodWWLT CoeTP
{
0:X1=x:red; 0:X2=y:red; 0:X3=y:green;
1:X0=y:green; 1:X3=x:red; 1:X4=x:green;
}
 P0          | P1                 ;
 MOV W0,#1   | MOV W2,#1          ;
 STR W0,[X1] | LDADDAL W2,W1,[X0] ;
 DMB ST      | STG X3,[X4]        ;
 STG X2,[X3] |                    ;
exists ([x]=1 /\ [y]=2 /\ 1:X1=0) /\ ~(fault (P0,x) \/ fault (P1,y))

which has an exists clause that cannot be satisfied for any ordering of events because y is only written by the LDADDAL which will atomically update it from 0 to 1 while the exists clause expects it to be 2. For it, I would expect the exists clause to be exists ([x]=1 /\ [y]=1 /\ 1:X1=0) /\ ~(fault (P0,x) \/ fault (P1,y))

For reference, the herd7 -through all output for this example is

Test WithCoeTP Allowed
States 4
1:X1=0; [x]=1; [y]=1;  ~Fault(P1,y); ~Fault(P0,x);
1:X1=0; [x]=1; [y]=1; Fault(P0,x:red); ~Fault(P1,y);
1:X1=0; [x]=1; [y]=1; Fault(P0,x:red); Fault(P1,y:green);
1:X1=0; [x]=1; [y]=1; Fault(P1,y:green); ~Fault(P0,x);
No
Witnesses
Positive: 0 Negative: 4
Condition exists ([x]=1 /\ [y]=2 /\ 1:X1=0 /\ not (fault(P0,x) \/ fault(P1,y)))
Observation WithCoeTP Never 0 4
Time WithCoeTP 0.01
Hash=166c82f2f4caed1d5f4a38d62764ec50

This is not limited to the Coe communication, we can get this behavior with, e.g. Rfe

AArch64 WithRfeTP
"DMB.STdRWPT RfeTA Amo.LdAddAL PodWWLT RfeTP"
Generator=diyone7 (version 7.56+02~dev)
Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
Com=Rf Rf
Orig=DMB.STdRWPT RfeTA Amo.LdAddAL PodWWLT RfeTP
{
0:X0=x:red; 0:X2=y:red; 0:X3=y:green;
1:X0=y:green; 1:X3=x:red; 1:X4=x:green;
}
 P0          | P1                 ;
 LDR W1,[X0] | MOV W2,#1          ;
 DMB ST      | LDADDAL W2,W1,[X0] ;
 STG X2,[X3] | STG X3,[X4]        ;
exists ([y]=2 /\ 0:X1=0 /\ 1:X1=0) /\ ~(fault (P0,x) \/ fault (P1,y))

It appears that the Amo is important for recreating this issue. If we replace the Amo relaxation with ordinary loads and stores in the "WithCoeTP" example, we get a correct exists clause

AArch64 NoAmo
"DMB.STdWWPT RfeTA PosRWAL PodWWLT CoeTP"
Generator=diyone7 (version 7.56+02~dev)
Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
Com=Rf Co
Orig=DMB.STdWWPT RfeTA PosRWAL PodWWLT CoeTP
{
0:X1=x:red; 0:X2=y:red; 0:X3=y:green;
1:X0=y:red; 1:X3=x:red; 1:X4=x:green;
}
 P0          | P1           ;
 MOV W0,#1   | LDAR W1,[X0] ;
 STR W0,[X1] | MOV W2,#1    ;
 DMB ST      | STLR W2,[X0] ;
 STG X2,[X3] | STG X3,[X4]  ;
exists ([x]=1 /\ [y]=1 /\ 1:X1=0) /\ ~(fault (P0,x) \/ fault (P1,y))

I'm not sure why the fix in #294 isn't affecting these tests.

herd7 AArch64 LDEORAL does not simulate MTE faults correctly when in precise mode

When running the following memtag cycle through herd7 in precise mode:

AArch64 A
"DMB.LDsRRTA Amo.LdEorAL PodWRLT HatTA Amo.LdSetAL PodWRLT DMB.LDdRWTT RfeTT"
Generator=diyone7 (version 7.56+02~dev)
Prefetch=0:x=F,0:y=T,1:y=F,1:x=W
Com=Fr Rf
Orig=DMB.LDsRRTA Amo.LdEorAL PodWRLT HatTA Amo.LdSetAL PodWRLT DMB.LDdRWTT RfeTT
{
0:X1=x:red; 0:X2=x:green; 0:X6=y:green;
1:X0=y:green; 1:X4=z:green; 1:X5=x:red; 1:X6=x:green;
}
 P0                 | P1                 ;
 MOV X0,X1          | MOV W2,#1          ;
 LDG X0,[X1]        | LDSETAL W2,W1,[X0] ;
 DMB LD             | MOV X3,X4          ;
 MOV W4,#1          | LDG X3,[X4]        ;
 LDEORAL W4,W3,[X2] | DMB LD             ;
 MOV X5,X6          | STG X5,[X6]        ;
 LDG X5,[X6]        |                    ;
exists
([x]=1 /\ 0:X0=x:red /\ 0:X3=0 /\ 0:X5=y:green /\ 1:X1=0) /\ ~fault (P0,x)

You will see the following output:

$ herd7 -variant memtag,precise fault

Test A Allowed
States 3
0:X0=x:green; 0:X3=0; 0:X5=y:green; 1:X1=0; [x]=0; Fault(P0,x:green);
0:X0=x:green; 0:X3=0; 0:X5=y:green; 1:X1=0; [x]=1;  ~Fault(P0,x);
0:X0=x:red; 0:X3=0; 0:X5=y:green; 1:X1=0; [x]=0; Fault(P0,x:green);
No
Witnesses
Positive: 0 Negative: 3
Condition exists ([x]=1 /\ 0:X0=x:red /\ 0:X3=0 /\ 0:X5=y:green /\ 1:X1=0 /\ not (fault(P0,x)))
Observation A Never 0 3
Time A 0.02
Hash=cd8e99e8a415a6d8524b6f6320c57adf

This is incorrect, as having MTE synchronous (precise) faults enabled would mean that for both cases where we have a fault on P0 for x, the faulting instruction must be the LDEORAL. This would mean that move into 0:X5 that happens after the faulting instruction would never execute, and 0:X5 would stay equal to 0 and not y:green as is shown by herd7.

Substituting the LDEORAL for a LDR shows that for that test, herd is able to correctly simulate the fault on the load for that instruction, and the value of 0:X5 is indeed 0 as we'd expect for the LDEORAL test too.

AArch64 substitute
{
0:X1=x:red; 0:X2=x:green; 0:X6=y:green;
1:X0=y:green; 1:X4=z:green; 1:X5=x:red; 1:X6=x:green;
}
 P0                 | P1                 ;
 MOV X0,X1          | MOV W2,#1          ;
 LDG X0,[X1]        | LDSETAL W2,W1,[X0] ;
 DMB LD             | MOV X3,X4          ;
 MOV W4,#1          | LDG X3,[X4]        ;
 LDR W4,[X2]        | DMB LD             ;
 MOV X5,X6          | STG X5,[X6]        ;
 LDG X5,[X6]        |                    ;
exists ~(0:X3=0 /\ 0:X5=y:green /\ 1:X1=0 /\ (~fault(P0,x) /\ [x]=1 /\ (0:X0=x:red \/ 0:X0=x:green) \/ fault(P0,x) /\ [x]=0 /\ (0:X0=x:green \/ 0:X0=x:red)))

Test substitute Allowed
States 3
0:X0=x:green; 0:X3=0; 0:X5=0; 1:X1=0; [x]=0; Fault(P0,x:green);
0:X0=x:green; 0:X3=0; 0:X5=y:green; 1:X1=0; [x]=0;  ~Fault(P0,x);
0:X0=x:red; 0:X3=0; 0:X5=0; 1:X1=0; [x]=0; Fault(P0,x:green);
Ok
Witnesses
Positive: 3 Negative: 0
Condition exists (not (0:X3=0 /\ 0:X5=y:green /\ 1:X1=0 /\ (not (fault(P0,x)) /\ [x]=1 /\ (0:X0=x:red \/ 0:X0=x:green) \/ fault(P0,x) /\ [x]=0 /\ (0:X0=x:green \/ 0:X0=x:red))))
Observation RR+RW+dmb.ldsta-amo.ldeoral-polt+amo.ldsetal-poRlt-dmb.ldtt Always 3 0
Time RR+RW+dmb.ldsta-amo.ldeoral-polt+amo.ldsetal-poRlt-dmb.ldtt 0.02
Hash=68ccc0e836131b4967a12fe3b4683c1b

I have not tried any other LSE instructions in the place of the LDEORAL, but I'd assume they could well have the same issue.

catalogue/hsa all.sh and ALL.sh confuse case-insensitive filesystems

On case-insensitive filesystems (such as the default macOS one =(), the presence of catalogue/hsa/ALL.sh / catalogue/hsa/all.sh
and
catalogue/hsa/papier-tests/ALL.sh / catalogue/hsa/papier-tests/all.sh causes several problems: generally git only clones one of them at a time and constantly thinks that it has uncommitted changes changing it from the other one.

I haven't used any of the scripts/content in the catalogue directory, so I'm not sure if there are any other issues that this causes, or what the best solution would be?

Data dependencies from AMO instructions in RISCV

Apparently herd7 does not generate data-dependencies originated from the destination register of an AMO instruction in RISCV.
In this example

{
0:x6=x; 0:x8=y;
1:x6=y; 1:x8=x;
}
 P0                      | P1                      ;
 ori x5,x0,2             | lw x5,0(x6)             ;
 amoswap.w.rl x0,x5,(x6) | ori x7,x0,1             ;
 ori x7,x0,1             | amoswap.w.rl x0,x7,(x8) ;
 sw x7,0(x8)             |                         ;
exists
(x=2 /\ 1:x5=1)

I would have expected a data-dependency in the first thread (amoswap -> ori -> sw via x0 and x7) which would forbid to reorder the swap and the store, making the behaviour unobservable.

However herd7 reports that the behaviour is possible an indeed the data edge is not in the generated graph

❯ herd7 -model ~/git/herdtools7/herd/libdir/riscv.cat test.litmus -o . -show all -doshow data
Test S+porlp+poprl+NEW Allowed
States 4
1:x5=0; x=1;
1:x5=0; x=2;
1:x5=1; x=1;
1:x5=1; x=2;
Ok
Witnesses
Positive: 1 Negative: 3
Condition exists (x=2 /\ 1:x5=1)
Observation S+porlp+poprl+NEW Sometimes 1 3
Time S+porlp+poprl+NEW 0.01
Hash=6911d30c1458d70f9a9a239417914cc7

Is this really intended? I could not find anything in RISCV's documentation here and here about AMO instructions not generating data dependencies.

diyone7 produces allowed tests

I've noticed that the diyone7 generator is producing tests with an "Allowed" condition. From what I can tell, they seem to involve Amo.LdClr/Amo.StClr which have no effect if the bit they are clearing is already 0.

For example, diyone7 produces the following test for the cycle "DMB.SYdWR Amo.LdClr Rfe Amo.LdClr PodWWPL CoeLP":

AArch64 S+dmb.sy-amo.ldclr+amo.ldclr-popl
"DMB.SYdWR Amo.LdClr Rfe Amo.LdClr PodWWPL CoeLP"
Generator=diyone7 (version 7.56+02~dev)
Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
Com=Rf Co
Orig=DMB.SYdWR Amo.LdClr Rfe Amo.LdClr PodWWPL CoeLP
{
0:X1=x; 0:X2=y;
1:X0=y; 1:X4=x;
}
 P0               | P1               ;
 MOV W0,#2        | MOV W2,#2        ;
 STR W0,[X1]      | LDCLR W2,W1,[X0] ;
 DMB SY           | MOV W3,#1        ;
 MOV W4,#1        | STLR W3,[X4]     ;
 LDCLR W4,W3,[X2] |                  ;
exists
([x]=2 /\ [y]=0 /\ 0:X3=0 /\ 1:X1=0)

This test is reported as "Allowed" by herd7 because [y] is initially 0, both LDCLR instructions have no effect on the value of [y]:

Test S+dmb.sy-amo.ldclr+amo.ldclr-popl Allowed
States 2
0:X3=0; 1:X1=0; [x]=1; [y]=0;
0:X3=0; 1:X1=0; [x]=2; [y]=0;
Ok
Witnesses
Positive: 1 Negative: 2
Condition exists ([x]=2 /\ [y]=0 /\ 0:X3=0 /\ 1:X1=0)
Observation S+dmb.sy-amo.ldclr+amo.ldclr-popl Sometimes 1 2
Time S+dmb.sy-amo.ldclr+amo.ldclr-popl 0.03
Hash=8e867caf45dd964b145056a56b7c9dd7

C11 fetch_sub performs an add, not a sub

atomic_fetch_sub behaves the same as atomic_fetch_add, i.e. it performs an addition instead of a subtraction. Seems like there is a 'typo' here:

herdtools7/lib/CLexer.mll

Lines 53 to 54 in 87ac9e5

 | "atomic_fetch_add_explicit" -> ATOMIC_FETCH_EXPLICIT Op.Add 

 | "atomic_fetch_sub_explicit" -> ATOMIC_FETCH_EXPLICIT Op.Add

C11: Missing mo for nonatomic stores to atomic locations

Consider the following c11 test:

C Test
{
}
void P0(atomic_int *x) {
	*x = 1;
	int n = atomic_load_explicit(x, memory_order_relaxed);
}
exists(0:n=0)

Herd allows 0:n=0 from the following execution:

in which b reads from ix, even though ix is not a visible side effect of b.

It seems to me like there is a mo missing between ix and a, because c11_cos.cat does not consider nonatomic stores to be part of mo for atomic locations. The rc11 model works fine, but this affects all the other c11 models.

Please let me know if I have understood this correctly, and if this is something you consider worth fixing.
Thanks

[Minor] Some annotations missing

Hello !

I noticed some unlisted annotations when running:
diy7 -arch AArch64 -show annotations
X.w0 X.h0 X.h2 XL.w0 XL.h0 XL.h2 XA.w0 XA.h0 XA.h2 XAL.w0 XAL.h0 XAL.h2 L.w0 L.h0 L.h2 Q.w0 Q.h0 Q.h2 A.w0 A.h0 A.h2 N1.w0 N1.h0 N1.h2 N2.w0 N2.h0 N2.h2 N3.w0 N3.h0 N3.h2 N4.w0 N4.h0 N4.h2 w0 h0 h2 X XL XA XAL L Q A N1 N2 N3 N4

More specifically, the annotation 'T' (meaning "Tag"), which I found in non-mixed MTE litmus tests for AArch64, is not listed. The same goes for the 'P' (meaning "Plain") annotation.
These are seen, for example, in: catalogue/aarch64-MTE/tests/MP+dmb.stPT+addr.litmus

Also, when looking at examples such as:

catalogue/aarch64-mixed/tests/MP+dmb.syb0b1+datab1b1-rfib1h0.litmus
catalogue/aarch64-mixed/tests/MP+dmb.syw0w4+dataw4w4-rfiw4q0.litmus
we can see that there are b0, b1 (from the first litmus test), and w4 and q0 (from the second one) missing too.

Just posting it here so this observation is known to you guys.
Have a good day!

aarch64-v07 is stronger than aarch64-v06

#331 claimed the change from v6 to v7 is a relaxation of the model. However, this test fails with v6 and passes with v7 (tested on herd7 web):

AArch64 lse-atomic-al-ops-are-not-fully-ordered
""
{
0:X1=x; 0:X3=y;
1:X1=x; 1:X3=y;
}
  P0                   | P1                  ;
  MOV X0, #1           | MOV X0, #1          ;
  LDSETAL X0, X2, [X1] | LDSETAL X0, X2, [X3];
  LDR X4, [X3]         | LDR X4, [X1]        ;
exists (0:X4=0 /\ 1:X4=0)

Either something was made stronger in v7, or there's a bug somewhere. @jalglave

Misleading error message for unimplemented instructions

Consider the following example used with the aarch64.cat model:

{
0:X1=x; 0:X3=y;
1:X1=y; 1:X3=x;
}
 P0                     | P1          ;
 STLXP W0, X1, X2, [X3] |             ;

exists (0:X0=1)

herd7 will complain because the STLXP instruction is not implemented, but the error message given is:
File "unknown-instr.litmus", line 7, characters 7-9: unexpected 'W0' (in prog) (User error)

If possible, it would improve usability in this scenario if the tool could report "Unrecognized statement 'STLXP'" or something like that instead.

Error using aarch64.cat - unbound var: DMB.ISH

Hi! After running herd7 -cat aarch64.cat 2+2W.litmus with the actual master (commit 1281ddc), I get the following error:

File "..../share/herdtools7/herd/aarch64.cat", line 74, characters 15-22: unbound var: DMB.ISH

Any advise on how to solve it?
Thanks!

[litmus7] Possible bug with the implies (=>) operator?

Consider this litmus test. Part of the output I am getting is as follows:

Histogram (3 states)
499997:>1:X1=0; 1:X2=0;
1     *>1:X1=10; 1:X2=0;
500002:>1:X1=10; 1:X2=10;
No

Witnesses
Positive: 999999, Negative: 1
Condition forall (1:X2=10 => 1:X1=10) is NOT validated

However, if I change the condition into an equivalent one that does not use the implies operator (like this), I am getting the following output:

Histogram (3 states)
501946:>1:X1=0; 1:X2=0;
7878  :>1:X1=10; 1:X2=0;
490176:>1:X1=10; 1:X2=10;
Ok

Witnesses
Positive: 1000000, Negative: 0
Condition forall (not (1:X2=10) \/ 1:X1=10) is validated

Given that 1:X2 = 10 => 1:X1 = 10 and not (1:X2=10) \/ 1:X1=10 are equivalent conditions (unless I am in the wrong 😅), shouldn't the litmus test produce Condition <FOO> is validated in both cases?

FYI, this is happening on master (i.e. at commit a82e652 at the time of reporting this).

option to extract litmus test as AST

Is there any way to extract a parsed litmus test as an AST in some easy-to-parse format (sexp, JSON, etc)?

Faults are not lexed by mcompare

Observed on version 7.56+02

With the following litmus test:

AArch64 Armv8-memtag
Orig=PodWRPA Amo.SwpAL RfeLP DMB.SYdRWPT CoeTP
{
0:X1=x:red; 0:X2=y:green;
1:X1=y:green; 1:X2=x:red; 1:X3=x:green;
}
 P0               | P1          ;
 MOV W0,#1        | LDR W0,[X1] ;
 STR W0,[X1]      | DMB SY      ;
 MOV W4,#1        | STG X2,[X3] ;
 SWPAL W4,W3,[X2] |             ;
exists (0:X3=0 /\ 1:X0=1) /\ ~fault(P0,x)

herd7 outputs:

Test Armv8-memtag Allowed
States 3
0:X3=0; 1:X0=0;
0:X3=0; 1:X0=0; Fault(P0,x:red);
0:X3=0; 1:X0=1; Fault(P0,x:red);
No
Witnesses
Positive: 0 Negative: 3
Condition exists (0:X3=0 /\ 1:X0=1 /\ not (fault(P0,x)))
Observation Armv8-memtag Never 0 3
Time Armv8-memtag 0.08
Hash=fb94969c809eecdc7b5a41d38c9ec202

The previous output is stored in out.log. Doing mcompare7 out.log out.log gives:

File "out.log", line 4, character 15: Lex error pline

NB: when manually removing both Fault(P0,x:red); from out.log, mcompare7 executes correctly, not having any problem with fault(P0,x) in the existence condition.

Herdtools does not build on 32-bit systems

Trying to build herdtools7 on a Raspberry Pi running Raspbian Buster 32-bit fails with:

% make
sh ./dune-build.sh $HOME
+ ./version-gen.sh /home/eth
+ dune build --profile release @all
File "lib/symbConstant.ml", line 37, characters 45-56:
Error: Integer literal exceeds the range of representable integers of type int
File "lib/symbValue.ml", line 115, characters 21-32:
Error: Integer literal exceeds the range of representable integers of type int
make: *** [Makefile:32: build] Error 1

This seems to be because the size of int is dependent on machine architecture, and the bit-manipulation in symbConstant.ml assumes a 64-bit architecture.

make test fails with Python 3.

My machine uses python 3.9.1, which causes this error with make test:

sh ./dune-build.sh $HOME
+ ./version-gen.sh /home/brad
+ dune build --profile release @all
Done: 4798/4800 (jobs: 1)
dune runtest --profile=release
  shelf_test alias internal/lib/tests/runtest (exit 2)
(cd _build/default/internal/lib/tests && ./shelf_test.exe)
Traceback (most recent call last):
  File "<stdin>", line 4, in <module>
NameError: name 'execfile' is not defined
Failed Shelf.of_file reads simple valid files: raised exception
Fatal error: exception Command.Error("Process returned error code 1")
Done: 1138/1141 (jobs: 1)make: *** [Makefile:78: dune-test] Error 1

It also fails in our CI running Python 2.7.

Python 3.9.1 can be supported by changing the execfile call (line 66 internal/lib/shelf.ml) to:

    Printf.fprintf chan "exec(open(%s).read(), m)\n" (Filename.quote (Filename.basename path)) ;

Note that execfile was removed in Python 3.3 so I'm not sure which Python version this is targetting?
Perhaps the targeted Python version should be documented in install.md?

Keywords in comment blocks cause parser errors

Consider the following example used with the aarch64.cat model:

AArch64 MP
{
0:X1=x; 0:X3=y;
1:X1=y; 1:X3=x;
}
 P0          | P1          ;
 MOV W0,#1   | LDR W0,[X1] ;
 STR W0,[X1] | LDR W2,[X3] ; (* I like the word observed *)
 MOV W2,#1   |             ;
 STR W2,[X3] |             ;

exists (1:X0=1 /\ 1:X2=0)

Trying to run this litmus test will return the following error:

% herd7 -model aarch64.cat keyword-comment.litmus
Warning: File "keyword-comment.litmus", line 8, character 48: Lex error eof in skip_comment (in prog) (User error)

Removing the word 'observed' from inside the comment block resolves the issue. This seems like a priority error in the parser.

[herd-www] aarch64-MTE cat file looks to be out of date on web interface

The aarch64-MTE.cat file provided by default for the aarch64-MTE profile includes an out of date cat file by default.

This is missing a couple of changes that went back into herd/libdir/aarch64.cat recently.

There may well be other profile cat files which are out of date, I have not personally checked.

This is resulting in the following MTE test showing as allowed, when it looks like it should actually be forbidden:

AArch64 Test
"Amo.LdEorAL PodWWLP CoePT DMB.SYdWRTQ HatQA"
Generator=diyone7 (version 7.56+02~dev)
Prefetch=0:x=F,0:y=W,1:y=F,1:x=T
Com=Co Fr
Orig=Amo.LdEorAL PodWWLP CoePT DMB.SYdWRTQ HatQA
{
0:X0=x:green; 0:X4=y:green;
1:X0=y:red; 1:X1=y:green; 1:X2=x:green;
}
 P0                 | P1            ;
 MOV W2,#1          | STG X0,[X1]   ;
 LDEORAL W2,W1,[X0] | DMB SY        ;
 MOV W3,#1          | LDAPR W3,[X2] ;
 STR W3,[X4]        |               ;
exists ([tag(y)]=:red /\ 0:X1=0 /\ 1:X3=0) /\ ~fault (P0,y)

How is "klitmus7 -carch PPC" supposed to work?

Hi,
I tried the "-carch PPC" option to klitmus7, but unable to generate proper code for PowerPC (ppc64le).

By manually replacing the code (for x86) in generated code:

inline static tb_t read_timebase(void) {
  uint32_t a,d; ;
  asm __volatile__ ("rdtsc" : "=a" (a), "=d" (d)) ;
  return ((tb_t)a) | (((tb_t)d)<<32);
}

with the one found in litmus/libdir/_ppc/timebase64.c:

inline static tb_t read_timebase(void) {
  tb_t r;
  asm __volatile__ ("mftb %[r1]" :[r1] "=r" (r) : : "memory");
  return r;
}

, "make" on ppc64le succeeds and the kernel module runs as expected.

How does the "-carch" option supposed to work?

Thanks, Akira

run_built_binary fails on linux

Line 29 makes a call to stat using -f. On Linux, this displays file system status, so the following error occurs:

make test                                                                                                                   

...

internal/run_built_binary herd_catalogue_regression_test \
	-herd-path _build/install/default/bin/herd7 \
	-libdir-path herd/libdir \
	-kinds-dir catalogue/aarch64/kinds \
	-shelf-path catalogue/aarch64/shelf.py \
	test
stat: cannot read file system information for '%m %N': No such file or directory
internal/run_built_binary: line 45: Total:: command not found
make: *** [Makefile:110: test] Error 127

I believe the option is supposed to be for formatting, so perhaps --format is preferred?

The man page is available here.

Once I apply this fix, the script still fails, this time with:

internal/run_built_binary herd_catalogue_regression_test \
	-herd-path _build/install/default/bin/herd7 \
	-libdir-path herd/libdir \
	-kinds-dir catalogue/aarch64/kinds \
	-shelf-path catalogue/aarch64/shelf.py \
	test
internal/run_built_binary: line 45: '/home/brad/gdp/repo/_build/default/internal/herd_catalogue_regression_test.exe': No such file or directory
make: *** [Makefile:110: test] Error 127

This file does exist, but apostrophes are not stripped from around the filename, so it cannot find the file.
I can make the test pass by changing line 45 to:

command="$(most_recent ${paths} | xargs) $@"
$command

I'm not the best with Bash, so perhaps there is a better way.

herd7: Fatal error: exception Stack overflow

Steps to reproduce

$ diyone7 -arch AArch64 "Rmw DMB.SYdWRPA RmwAL RfeLA RmwAL DMB.SYdWRLP RmwPL RfeLP" | tee test.litmus
AArch64 A
"LxSx DMB.SYdWRPA LxSxAL RfeLA LxSxAL DMB.SYdWRLP LxSxPL RfeLP"
Generator=diyone7 (version 7.56+02~dev)
Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
Com=Rf Rf
Orig=LxSx DMB.SYdWRPA LxSxAL RfeLA LxSxAL DMB.SYdWRLP LxSxPL RfeLP
{
0:X0=x; 0:X4=y;
1:X0=y; 1:X4=x;
}
 P0               | P1               ;
 MOV W2,#2        | MOV W2,#2        ;
 Loop00:          | Loop02:          ;
 LDXR W1,[X0]     | LDAXR W1,[X0]    ;
 STXR W3,W2,[X0]  | STLXR W3,W2,[X0] ;
 CBNZ W3,Loop00   | CBNZ W3,Loop02   ;
 DMB SY           | DMB SY           ;
 MOV W6,#1        | MOV W6,#1        ;
 Loop01:          | Loop03:          ;
 LDAXR W5,[X4]    | LDXR W5,[X4]     ;
 STLXR W3,W6,[X4] | STLXR W3,W6,[X4] ;
 CBNZ W3,Loop01   | CBNZ W3,Loop03   ;
exists (x=2 /\ y=2 /\ 0:X1=1 /\ 0:X5=0 /\ 1:X1=1 /\ 1:X5=0)
$ herd7 test.litmus 

Fatal: File "test.litmus" Adios
Fatal error: exception Stack overflow

Cannot reconstruct PTW test from the cycle (exists clauses are different)

I was given a PTW test (I think it was previously generated) and I cannot reconstruct it from the cycle.
Original test

AArch64 2+2W+popteoap-[dsb.ish]-[tlbi]-[dsb.ish]-[isb]+popteoapteva-[dsb.ish]-[tlbi]-[dsb.ish]-[isb]
"PodWWPteOAP DSB.ISH TLBI DSB.ISH ISB CoePPteOA PodWWPteOAPteVA DSB.ISH TLBI DSB.ISH ISB CoePteVAPteOA"
variant=precise
Cycle=ISB CoePPteOA PodWWPteOAPteVA DSB.ISH TLBI DSB.ISH ISB CoePteVAPteOA PodWWPteOAP DSB.ISH TLBI DSB.ISH
Relax=PteOA PteVA
Safe=Coe [PodWW,DSB.ISH,TLBI,DSB.ISH,ISB]
Generator=diy7 (version 7.56+02~dev)
Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
Com=Co Co
Orig=PodWWPteOAP DSB.ISH TLBI DSB.ISH ISB CoePPteOA PodWWPteOAPteVA DSB.ISH TLBI DSB.ISH ISB CoePteVAPteOA
{ int y=0; int x=4;
0:X0=PTE(x); 0:X1=(oa:PA(y), valid:0); 0:X3=y;
1:X0=PTE(y); 1:X1=(oa:PA(x)); 1:X2=PTE(x); 1:X3=(oa:PA(x), valid:0); 1:X4=x;
}
 P0              | P1              ;
 STR X1,[X0]     | STR X1,[X0]     ;
 DSB ISH         | DSB ISH         ;
 LSR X4,X3,#12   | LSR X5,X4,#12   ;
 TLBI VAAE1IS,X4 | TLBI VAAE1IS,X5 ;
 DSB ISH         | DSB ISH         ;
 ISB             | ISB             ;
 MOV W2,#1       | STR X3,[X2]     ;
 STR W2,[X3]     |                 ;
exists [PTE(x)]=(oa:PA(y), valid:0) /\ [y]=1 /\ ~fault(P0,y) /\ ~fault(P1,x)

And this is what I get from diyone7 for given cycle

$ diyone7 -arch AArch64 -variant kvm "PodWWPteOAP DSB.ISH TLBI DSB.ISH ISB CoePPteOA PodWWPteOAPteVA DSB.ISH TLBI DSB.ISH ISB CoePteVAPteOA"
AArch64 A
"PodWWPteOAP DSB.ISH TLBI DSB.ISH ISB CoePPteOA PodWWPteOAPteVA DSB.ISH TLBI DSB.ISH ISB CoePteVAPteOA"
Generator=diyone7 (version 7.56+02~dev)
Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
Com=Co Co
Orig=PodWWPteOAP DSB.ISH TLBI DSB.ISH ISB CoePPteOA PodWWPteOAPteVA DSB.ISH TLBI DSB.ISH ISB CoePteVAPteOA
{ int y=0; int x=4;
0:X0=PTE(x); 0:X1=(oa:PA(y), valid:0); 0:X3=y;
1:X0=PTE(y); 1:X1=(oa:PA(x)); 1:X2=PTE(x); 1:X3=(oa:PA(x), valid:0); 1:X4=x;
}
 P0              | P1              ;
 STR X1,[X0]     | STR X1,[X0]     ;
 DSB ISH         | DSB ISH         ;
 LSR X4,X3,#12   | LSR X5,X4,#12   ;
 TLBI VAAE1IS,X4 | TLBI VAAE1IS,X5 ;
 DSB ISH         | DSB ISH         ;
 ISB             | ISB             ;
 MOV W2,#1       | STR X3,[X2]     ;
 STR W2,[X3]     |                 ;
locations [fault (P0,y); fault (P1,x);]
exists ([PTE(x)]=(oa:PA(y), valid:0))

As you can see exists clause is different.

I suspect that it might be related to variant=precise in original test and I might need to invoke diyone7 somehow different. Any ideas what I've been missing?

Thanks!

Herd does not build with OCamlbuild

PR #84 introduced a new library dependency, Stdint. The OCamlbuild script was not updated to match, and now Herd does not build with OCamlbuild.

Litmus generated scripts do not have shebangs

This can cause issues when not using bash.

This issue can be fixed by adding a shebang to the top of comp.sh and run.sh.

Soundness issue with C atomic_compare_exchange_strong

The following test case

C casrot/3

{ [x] = 0; [zero] = 0; [one] = 1; [two] = 2;}

P0 (atomic_int *x, volatile int *zero)
{
        int r1 = atomic_compare_exchange_strong_explicit(x, zero, 1, memory_order_relaxed,
                                                                     memory_order_relaxed);
}

P1 (atomic_int *x, volatile int *one)
{
        int r2 = atomic_compare_exchange_strong_explicit(x, one, 2, memory_order_relaxed,
                                                                    memory_order_relaxed);
}

P2 (atomic_int *x, volatile int *two)
{
        int r3 = atomic_compare_exchange_strong_explicit(x, two, 3, memory_order_relaxed,
                                                                    memory_order_relaxed);
}

exists
(  zero=0 /\ one=1 /\ two=1 )

run with the empty cat model

"empty" withinit

generates 3 executions, none of which satisfies the postcondition.

The execution where the CASes of P0 and P1 succeed and the CAS of P2 reads from the CAS of P0 (and fails) is, however, consistent (even taking the C++11 axioms into account).

An example for RC11 litmus test

Could you please provide an example on how to write litmus test for RC11 memory model?
Trying to run any test included in doc/ folder, I get following error:

$ herd7 -c11 -statelessrc11 true doc/tst-arm/LB.litmus 
File "doc/tst-arm/LB.litmus": annotation RMW not found

How should I define/include this relation and what is a syntax for RC11 tests in general?

can't use affnity

I tried to run litmus7 with -p option, but some case didn't work (some did, same enviorment).
I also tried to remove all preamble, only left the init part and test part. Still not working. Does the affinity relies on anything I missed? Thanks.

klitmus7 regression since KVM branch merge

C flavour of litmus tests stopped working.
old-master works fine.

A simple C flavour litmus test:

C C-2+2W+o-o+o-o

{}

P0(int *x0, int *x1)
{
	WRITE_ONCE(*x0, 1);
	WRITE_ONCE(*x1, 2);
}

P1(int *x0, int *x1)
{
	WRITE_ONCE(*x1, 1);
	WRITE_ONCE(*x0, 2);
}

exists (x0=1 /\ x1=1)

ends up in the error:

klitmus7 -o /tmp C-2+2W+o-o+o-o.litmus File "C-2+2W+o-o+o-o.litmus" exception File "litmus/CArch_litmus.ml", line 75, characters 27-33: Assertion failed Fatal error: exception File "litmus/CArch_litmus.ml", line 75, characters 27-33: Assertion failed

Handling "atomic_compare_exchange_strong_explicit" in C11

Hi,

I was using herd7 (7.43, installed via OPAM) to run against the C11 litmus from https://github.com/nchong/c11popl15/blob/master/tests/a2.litmus:

C a2
{ [x] = 0; [y] = 0; [z] = 0; }

P0 (atomic_int* x, atomic_int* y, atomic_int *z) {
  int r0 = atomic_load_explicit(y, memory_order_relaxed);
  int r1 = atomic_compare_exchange_strong_explicit(x, z, 1, memory_order_release, memory_order_relaxed);
}

P1 (atomic_int* x, volatile int* y) {
  int r2 = atomic_load_explicit(x, memory_order_acquire);
  if (r2) {
    *y = 1;
  }
}

But herd7 complains:

line 6, characters 11-50: unexpected 'atomic_compare_exchange_strong_explicit' (in prog)

It seems "atomic_load_explicit" (and also "atomic_store_explicit" according to other tests) are recognized, but not "atomic_compare_exchange_strong_explicit".

I tried with latest version in master branch up to now, it complains the message as well. I also tried with old version herd in https://github.com/herd/herdtools, and it can successfully finish the run there.

So is herd7 indeed missing the part for "atomic_compare_exchange_strong_explicit" at the moment?
Thanks.

Litmus operating system check doesn't recognise macOS correctly

The check for macOS in litmus/runUtils.ml does so by testing the presence of the file /mach_kernel. This file hasn't existed since OSX Yosemite and as such the check erroneously reports modern macOS as Linux. This then leads to:

Fatal error: open_in failed: /proc/cpuinfo: No such file or directory

I have a quick-ish fix that replaces the file test with a scrape on the output of uname -s, which I'll post as a PRQ, but there might be a more principled way of doing it that I hadn't thought of!

Parameter evaluation ordering for C11

I'm trying to understand why herd gives different results using c11_partialSC.cat on the two litmus tests below

❯ cat litmus/C11/auto/linearisation.litmus
C linearisation
{ [x] = 0; [y] = 0; [w] = 0; [z] = 0; }

P0 (atomic_int* w, atomic_int* x, volatile int* y) {
  int t = atomic_load_explicit(x, memory_order_acquire) + *y;

  if (t == 2) {
    atomic_store_explicit(w, 1, memory_order_release);
  }
}

P1 (atomic_int* w, atomic_int* z) {
  int r0 = atomic_load_explicit(w, memory_order_relaxed);
  if (r0) {
    atomic_store_explicit(z, 1, memory_order_relaxed);
  }
}

P2 (atomic_int* x, volatile int* y, atomic_int* z) {
  int r1 = atomic_load_explicit(z, memory_order_relaxed);
  if (r1) {
    *y = 1;
    atomic_store_explicit(x, 1, memory_order_release);
  }
}

exists (0:t=2 /\ w=1 /\ x=1 /\ y=1 /\ z=1)
❯ herd7 -c11 -model ~/git/herdtools7/herd/libdir/c11_partialSC.cat litmus/C11/auto/linearisation.litmus
Test linearisation Allowed
States 1
0:t=0; w=0; x=0; y=0; z=0;
No
Witnesses
Positive: 0 Negative: 1
Condition exists (0:t=2 /\ w=1 /\ x=1 /\ y=1 /\ z=1)
Observation linearisation Never 0 1
Time linearisation 0.00
Hash=34cc828a9b87232ac12e05b762c4acfc

❯ cat litmus/C11/auto/linearisation2.litmus
C linearisation2
{ [x] = 0; [y] = 0; [w] = 0; [z] = 0; }

P0 (atomic_int* w, atomic_int* x, volatile int* y) {
  int t = atomic_load_explicit(x, memory_order_acquire);
  t = t + *y;
  if (t == 2) {
    atomic_store_explicit(w, 1, memory_order_release);
  }
}

P1 (atomic_int* w, atomic_int* z) {
  int r0 = atomic_load_explicit(w, memory_order_relaxed);
  if (r0) {
    atomic_store_explicit(z, 1, memory_order_relaxed);
  }
}

P2 (atomic_int* x, volatile int* y, atomic_int* z) {
  int r1 = atomic_load_explicit(z, memory_order_relaxed);
  if (r1) {
    *y = 1;
    atomic_store_explicit(x, 1, memory_order_release);
  }
}

exists (0:t=2 /\ w=1 /\ x=1 /\ y=1 /\ z=1)
❯ herd7 -c11 -model ~/git/herdtools7/herd/libdir/c11_partialSC.cat litmus/C11/auto/linearisation2.litmus
Test linearisation2 Allowed
States 2
0:t=0; w=0; x=0; y=0; z=0;
0:t=2; w=1; x=1; y=1; z=1;
Ok
Witnesses
Positive: 1 Negative: 1
Condition exists (0:t=2 /\ w=1 /\ x=1 /\ y=1 /\ z=1)
Observation linearisation2 Sometimes 1 1
Time linearisation2 0.00
Hash=a053a418e2b4bb0eaa0d717995884b30

I suspect that this is related to the fact that C11 does not specify the evaluation ordering for the parameters of a function (here +). However, even with that in mind, I cannot really understand why the first program has less executions than the second one.

diy doen't generate existence conditions for memory locations with memtag

Result of diyone7 -arch AArch64 Rfe PodRW Coe PodWW:

Orig=Rfe PodRW Coe PodWW
{
0:X1=x; 0:X3=y;
1:X1=y; 1:X3=x;
}
 P0          | P1          ;
 LDR W0,[X1] | MOV W0,#2   ;
 MOV W2,#1   | STR W0,[X1] ;
 STR W2,[X3] | MOV W2,#1   ;
             | STR W2,[X3] ;
exists (y=2 /\ 0:X0=1)

Result of diyone7 -arch AArch64 Rfe PodRW CoeTT PodWW -variant memtag:

Orig=Rfe PodRWPT CoeTT PodWWTP
{
0:X1=x:green; 0:X2=y:red; 0:X3=y:green;
1:X0=y:blue; 1:X1=y:red; 1:X3=x:green;
}
 P0          | P1          ;
 LDR W0,[X1] | STG X0,[X1] ;
 STG X2,[X3] | MOV W2,#1   ;
             | STR W2,[X3] ;
exists (0:X0=1)

The existence condition of the second litmus should mention that "y" is expected to be blue.

[klitmus] Linux v5.17 stopped exporting do_exit()

Hi,

I could have reported this issue earlier, but noticed it after updating the distro kernel packages
on a Fedora 35 machine.

Now, building kernel modules generated by klitmus7 ends up in errors from modpost:

[...]
ERROR: modpost: "do_exit" [/<path to klitmus7 output>/litmus002.ko] undefined!
ERROR: modpost: "do_exit" [/<path to klitmus7 output>/litmus001.ko] undefined!
ERROR: modpost: "do_exit" [/<path to klitmus7 output>/litmus000.ko] undefined!

This is because Linux kernel no longer exports do_exit(). The change were done by
one of the changes pulled into mainline by merge commit 35ce8ae9ae2
("Merge branch 'signal-for-v5.17' of git://git.kernel.org/pub/scm/linux/kernel/git/ebiederm/user-namespace")

I've not figured out which exported API to use instead, though.

All I can do for now is to report the issue.

RC11 definition

I'm trying to understand the following two definitions from this file

let myrmw = [RMW] | rmw
let rb = (rf^-1; mo) \ id

AFAIK herd models RMW instructions as a pair of events, however the definitions above suggest there might be cases where those instructions are modeled by a single event which is both a read and a write (otherwise the \ id would not make any sense).

diy: missing existence condition with Pos

Observed on version 7.56+02

With the following litmus test:

AArch64 A
Orig=PodWW Rfe PodRR PosRR Fre
{
0:X1=x; 0:X3=y;
1:X1=y; 1:X3=x;
}
 P0          | P1          ;
 MOV W0,#1   | LDR W0,[X1] ;
 STR W0,[X1] | LDR W2,[X3] ;
 MOV W2,#1   | LDR W4,[X3] ;
 STR W2,[X3] |             ;
exists (1:X0=1 /\ 1:X4=0)

The state of 1:X2 (expected to be 0) doesn't appear in the existence condition, probably because the two reads resulting in 1:X2 and 1:X4 are from the same memory location. I think it should be there, because the values read can be different.

It also shows with -variant memtag, even when reading from different banks:

AArch64 B
Orig=PodWWTT RfeTT PodRRTT PosRRTP FrePT
{
0:X0=x:red; 0:X1=x:green; 0:X2=y:red; 0:X3=y:green;
1:X1=y:red; 1:X3=x:green;
}
 P0          | P1          ;
 STG X0,[X1] | MOV X0,X1   ;
 STG X2,[X3] | LDG X0,[X1] ;
             | MOV X2,X3   ;
             | LDG X2,[X3] ;
             | LDR W4,[X3] ;
exists (1:X0=y:red /\ 1:X4=0) /\ ~fault(P1,x)

diy7 produces allowed cycles with Hat

I'm observing some Allowed cycles being generated by diy7. They all seem to contain the Hat relaxation and have a "split" ordering on one of the threads such that the first effect is ordered before the last effect and the first effect is ordered before some intermediate effect but the intermediate effect isn't ordered before the last effect.

For example, with -safe 'PodRRAP Hat Rfe' -relax '[DpAddrsW,PodWW]', diy7 produces the cycle "PodRRAP Hat DpAddrsW PodWW RfePA" which corresponds to this test:

AArch64 RR+RW+poap+addrsW-po
"PodRRAP Hat DpAddrsW PodWW RfePA"
Generator=diyone7 (version 7.56+02~dev)
Prefetch=0:x=F,0:y=T,1:y=F,1:x=W
Com=Fr Rf
Orig=PodRRAP Hat DpAddrsW PodWW RfePA
{
0:X0=x; 0:X2=y;
1:X0=y; 1:X5=x;
}
 P0           | P1                  ;
 LDAR W1,[X0] | LDR W1,[X0]         ;
 LDR W3,[X2]  | EOR W2,W1,W1        ;
              | MOV W3,#1           ;
              | STR W3,[X0,W2,SXTW] ;
              | MOV W4,#1           ;
              | STR W4,[X5]         ;
exists
(0:X1=1 /\ 0:X3=0 /\ 1:X1=0)

On P0, the LDAR is barrier-ordered-before the LDR. On P1, the LDR W1,[X0] is dependency-ordered-before the STR W3,[X0,W2,SXTW] (by means of an address dependency) and the LDR W1,[X0] is dependency-ordered-before the STR W4,[X5] (which is a write in program order following an address dependency, or addr; po; [W]). However, there is no ordering between the STR W3,[X0,W2,SXTW] and the STR W4,[X5].

In terms of the relaxations, PodRRAP, Hat, and Rfe all provide order and [DpAddrsW,PodWW] provides order between the first and last memory effect but not between the intermediate write and the last memory effect. To address this, I believe that communication (specifically Hat) must be between the first or last memory effect of a relaxation.

Another litmus test that runs on old herd but fails on herd7

Hi,

While trying multiple C11 tests, I found another test from http://multicore.doc.ic.ac.uk/overhauling/C11/cppmem_unsequencedrace.litmus:

C cppmem_unsequenced_race

{
[x] = 2;
[y] = 0;
}

// This litmus test is ported from an example distributed
// with the CppMem tool. Original is available online at:
// http://svr-pes20-cppmem.cl.cam.ac.uk/cppmem/index.html

P0 (int* x, int* y) {
  *y = (*x == (*x = 3));
}

exists
()

which will complain:

line 13, characters 18-19: unexpected '=' (in prog)

in herd7 but runs with old version herd.

Tracking Issue for regression-testing the Catalogue

This issue exists to track & log PRs for implementing regression-testing of the Catalogue. This Issue will link to those PRs, and those PRs will link to this Issue.

I am currently doing this work, but want to split it into multiple PRs instead of a single giant PR.

Multiple definition error

Hello,

I just tried to compile it and received this error:

File "herd/archExtra_herd.ml", line 82, characters 2-42:
Error: Multiple definition of the type name loc_global.
Names must be unique in a given structure or signature.

It was working before the last updates. Thanks.

OS: Kubuntu 19.10
GNU Make 4.2.1

Commands of herdtools7 7.56.1 doesn't print ther version

After installing herdtools7 by opam install, running herd7 -version prints only:

, Rev: exported

Looking at commit f544fd4, I suspect fields of name: "herdtools7" and
version: "7.56.1" were removed by accident.

Can you do another release with this issue fixed?
I have no idea if it can be 7.56.1 or needs to be 7.56.2.

Soundness issue with an AArch64 litmus test

Hello,

I have the following variation of message passing, where the first read of the second thread is performed N times (see attached).

While I would expect it to have N + 1 executions, herd only reports 3, for different values of N. Is this a bug or there is something wrong with the test case?

Thank you,
Michalis

Struggling to understand intention of (generated?) PTW litmus test

I was given a PTW test (I think it was previously generated) and I struggle to understand what aspect of PTW it is supposed to check.

AArch64 2+2W+popteoap-[dsb.ish]-[tlbi]-[dsb.ish]-[isb]+popteoapteaf-[dsb.ish]-[tlbi]-[dsb.ish]-[isb]
"PodWWPteOAP DSB.ISH TLBI DSB.ISH ISB CoePPteOA PodWWPteOAPteAF DSB.ISH TLBI DSB.ISH ISB CoePteAFPteOA"
variant=precise
Cycle=ISB CoePPteOA PodWWPteOAPteAF DSB.ISH TLBI DSB.ISH ISB CoePteAFPteOA PodWWPteOAP DSB.ISH TLBI DSB.ISH
Relax=PteAF PteOA
Safe=Coe [PodWW,DSB.ISH,TLBI,DSB.ISH,ISB]
Generator=diy7 (version 7.56+02~dev)
Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
Com=Co Co
Orig=PodWWPteOAP DSB.ISH TLBI DSB.ISH ISB CoePPteOA PodWWPteOAPteAF DSB.ISH TLBI DSB.ISH ISB CoePteAFPteOA
{ int y=0; int x=4;
0:X0=PTE(x); 0:X1=(oa:PA(y), af:0); 0:X3=y;
1:X0=PTE(y); 1:X1=(oa:PA(x)); 1:X2=PTE(x); 1:X3=(oa:PA(x), af:0); 1:X4=x;
}
 P0              | P1              ;
 STR X1,[X0]     | STR X1,[X0]     ;
 DSB ISH         | DSB ISH         ;
 LSR X4,X3,#12   | LSR X5,X4,#12   ;
 TLBI VAAE1IS,X4 | TLBI VAAE1IS,X5 ;
 DSB ISH         | DSB ISH         ;
 ISB             | ISB             ;
 MOV W2,#1       | STR X3,[X2]     ;
 STR W2,[X3]     |                 ;
 exists [PTE(x)]=(oa:PA(y), af:0) /\ [y]=1 /\ ~fault(P0,y) /\ ~fault(P1,x)

IIUC, fault(P1,x) is unreachable since there is no access to x, fault(P0, y) is not possible because PTE(y) always hold valid translation. So it looks like PTE are used as shared locations, at least if I reduce test to

AArch64 Reduced
{ int y=0; int x=4;
0:X0=PTE(x); 0:X1=(oa:PA(y), af:0); 0:X3=y;
1:X0=PTE(y); 1:X1=(oa:PA(x)); 1:X2=PTE(x); 1:X3=(oa:PA(x), af:0); 1:X4=x;
}
 P0              | P1              ;
 STR X1,[X0]     | STR X1,[X0]     ;
 DSB ISH         | DSB ISH         ;
 MOV W2,#1       | STR X3,[X2]     ;
 STR W2,[X3]     |                 ;
 exists [PTE(x)]=(oa:PA(y), af:0) /\ [y]=1  /\ ~fault(P0,y) /\ ~fault(P1,x)

Output from herd7 does not change

Test Reduced Allowed
States 3
[y]=0; [PTE(x)]=(oa:PA(x), af:0);  ~Fault(P1,x); ~Fault(P0,y);
[y]=0; [PTE(x)]=(oa:PA(y), af:0);  ~Fault(P1,x); ~Fault(P0,y);
[y]=1; [PTE(x)]=(oa:PA(x), af:0);  ~Fault(P1,x); ~Fault(P0,y);
No
Witnesses
Positive: 0 Negative: 3
Flag Assuming-common-inner-shareable-domain
Condition exists ([PTE(x)]=(oa:PA(y), af:0) /\ [y]=1 /\ not (fault(P0,y)) /\ not (fault(P1,x)))
Observation Reduced Never 0 3
Time Reduced 0.01
Hash=f5900a9742d29fdbffec4f3a26684897

Am I missing something ?

Get rid of the rsync dependency

ocaml/opam-repository#12084 (comment)

Failed atomic_cmpxchg_acquire interpreted as R[once]

I'm trying the following litmus tests in the web-version of herd7

C C-atomic-cmpxchg-failure-02

{
  atomic_t x = ATOMIC_INIT(0);
  atomic_t z = ATOMIC_INIT(0);
}

P0(atomic_t *x, atomic_t *z) {
  int r0; int r1;
  r0 = atomic_cmpxchg_acquire(z,2,1);
  r1 = atomic_read(x);
}

P1(atomic_t *x, atomic_t *z) {
  atomic_set(x,1);
  atomic_set_release(z,1);
}

exists (0:r0 = 1 /\ 0:r1 = 0)

This is what I observe in the event structures section

meaning that the read part of the comparison is given once as memory order. I checked the code and I assume this is coming from here. The question is: why the read part of an cmpxhg_acquire is assigned once instead of acquire?

	\| "atomic_fetch_add_explicit" -> ATOMIC_FETCH_EXPLICIT Op.Add
	\| "atomic_fetch_sub_explicit" -> ATOMIC_FETCH_EXPLICIT Op.Add

herd / herdtools7 Goto Github PK

herdtools7's People

Contributors

Stargazers

Watchers

Forkers

herdtools7's Issues

Recommend Projects

Recommend Topics

Recommend Org