From fd55868a58cd8d4a227172d9452b21ac9f93213a Mon Sep 17 00:00:00 2001 From: Haining Date: Wed, 25 Oct 2023 18:15:26 +0300 Subject: [PATCH 1/5] Add tests Co-authored-by: Hernan Ponce de Leon --- alloy/tests/coww-rr.test | 13 +++++++++++++ alloy/tests/mp-avvis.test | 12 ++++++++++++ alloy/tests/mp-no-avvis.test | 12 ++++++++++++ 3 files changed, 37 insertions(+) create mode 100644 alloy/tests/coww-rr.test create mode 100644 alloy/tests/mp-avvis.test create mode 100644 alloy/tests/mp-no-avvis.test diff --git a/alloy/tests/coww-rr.test b/alloy/tests/coww-rr.test new file mode 100644 index 0000000..6700e65 --- /dev/null +++ b/alloy/tests/coww-rr.test @@ -0,0 +1,13 @@ +// Non-atomic memory operations may be observed by one thread in a different order than they were written by another thread +NEWWG +NEWSG +NEWTHREAD +st.sc0 x = 1 +st.sc0 x = 2 +NEWWG +NEWSG +NEWTHREAD +ld.sc0 x = 2 +ld.sc0 x = 1 +SATISFIABLE consistent[X] +NOSOLUTION consistent[X] && #dr=0 \ No newline at end of file diff --git a/alloy/tests/mp-avvis.test b/alloy/tests/mp-avvis.test new file mode 100644 index 0000000..aeb94e8 --- /dev/null +++ b/alloy/tests/mp-avvis.test @@ -0,0 +1,12 @@ +// Av/Vis + Rel/Acq forbids the behavior +NEWWG +NEWSG +NEWTHREAD +st.av.scopedev.sc0 x = 1 +st.atom.rel.scopewg.sc0.semsc0 y = 1 +NEWSG +NEWTHREAD +ld.atom.acq.scopewg.sc0.semsc0 y = 1 +ld.vis.scopedev.sc0 x = 0 +NOSOLUTION consistent[X] +NOSOLUTION consistent[X] && #dr=0 \ No newline at end of file diff --git a/alloy/tests/mp-no-avvis.test b/alloy/tests/mp-no-avvis.test new file mode 100644 index 0000000..7583b64 --- /dev/null +++ b/alloy/tests/mp-no-avvis.test @@ -0,0 +1,12 @@ +// Rel/Acq alone is not enough to forbid the behavior +NEWWG +NEWSG +NEWTHREAD +st.scopedev.sc0 x = 1 +st.atom.rel.scopewg.sc0.semsc0 y = 1 +NEWSG +NEWTHREAD +ld.atom.acq.scopewg.sc0.semsc0 y = 1 +ld.scopedev.sc0 x = 0 +SATISFIABLE consistent[X] +NOSOLUTION consistent[X] && #dr=0 \ No newline at end of file From 28539578d72b8dc3f9f9b4285a454ec5385f97b6 Mon Sep 17 00:00:00 2001 From: haining Date: Mon, 30 Oct 2023 20:22:24 +0200 Subject: [PATCH 2/5] Add asmo-weak.test Co-authored-by: Hernan Ponce de Leon --- alloy/tests/asmo-weak.test | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) create mode 100644 alloy/tests/asmo-weak.test diff --git a/alloy/tests/asmo-weak.test b/alloy/tests/asmo-weak.test new file mode 100644 index 0000000..6f347d9 --- /dev/null +++ b/alloy/tests/asmo-weak.test @@ -0,0 +1,21 @@ +// Test if thread 3 and thread 4 can read updates to x in conflicting order +NEWWG +NEWSG +NEWTHREAD +st.scopedev.sc0 x = 1 +NEWWG +NEWSG +NEWTHREAD +st.scopedev.sc0 x = 2 +NEWWG +NEWSG +NEWTHREAD +ld.atom.scopedev.sc0 x = 1 +ld.atom.scopedev.sc0 x = 2 +NEWWG +NEWSG +NEWTHREAD +ld.atom.scopedev.sc0 x = 2 +ld.atom.scopedev.sc0 x = 1 +SATISFIABLE consistent[X] && #dr>0 +SATISFIABLE consistent[X] \ No newline at end of file From f72e5e6ae079a01758dd963165fe11b0cefb2dd7 Mon Sep 17 00:00:00 2001 From: Haining Date: Wed, 8 Nov 2023 17:56:59 +0200 Subject: [PATCH 3/5] Add two tests adapted from Figure 5 of paper: Heterogeneous-race-free Memory Models Co-authored-by: Hernan Ponce de Leon --- alloy/tests/sb2dv.test | 13 +++++++++++++ alloy/tests/sb2wg.test | 11 +++++++++++ 2 files changed, 24 insertions(+) create mode 100644 alloy/tests/sb2dv.test create mode 100644 alloy/tests/sb2wg.test diff --git a/alloy/tests/sb2dv.test b/alloy/tests/sb2dv.test new file mode 100644 index 0000000..3f46e61 --- /dev/null +++ b/alloy/tests/sb2dv.test @@ -0,0 +1,13 @@ +// Adapted from Figure 5 of paper: Heterogeneous-race-free Memory Models +NEWWG +NEWSG +NEWTHREAD +st.atom.rel.scopewg.sc0.semsc0 x = 1 +ld.atom.acq.scopedev.sc0.semsc0 y = 0 +NEWWG +NEWSG +NEWTHREAD +st.atom.rel.scopewg.sc0.semsc0 y = 1 +ld.atom.acq.scopedev.sc0.semsc0 x = 0 +SATISFIABLE consistent[X] && #dr>0 +NOSOLUTION consistent[X] && #dr=0 \ No newline at end of file diff --git a/alloy/tests/sb2wg.test b/alloy/tests/sb2wg.test new file mode 100644 index 0000000..d012425 --- /dev/null +++ b/alloy/tests/sb2wg.test @@ -0,0 +1,11 @@ +// Adapted from Figure 5 of paper: Heterogeneous-race-free Memory Models +NEWWG +NEWSG +NEWTHREAD +st.atom.rel.scopewg.sc0.semsc0 x = 1 +ld.atom.acq.scopedev.sc0.semsc0 y = 0 +NEWSG +NEWTHREAD +st.atom.rel.scopewg.sc0.semsc0 y = 1 +ld.atom.acq.scopedev.sc0.semsc0 x = 0 +SATISFIABLE consistent[X] && #dr=0 \ No newline at end of file From 6bc11c7e0f85625d2b7d5e86d4879a1a2f20782f Mon Sep 17 00:00:00 2001 From: Haining Date: Tue, 28 Nov 2023 12:04:14 +0200 Subject: [PATCH 4/5] Remove scope of private operations Co-authored-by: Hernan Ponce de Leon --- alloy/tests/asmo-weak.test | 4 ++-- alloy/tests/mp-no-avvis.test | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/alloy/tests/asmo-weak.test b/alloy/tests/asmo-weak.test index 6f347d9..b59e267 100644 --- a/alloy/tests/asmo-weak.test +++ b/alloy/tests/asmo-weak.test @@ -2,11 +2,11 @@ NEWWG NEWSG NEWTHREAD -st.scopedev.sc0 x = 1 +st.sc0 x = 1 NEWWG NEWSG NEWTHREAD -st.scopedev.sc0 x = 2 +st.sc0 x = 2 NEWWG NEWSG NEWTHREAD diff --git a/alloy/tests/mp-no-avvis.test b/alloy/tests/mp-no-avvis.test index 7583b64..b26c081 100644 --- a/alloy/tests/mp-no-avvis.test +++ b/alloy/tests/mp-no-avvis.test @@ -2,11 +2,11 @@ NEWWG NEWSG NEWTHREAD -st.scopedev.sc0 x = 1 +st.sc0 x = 1 st.atom.rel.scopewg.sc0.semsc0 y = 1 NEWSG NEWTHREAD ld.atom.acq.scopewg.sc0.semsc0 y = 1 -ld.scopedev.sc0 x = 0 +ld.sc0 x = 0 SATISFIABLE consistent[X] NOSOLUTION consistent[X] && #dr=0 \ No newline at end of file From 889fcd9bec7dc617578eeb0393b08c3018f0d18a Mon Sep 17 00:00:00 2001 From: Haining Date: Thu, 30 Nov 2023 15:42:39 +0200 Subject: [PATCH 5/5] Add Control Barrier Tests Co-authored-by: Hernan Ponce de Leon --- alloy/tests/PC-bar-acq-rel-atom.test | 13 +++++++++++++ alloy/tests/PC-bar-acq-rel-nonpriv.test | 13 +++++++++++++ alloy/tests/PC-bar-acq-rel-priv.test | 13 +++++++++++++ alloy/tests/PC-bar-atom.test | 13 +++++++++++++ alloy/tests/PC-bar-nonpriv.test | 13 +++++++++++++ 5 files changed, 65 insertions(+) create mode 100644 alloy/tests/PC-bar-acq-rel-atom.test create mode 100644 alloy/tests/PC-bar-acq-rel-nonpriv.test create mode 100644 alloy/tests/PC-bar-acq-rel-priv.test create mode 100644 alloy/tests/PC-bar-atom.test create mode 100644 alloy/tests/PC-bar-nonpriv.test diff --git a/alloy/tests/PC-bar-acq-rel-atom.test b/alloy/tests/PC-bar-acq-rel-atom.test new file mode 100644 index 0000000..f305282 --- /dev/null +++ b/alloy/tests/PC-bar-acq-rel-atom.test @@ -0,0 +1,13 @@ +// Producer-Consumer pattern using named barriers. +// Atomic operations are non-private and thus the load and store are in locord. +// Barriers are acq_rel and thus they are in sw. +NEWWG +NEWSG +NEWTHREAD +ld.atom.scopewg.sc0 x = 1 +cbar.acq.rel.scopewg.semsc0 0 +NEWTHREAD +cbar.acq.rel.scopewg.semsc0 0 +st.atom.scopewg.sc0 x = 1 +NOSOLUTION consistent[X] && #dr=0 +NOSOLUTION #dr>0 \ No newline at end of file diff --git a/alloy/tests/PC-bar-acq-rel-nonpriv.test b/alloy/tests/PC-bar-acq-rel-nonpriv.test new file mode 100644 index 0000000..9de9764 --- /dev/null +++ b/alloy/tests/PC-bar-acq-rel-nonpriv.test @@ -0,0 +1,13 @@ +// Producer-Consumer pattern using named barriers. +// Load and store are non-private and thus in locord. +// Barriers are acq_rel and thus they are in sw. +NEWWG +NEWSG +NEWTHREAD +ld.nonpriv.sc0 x = 1 +cbar.acq.rel.scopewg.semsc0 0 +NEWTHREAD +cbar.acq.rel.scopewg.semsc0 0 +st.nonpriv.sc0 x = 1 +NOSOLUTION consistent[X] && #dr=0 +NOSOLUTION #dr>0 \ No newline at end of file diff --git a/alloy/tests/PC-bar-acq-rel-priv.test b/alloy/tests/PC-bar-acq-rel-priv.test new file mode 100644 index 0000000..86dcbb0 --- /dev/null +++ b/alloy/tests/PC-bar-acq-rel-priv.test @@ -0,0 +1,13 @@ +// Producer-Consumer pattern using named barriers. +// Load and store are private and thus not in locord. +// Barriers are acq_rel and thus they are in sw. +NEWWG +NEWSG +NEWTHREAD +ld.sc0 x = 1 +cbar.acq.rel.scopewg.semsc0 0 +NEWTHREAD +cbar.acq.rel.scopewg.semsc0 0 +st.sc0 x = 1 +SATISFIABLE consistent[X] +SATISFIABLE #dr>0 \ No newline at end of file diff --git a/alloy/tests/PC-bar-atom.test b/alloy/tests/PC-bar-atom.test new file mode 100644 index 0000000..5d357cf --- /dev/null +++ b/alloy/tests/PC-bar-atom.test @@ -0,0 +1,13 @@ +// Producer-Consumer pattern using named barriers. +// Atomic operations are non-private and thus the load and store are in locord. +// Barriers are not acq_rel and thus they are not in sw. +NEWWG +NEWSG +NEWTHREAD +ld.atom.scopewg.sc0 x = 1 +cbar.scopewg 0 +NEWTHREAD +cbar.scopewg 0 +st.atom.scopewg.sc0 x = 1 +SATISFIABLE consistent[X] && #dr=0 +NOSOLUTION #dr>0 diff --git a/alloy/tests/PC-bar-nonpriv.test b/alloy/tests/PC-bar-nonpriv.test new file mode 100644 index 0000000..6b65818 --- /dev/null +++ b/alloy/tests/PC-bar-nonpriv.test @@ -0,0 +1,13 @@ +// Producer-Consumer pattern using named barriers. +// Load and store are non-private and thus in locord. +// Barriers are not acq_rel and thus they are not in sw. +NEWWG +NEWSG +NEWTHREAD +ld.nonpriv.sc0 x = 1 +cbar.scopewg 0 +NEWTHREAD +cbar.scopewg 0 +st.nonpriv.sc0 x = 1 +SATISFIABLE consistent[X] +SATISFIABLE #dr>0 \ No newline at end of file