include litmus files and runner script

run_riscv_mm_litmus.sh

@@ -0,0 +1,9 @@
+#!/bin/bash
+
+for f in $(ls test/litmus/*.litmus); do
+  echo $f ;
+  /usr/bin/time stack exec riscv-mm $f > $f.log 2>&1 ;
+  rm $f.S
+  rm $f.o
+  rm $f.exe
+done

test/litmus/2+2W+fence.rw.rw+po.litmus

@@ -0,0 +1,19 @@
+RISCV 2+2W+fence.rw.rw+po
+"Fence.rw.rwdWW Wse PodWW Wse"
+Cycle=Wse PodWW Wse Fence.rw.rwdWW
+Relax=
+Safe=Wse PodWW Fence.rw.rwdWW
+Generator=diy7 (version 7.51+4(dev))
+Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
+Com=Ws Ws
+Orig=Fence.rw.rwdWW Wse PodWW Wse
+{
+0:x5=2; 0:x6=x; 0:x7=1; 0:x8=y;
+1:x5=2; 1:x6=y; 1:x7=1; 1:x8=x;
+}
+ P0          | P1          ;
+ sw x5,0(x6) | sw x5,0(x6) ;
+ fence rw,rw | sw x7,0(x8) ;
+ sw x7,0(x8) |             ;
+exists
+(x=2 /\ y=2)

test/litmus/2+2W+fence.rw.rws.litmus

@@ -0,0 +1,19 @@
+RISCV 2+2W+fence.rw.rws
+"Fence.rw.rwdWW Wse Fence.rw.rwdWW Wse"
+Cycle=Wse Fence.rw.rwdWW Wse Fence.rw.rwdWW
+Relax=
+Safe=Wse Fence.rw.rwdWW
+Generator=diy7 (version 7.51+4(dev))
+Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
+Com=Ws Ws
+Orig=Fence.rw.rwdWW Wse Fence.rw.rwdWW Wse
+{
+0:x5=2; 0:x6=x; 0:x7=1; 0:x8=y;
+1:x5=2; 1:x6=y; 1:x7=1; 1:x8=x;
+}
+ P0          | P1          ;
+ sw x5,0(x6) | sw x5,0(x6) ;
+ fence rw,rw | fence rw,rw ;
+ sw x7,0(x8) | sw x7,0(x8) ;
+exists
+(x=2 /\ y=2)

test/litmus/2+2W.litmus

@@ -0,0 +1,18 @@
+RISCV 2+2W
+"PodWW Wse PodWW Wse"
+Cycle=Wse PodWW Wse PodWW
+Relax=
+Safe=Wse PodWW
+Generator=diy7 (version 7.51+4(dev))
+Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
+Com=Ws Ws
+Orig=PodWW Wse PodWW Wse
+{
+0:x5=2; 0:x6=x; 0:x7=1; 0:x8=y;
+1:x5=2; 1:x6=y; 1:x7=1; 1:x8=x;
+}
+ P0          | P1          ;
+ sw x5,0(x6) | sw x5,0(x6) ;
+ sw x7,0(x8) | sw x7,0(x8) ;
+exists
+(x=2 /\ y=2)

test/litmus/LB+ctrl+po.litmus

@@ -0,0 +1,20 @@
+RISCV LB+ctrl+po
+"DpCtrldW Rfe PodRW Rfe"
+Cycle=Rfe PodRW Rfe DpCtrldW
+Relax=
+Safe=Rfe PodRW DpCtrldW
+Generator=diy7 (version 7.51+4(dev))
+Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
+Com=Rf Rf
+Orig=DpCtrldW Rfe PodRW Rfe
+{
+0:x6=x; 0:x7=1; 0:x8=y;
+1:x6=y; 1:x7=1; 1:x8=x;
+}
+ P0             | P1          ;
+ lw x5,0(x6)    | lw x5,0(x6) ;
+ bne x5,x0,LC00 | sw x7,0(x8) ;
+ LC00:          |             ;
+ sw x7,0(x8)    |             ;
+exists
+(0:x5=1 /\ 1:x5=1)

test/litmus/LB+ctrls.litmus

@@ -0,0 +1,20 @@
+RISCV LB+ctrls
+"DpCtrldW Rfe DpCtrldW Rfe"
+Cycle=Rfe DpCtrldW Rfe DpCtrldW
+Relax=
+Safe=Rfe DpCtrldW
+Generator=diy7 (version 7.51+4(dev))
+Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
+Com=Rf Rf
+Orig=DpCtrldW Rfe DpCtrldW Rfe
+{
+0:x6=x; 0:x7=1; 0:x8=y;
+1:x6=y; 1:x7=1; 1:x8=x;
+}
+ P0             | P1             ;
+ lw x5,0(x6)    | lw x5,0(x6)    ;
+ bne x5,x0,LC00 | bne x5,x0,LC01 ;
+ LC00:          | LC01:          ;
+ sw x7,0(x8)    | sw x7,0(x8)    ;
+exists
+(0:x5=1 /\ 1:x5=1)

test/litmus/LB+data+ctrl.litmus

@@ -0,0 +1,20 @@
+RISCV LB+data+ctrl
+"DpDatadW Rfe DpCtrldW Rfe"
+Cycle=Rfe DpDatadW Rfe DpCtrldW
+Relax=
+Safe=Rfe DpDatadW DpCtrldW
+Generator=diy7 (version 7.51+4(dev))
+Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
+Com=Rf Rf
+Orig=DpDatadW Rfe DpCtrldW Rfe
+{
+0:x6=x; 0:x8=y;
+1:x6=y; 1:x7=1; 1:x8=x;
+}
+ P0           | P1             ;
+ lw x5,0(x6)  | lw x5,0(x6)    ;
+ xor x7,x5,x5 | bne x5,x0,LC00 ;
+ ori x7,x7,1  | LC00:          ;
+ sw x7,0(x8)  | sw x7,0(x8)    ;
+exists
+(0:x5=1 /\ 1:x5=1)

test/litmus/LB+data+po.litmus

@@ -0,0 +1,20 @@
+RISCV LB+data+po
+"DpDatadW Rfe PodRW Rfe"
+Cycle=Rfe PodRW Rfe DpDatadW
+Relax=
+Safe=Rfe PodRW DpDatadW
+Generator=diy7 (version 7.51+4(dev))
+Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
+Com=Rf Rf
+Orig=DpDatadW Rfe PodRW Rfe
+{
+0:x6=x; 0:x8=y;
+1:x6=y; 1:x7=1; 1:x8=x;
+}
+ P0           | P1          ;
+ lw x5,0(x6)  | lw x5,0(x6) ;
+ xor x7,x5,x5 | sw x7,0(x8) ;
+ ori x7,x7,1  |             ;
+ sw x7,0(x8)  |             ;
+exists
+(0:x5=1 /\ 1:x5=1)

test/litmus/LB+datas.litmus

@@ -0,0 +1,20 @@
+RISCV LB+datas
+"DpDatadW Rfe DpDatadW Rfe"
+Cycle=Rfe DpDatadW Rfe DpDatadW
+Relax=
+Safe=Rfe DpDatadW
+Generator=diy7 (version 7.51+4(dev))
+Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
+Com=Rf Rf
+Orig=DpDatadW Rfe DpDatadW Rfe
+{
+0:x6=x; 0:x8=y;
+1:x6=y; 1:x8=x;
+}
+ P0           | P1           ;
+ lw x5,0(x6)  | lw x5,0(x6)  ;
+ xor x7,x5,x5 | xor x7,x5,x5 ;
+ ori x7,x7,1  | ori x7,x7,1  ;
+ sw x7,0(x8)  | sw x7,0(x8)  ;
+exists
+(0:x5=1 /\ 1:x5=1)

test/litmus/LB+fence.rw.rw+ctrl.litmus

@@ -0,0 +1,20 @@
+RISCV LB+fence.rw.rw+ctrl
+"Fence.rw.rwdRW Rfe DpCtrldW Rfe"
+Cycle=Rfe Fence.rw.rwdRW Rfe DpCtrldW
+Relax=
+Safe=Rfe Fence.rw.rwdRW DpCtrldW
+Generator=diy7 (version 7.51+4(dev))
+Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
+Com=Rf Rf
+Orig=Fence.rw.rwdRW Rfe DpCtrldW Rfe
+{
+0:x6=x; 0:x7=1; 0:x8=y;
+1:x6=y; 1:x7=1; 1:x8=x;
+}
+ P0          | P1             ;
+ lw x5,0(x6) | lw x5,0(x6)    ;
+ fence rw,rw | bne x5,x0,LC00 ;
+ sw x7,0(x8) | LC00:          ;
+             | sw x7,0(x8)    ;
+exists
+(0:x5=1 /\ 1:x5=1)

test/litmus/LB+fence.rw.rw+data.litmus

@@ -0,0 +1,20 @@
+RISCV LB+fence.rw.rw+data
+"Fence.rw.rwdRW Rfe DpDatadW Rfe"
+Cycle=Rfe Fence.rw.rwdRW Rfe DpDatadW
+Relax=
+Safe=Rfe Fence.rw.rwdRW DpDatadW
+Generator=diy7 (version 7.51+4(dev))
+Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
+Com=Rf Rf
+Orig=Fence.rw.rwdRW Rfe DpDatadW Rfe
+{
+0:x6=x; 0:x7=1; 0:x8=y;
+1:x6=y; 1:x8=x;
+}
+ P0          | P1           ;
+ lw x5,0(x6) | lw x5,0(x6)  ;
+ fence rw,rw | xor x7,x5,x5 ;
+ sw x7,0(x8) | ori x7,x7,1  ;
+             | sw x7,0(x8)  ;
+exists
+(0:x5=1 /\ 1:x5=1)

test/litmus/LB+fence.rw.rw+po.litmus

@@ -0,0 +1,19 @@
+RISCV LB+fence.rw.rw+po
+"Fence.rw.rwdRW Rfe PodRW Rfe"
+Cycle=Rfe PodRW Rfe Fence.rw.rwdRW
+Relax=
+Safe=Rfe PodRW Fence.rw.rwdRW
+Generator=diy7 (version 7.51+4(dev))
+Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
+Com=Rf Rf
+Orig=Fence.rw.rwdRW Rfe PodRW Rfe
+{
+0:x6=x; 0:x7=1; 0:x8=y;
+1:x6=y; 1:x7=1; 1:x8=x;
+}
+ P0          | P1          ;
+ lw x5,0(x6) | lw x5,0(x6) ;
+ fence rw,rw | sw x7,0(x8) ;
+ sw x7,0(x8) |             ;
+exists
+(0:x5=1 /\ 1:x5=1)

test/litmus/LB+fence.rw.rws.litmus

@@ -0,0 +1,19 @@
+RISCV LB+fence.rw.rws
+"Fence.rw.rwdRW Rfe Fence.rw.rwdRW Rfe"
+Cycle=Rfe Fence.rw.rwdRW Rfe Fence.rw.rwdRW
+Relax=
+Safe=Rfe Fence.rw.rwdRW
+Generator=diy7 (version 7.51+4(dev))
+Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
+Com=Rf Rf
+Orig=Fence.rw.rwdRW Rfe Fence.rw.rwdRW Rfe
+{
+0:x6=x; 0:x7=1; 0:x8=y;
+1:x6=y; 1:x7=1; 1:x8=x;
+}
+ P0          | P1          ;
+ lw x5,0(x6) | lw x5,0(x6) ;
+ fence rw,rw | fence rw,rw ;
+ sw x7,0(x8) | sw x7,0(x8) ;
+exists
+(0:x5=1 /\ 1:x5=1)

test/litmus/LB.litmus

@@ -0,0 +1,18 @@
+RISCV LB
+"PodRW Rfe PodRW Rfe"
+Cycle=Rfe PodRW Rfe PodRW
+Relax=
+Safe=Rfe PodRW
+Generator=diy7 (version 7.51+4(dev))
+Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
+Com=Rf Rf
+Orig=PodRW Rfe PodRW Rfe
+{
+0:x6=x; 0:x7=1; 0:x8=y;
+1:x6=y; 1:x7=1; 1:x8=x;
+}
+ P0          | P1          ;
+ lw x5,0(x6) | lw x5,0(x6) ;
+ sw x7,0(x8) | sw x7,0(x8) ;
+exists
+(0:x5=1 /\ 1:x5=1)

test/litmus/MP+fence.rw.rw+addr.litmus

@@ -0,0 +1,20 @@
+RISCV MP+fence.rw.rw+addr
+"Fence.rw.rwdWW Rfe DpAddrdR Fre"
+Cycle=Rfe DpAddrdR Fre Fence.rw.rwdWW
+Relax=
+Safe=Rfe Fre Fence.rw.rwdWW DpAddrdR
+Generator=diy7 (version 7.51+4(dev))
+Prefetch=0:x=F,0:y=W,1:y=F,1:x=T
+Com=Rf Fr
+Orig=Fence.rw.rwdWW Rfe DpAddrdR Fre
+{
+0:x5=1; 0:x6=x; 0:x7=y;
+1:x6=y; 1:x9=x;
+}
+ P0          | P1            ;
+ sw x5,0(x6) | lw x5,0(x6)   ;
+ fence rw,rw | xor x7,x5,x5  ;
+ sw x5,0(x7) | add x10,x9,x7 ;
+             | lw x8,0(x10)  ;
+exists
+(1:x5=1 /\ 1:x8=0)

test/litmus/MP+fence.rw.rw+ctrl.litmus

@@ -0,0 +1,20 @@
+RISCV MP+fence.rw.rw+ctrl
+"Fence.rw.rwdWW Rfe DpCtrldR Fre"
+Cycle=Rfe DpCtrldR Fre Fence.rw.rwdWW
+Relax=
+Safe=Rfe Fre Fence.rw.rwdWW DpCtrldR
+Generator=diy7 (version 7.51+4(dev))
+Prefetch=0:x=F,0:y=W,1:y=F,1:x=T
+Com=Rf Fr
+Orig=Fence.rw.rwdWW Rfe DpCtrldR Fre
+{
+0:x5=1; 0:x6=x; 0:x7=y;
+1:x6=y; 1:x8=x;
+}
+ P0          | P1             ;
+ sw x5,0(x6) | lw x5,0(x6)    ;
+ fence rw,rw | bne x5,x0,LC00 ;
+ sw x5,0(x7) | LC00:          ;
+             | lw x7,0(x8)    ;
+exists
+(1:x5=1 /\ 1:x7=0)

test/litmus/MP+fence.rw.rw+po.litmus

@@ -0,0 +1,19 @@
+RISCV MP+fence.rw.rw+po
+"Fence.rw.rwdWW Rfe PodRR Fre"
+Cycle=Rfe PodRR Fre Fence.rw.rwdWW
+Relax=
+Safe=Rfe Fre PodRR Fence.rw.rwdWW
+Generator=diy7 (version 7.51+4(dev))
+Prefetch=0:x=F,0:y=W,1:y=F,1:x=T
+Com=Rf Fr
+Orig=Fence.rw.rwdWW Rfe PodRR Fre
+{
+0:x5=1; 0:x6=x; 0:x7=y;
+1:x6=y; 1:x8=x;
+}
+ P0          | P1          ;
+ sw x5,0(x6) | lw x5,0(x6) ;
+ fence rw,rw | lw x7,0(x8) ;
+ sw x5,0(x7) |             ;
+exists
+(1:x5=1 /\ 1:x7=0)

test/litmus/MP+fence.rw.rws.litmus

@@ -0,0 +1,19 @@
+RISCV MP+fence.rw.rws
+"Fence.rw.rwdWW Rfe Fence.rw.rwdRR Fre"
+Cycle=Rfe Fence.rw.rwdRR Fre Fence.rw.rwdWW
+Relax=
+Safe=Rfe Fre Fence.rw.rwdWW Fence.rw.rwdRR
+Generator=diy7 (version 7.51+4(dev))
+Prefetch=0:x=F,0:y=W,1:y=F,1:x=T
+Com=Rf Fr
+Orig=Fence.rw.rwdWW Rfe Fence.rw.rwdRR Fre
+{
+0:x5=1; 0:x6=x; 0:x7=y;
+1:x6=y; 1:x8=x;
+}
+ P0          | P1          ;
+ sw x5,0(x6) | lw x5,0(x6) ;
+ fence rw,rw | fence rw,rw ;
+ sw x5,0(x7) | lw x7,0(x8) ;
+exists
+(1:x5=1 /\ 1:x7=0)

test/litmus/MP+po+addr.litmus

@@ -0,0 +1,20 @@
+RISCV MP+po+addr
+"PodWW Rfe DpAddrdR Fre"
+Cycle=Rfe DpAddrdR Fre PodWW
+Relax=
+Safe=Rfe Fre PodWW DpAddrdR
+Generator=diy7 (version 7.51+4(dev))
+Prefetch=0:x=F,0:y=W,1:y=F,1:x=T
+Com=Rf Fr
+Orig=PodWW Rfe DpAddrdR Fre
+{
+0:x5=1; 0:x6=x; 0:x7=y;
+1:x6=y; 1:x9=x;
+}
+ P0          | P1            ;
+ sw x5,0(x6) | lw x5,0(x6)   ;
+ sw x5,0(x7) | xor x7,x5,x5  ;
+             | add x10,x9,x7 ;
+             | lw x8,0(x10)  ;
+exists
+(1:x5=1 /\ 1:x8=0)

test/litmus/MP+po+ctrl.litmus

@@ -0,0 +1,20 @@
+RISCV MP+po+ctrl
+"PodWW Rfe DpCtrldR Fre"
+Cycle=Rfe DpCtrldR Fre PodWW
+Relax=
+Safe=Rfe Fre PodWW DpCtrldR
+Generator=diy7 (version 7.51+4(dev))
+Prefetch=0:x=F,0:y=W,1:y=F,1:x=T
+Com=Rf Fr
+Orig=PodWW Rfe DpCtrldR Fre
+{
+0:x5=1; 0:x6=x; 0:x7=y;
+1:x6=y; 1:x8=x;
+}
+ P0          | P1             ;
+ sw x5,0(x6) | lw x5,0(x6)    ;
+ sw x5,0(x7) | bne x5,x0,LC00 ;
+             | LC00:          ;
+             | lw x7,0(x8)    ;
+exists
+(1:x5=1 /\ 1:x7=0)