Skip to content

Dxxxx fix for non-atomic accesses #1

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
gonzalobg wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Dxxxx fix for non-atomic accesses #1

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 4 additions & 6 deletions tests/dat3m/auto/arfna.litmus.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,12 +1,10 @@
Test arfna Allowed
States 2
States 1
[x]=0; [y]=0;
[x]=1; [y]=1;
Undef
No
Witnesses
Positive: 1 Negative: 1
Flag *undef*
Positive: 0 Negative: 1
Condition exists ([x]=1 /\ [y]=1)
Observation arfna Sometimes 1 1
Observation arfna Never 0 1
Hash=c69a80006463884aeaf6958f9e74807a

10 changes: 4 additions & 6 deletions tests/dat3m/auto/arfna2.litmus.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,12 +1,10 @@
Test arfna_transformed Allowed
States 2
States 1
[x]=0; [y]=0;
[x]=1; [y]=1;
Undef
No
Witnesses
Positive: 1 Negative: 1
Flag *undef*
Positive: 0 Negative: 1
Condition exists ([x]=1 /\ [y]=1)
Observation arfna_transformed Sometimes 1 1
Observation arfna_transformed Never 0 1
Hash=fbb437dbcdc8a88611a71fe92622c1d5

9 changes: 4 additions & 5 deletions tests/dat3m/auto/b+acq+rel.litmus.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,13 +1,12 @@
Test b+acq+rel Allowed
States 4
States 3
0:r0=0; 1:r1=0;
0:r0=0; 1:r1=1;
0:r0=1; 1:r1=0;
0:r0=1; 1:r1=1;
Ok
No
Witnesses
Positive: 1 Negative: 3
Positive: 0 Negative: 3
Condition exists (0:r0=1 /\ 1:r1=1)
Observation b+acq+rel Sometimes 1 3
Observation b+acq+rel Never 0 3
Hash=0f7142d4a35f9e4a34d811105d759b25

9 changes: 4 additions & 5 deletions tests/dat3m/auto/b+acq+rlx.litmus.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,13 +1,12 @@
Test b+acq+rlx Allowed
States 4
States 3
0:r0=0; 1:r1=0;
0:r0=0; 1:r1=1;
0:r0=1; 1:r1=0;
0:r0=1; 1:r1=1;
Ok
No
Witnesses
Positive: 1 Negative: 3
Positive: 0 Negative: 3
Condition exists (0:r0=1 /\ 1:r1=1)
Observation b+acq+rlx Sometimes 1 3
Observation b+acq+rlx Never 0 3
Hash=a6ddbce34f4ed83e7398a60863004d24

9 changes: 4 additions & 5 deletions tests/dat3m/auto/b+acq+sc.litmus.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,13 +1,12 @@
Test b+acq+sc Allowed
States 4
States 3
0:r0=0; 1:r1=0;
0:r0=0; 1:r1=1;
0:r0=1; 1:r1=0;
0:r0=1; 1:r1=1;
Ok
No
Witnesses
Positive: 1 Negative: 3
Positive: 0 Negative: 3
Condition exists (0:r0=1 /\ 1:r1=1)
Observation b+acq+sc Sometimes 1 3
Observation b+acq+sc Never 0 3
Hash=f4c9acce455da0095bd9a81f9398dda3

9 changes: 4 additions & 5 deletions tests/dat3m/auto/b+rlx+rel.litmus.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,13 +1,12 @@
Test b+rlx+rel Allowed
States 4
States 3
0:r0=0; 1:r1=0;
0:r0=0; 1:r1=1;
0:r0=1; 1:r1=0;
0:r0=1; 1:r1=1;
Ok
No
Witnesses
Positive: 1 Negative: 3
Positive: 0 Negative: 3
Condition exists (0:r0=1 /\ 1:r1=1)
Observation b+rlx+rel Sometimes 1 3
Observation b+rlx+rel Never 0 3
Hash=f4364386d981d551de45022ce1bd6389

9 changes: 4 additions & 5 deletions tests/dat3m/auto/b+rlx+rlx.litmus.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,13 +1,12 @@
Test b+rlx+rlx Allowed
States 4
States 3
0:r0=0; 1:r1=0;
0:r0=0; 1:r1=1;
0:r0=1; 1:r1=0;
0:r0=1; 1:r1=1;
Ok
No
Witnesses
Positive: 1 Negative: 3
Positive: 0 Negative: 3
Condition exists (0:r0=1 /\ 1:r1=1)
Observation b+rlx+rlx Sometimes 1 3
Observation b+rlx+rlx Never 0 3
Hash=263307ea63cba772b35ffa9562467a92

9 changes: 4 additions & 5 deletions tests/dat3m/auto/b+rlx+sc.litmus.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,13 +1,12 @@
Test b+rlx+sc Allowed
States 4
States 3
0:r0=0; 1:r1=0;
0:r0=0; 1:r1=1;
0:r0=1; 1:r1=0;
0:r0=1; 1:r1=1;
Ok
No
Witnesses
Positive: 1 Negative: 3
Positive: 0 Negative: 3
Condition exists (0:r0=1 /\ 1:r1=1)
Observation b+rlx+sc Sometimes 1 3
Observation b+rlx+sc Never 0 3
Hash=fd321ba779c3afaa5a5f39644ed84c62

9 changes: 4 additions & 5 deletions tests/dat3m/auto/b+sc+rel.litmus.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,13 +1,12 @@
Test b+sc+rel Allowed
States 4
States 3
0:r0=0; 1:r1=0;
0:r0=0; 1:r1=1;
0:r0=1; 1:r1=0;
0:r0=1; 1:r1=1;
Ok
No
Witnesses
Positive: 1 Negative: 3
Positive: 0 Negative: 3
Condition exists (0:r0=1 /\ 1:r1=1)
Observation b+sc+rel Sometimes 1 3
Observation b+sc+rel Never 0 3
Hash=f88964bb60588f8339ee6ec8fc43c303

9 changes: 4 additions & 5 deletions tests/dat3m/auto/b+sc+rlx.litmus.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,13 +1,12 @@
Test b+sc+rlx Allowed
States 4
States 3
0:r0=0; 1:r1=0;
0:r0=0; 1:r1=1;
0:r0=1; 1:r1=0;
0:r0=1; 1:r1=1;
Ok
No
Witnesses
Positive: 1 Negative: 3
Positive: 0 Negative: 3
Condition exists (0:r0=1 /\ 1:r1=1)
Observation b+sc+rlx Sometimes 1 3
Observation b+sc+rlx Never 0 3
Hash=307b4f4af7807a1e790f80e56e464e74

9 changes: 4 additions & 5 deletions tests/dat3m/auto/b+sc+sc.litmus.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,13 +1,12 @@
Test b+sc+sc Allowed
States 4
States 3
0:r0=0; 1:r1=0;
0:r0=0; 1:r1=1;
0:r0=1; 1:r1=0;
0:r0=1; 1:r1=1;
Ok
No
Witnesses
Positive: 1 Negative: 3
Positive: 0 Negative: 3
Condition exists (0:r0=1 /\ 1:r1=1)
Observation b+sc+sc Sometimes 1 3
Observation b+sc+sc Never 0 3
Hash=1b961ffe905698d0e34c2f492e2f63ed

9 changes: 4 additions & 5 deletions tests/dat3m/auto/b.litmus.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,13 +1,12 @@
Test b Allowed
States 4
States 3
0:r0=0; 1:r1=0;
0:r0=0; 1:r1=1;
0:r0=1; 1:r1=0;
0:r0=1; 1:r1=1;
Ok
No
Witnesses
Positive: 1 Negative: 3
Positive: 0 Negative: 3
Condition exists (0:r0=1 /\ 1:r1=1)
Observation b Sometimes 1 3
Observation b Never 0 3
Hash=263307ea63cba772b35ffa9562467a92

10 changes: 4 additions & 6 deletions tests/dat3m/auto/c.litmus.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,12 +1,10 @@
Test c Allowed
States 2
States 1
[p]=0; [q]=0;
[p]=1; [q]=1;
Undef
No
Witnesses
Positive: 1 Negative: 1
Flag *undef*
Positive: 0 Negative: 1
Condition exists ([p]=1 /\ [q]=1)
Observation c Sometimes 1 1
Observation c Never 0 1
Hash=0ff4377802cdc23062bd3f44362c7fac

10 changes: 4 additions & 6 deletions tests/dat3m/auto/c_p.litmus.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,12 +1,10 @@
Test c_p Allowed
States 2
States 1
[p]=0; [q]=0;
[p]=2; [q]=1;
Undef
No
Witnesses
Positive: 0 Negative: 2
Flag *undef*
Positive: 0 Negative: 1
Condition exists ([p]=1 /\ [q]=1)
Observation c_p Never 0 2
Observation c_p Never 0 1
Hash=6b0ea2e4212c129f4929f58e34375feb

10 changes: 4 additions & 6 deletions tests/dat3m/auto/c_p_reorder.litmus.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,12 +1,10 @@
Test c_p_reorder Allowed
States 2
States 1
[p]=0; [q]=0;
[p]=2; [q]=1;
Undef
No
Witnesses
Positive: 0 Negative: 2
Flag *undef*
Positive: 0 Negative: 1
Condition exists ([p]=1 /\ [q]=1)
Observation c_p_reorder Never 0 2
Observation c_p_reorder Never 0 1
Hash=c67c1c81fada13c17a7e8ef2e1944b35

10 changes: 4 additions & 6 deletions tests/dat3m/auto/c_pq.litmus.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,12 +1,10 @@
Test c_pq Allowed
States 2
States 1
[p]=0; [q]=0;
[p]=2; [q]=1;
Undef
No
Witnesses
Positive: 0 Negative: 2
Flag *undef*
Positive: 0 Negative: 1
Condition exists ([p]=1 /\ [q]=1)
Observation c_pq Never 0 2
Observation c_pq Never 0 1
Hash=86e3436a379bae81d0e2f1d960cfd7cd

10 changes: 4 additions & 6 deletions tests/dat3m/auto/c_pq_reorder.litmus.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,12 +1,10 @@
Test c_pq_reorder Allowed
States 2
States 1
[p]=0; [q]=0;
[p]=2; [q]=1;
Undef
No
Witnesses
Positive: 0 Negative: 2
Flag *undef*
Positive: 0 Negative: 1
Condition exists ([p]=1 /\ [q]=1)
Observation c_pq_reorder Never 0 2
Observation c_pq_reorder Never 0 1
Hash=63b97be159ec65f84ff3c70d2e4e40e2

10 changes: 4 additions & 6 deletions tests/dat3m/auto/c_q.litmus.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,12 +1,10 @@
Test c_q Allowed
States 2
States 1
[p]=0; [q]=0;
[p]=1; [q]=1;
Undef
No
Witnesses
Positive: 1 Negative: 1
Flag *undef*
Positive: 0 Negative: 1
Condition exists ([p]=1 /\ [q]=1)
Observation c_q Sometimes 1 1
Observation c_q Never 0 1
Hash=bd2094625f1ee93e2689abfeb1c12d02

10 changes: 4 additions & 6 deletions tests/dat3m/auto/c_q_reorder.litmus.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,12 +1,10 @@
Test c_q_reorder Allowed
States 2
States 1
[p]=0; [q]=0;
[p]=1; [q]=1;
Undef
No
Witnesses
Positive: 1 Negative: 1
Flag *undef*
Positive: 0 Negative: 1
Condition exists ([p]=1 /\ [q]=1)
Observation c_q_reorder Sometimes 1 1
Observation c_q_reorder Never 0 1
Hash=abda1ea76cc8deea5b2c8ca2ddb27a04

10 changes: 4 additions & 6 deletions tests/dat3m/auto/c_reorder.litmus.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,12 +1,10 @@
Test c_reorder Allowed
States 2
States 1
[p]=0; [q]=0;
[p]=1; [q]=1;
Undef
No
Witnesses
Positive: 1 Negative: 1
Flag *undef*
Positive: 0 Negative: 1
Condition exists ([p]=1 /\ [q]=1)
Observation c_reorder Sometimes 1 1
Observation c_reorder Never 0 1
Hash=c6e61b3cc4e99d188768c792a17890f8

9 changes: 4 additions & 5 deletions tests/dat3m/auto/cyc.litmus.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,11 +1,10 @@
Test cyc Allowed
States 2
States 1
0:r0=0; 1:r1=0;
0:r0=1; 1:r1=1;
Ok
No
Witnesses
Positive: 1 Negative: 1
Positive: 0 Negative: 1
Condition exists (0:r0=1 /\ 1:r1=1)
Observation cyc Sometimes 1 1
Observation cyc Never 0 1
Hash=d16e1b2160f9a55f0bb557046b596103

10 changes: 4 additions & 6 deletions tests/dat3m/auto/cyc_na.litmus.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,12 +1,10 @@
Test cyc_na Allowed
States 2
States 1
0:r0=0; 1:r1=0;
0:r0=1; 1:r1=1;
Undef
No
Witnesses
Positive: 1 Negative: 1
Flag *undef*
Positive: 0 Negative: 1
Condition exists (0:r0=1 /\ 1:r1=1)
Observation cyc_na Sometimes 1 1
Observation cyc_na Never 0 1
Hash=592962ab016c17f023c60a22e9365300

4 changes: 2 additions & 2 deletions tests/dat3m/auto/fig1.litmus.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ States 1
[a]=1; [x]=1; [y]=1;
Ok
Witnesses
Positive: 4 Negative: 0
Positive: 3 Negative: 0
Condition exists ([a]=1 /\ [x]=1 /\ [y]=1)
Observation fig1 Always 4 0
Observation fig1 Always 3 0
Hash=1f61ce15fe6a88e6d904d414bf4b4d44

Loading