Skip to content

Commit 2853957

Browse files
Add asmo-weak.test
Co-authored-by: Hernan Ponce de Leon <hernanl.leon@huawei.com>
1 parent fd55868 commit 2853957

1 file changed

Lines changed: 21 additions & 0 deletions

File tree

alloy/tests/asmo-weak.test

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
// Test if thread 3 and thread 4 can read updates to x in conflicting order
2+
NEWWG
3+
NEWSG
4+
NEWTHREAD
5+
st.scopedev.sc0 x = 1
6+
NEWWG
7+
NEWSG
8+
NEWTHREAD
9+
st.scopedev.sc0 x = 2
10+
NEWWG
11+
NEWSG
12+
NEWTHREAD
13+
ld.atom.scopedev.sc0 x = 1
14+
ld.atom.scopedev.sc0 x = 2
15+
NEWWG
16+
NEWSG
17+
NEWTHREAD
18+
ld.atom.scopedev.sc0 x = 2
19+
ld.atom.scopedev.sc0 x = 1
20+
SATISFIABLE consistent[X] && #dr>0
21+
SATISFIABLE consistent[X]

0 commit comments

Comments
 (0)