Skip to content

Commit 84198e5

Browse files
Add coherence tests
Co-authored-by: Hernan Ponce de Leon <hernanl.leon@huawei.com>
1 parent fc4f786 commit 84198e5

2 files changed

Lines changed: 44 additions & 0 deletions

File tree

tests/Manual/Coherence-weak.test

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
// Test if P2 and P3 can read updates to x in conflicting order
2+
.global x;
3+
4+
d0.b0.t0 {
5+
st.weak [x], 1;
6+
}
7+
8+
d0.b0.t1 {
9+
st.weak [x], 2;
10+
}
11+
12+
d0.b0.t2 {
13+
ld.acquire.sys r0, [x];
14+
ld.acquire.sys r1, [x];
15+
}
16+
17+
d0.b0.t3 {
18+
ld.acquire.sys r2, [x];
19+
ld.acquire.sys r3, [x];
20+
}
21+
22+
permit(r0 == 1 && r1 == 2 && r2 == 2 && r3 == 1) as coherence_weak;

tests/Manual/Coherence.test

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
// Test that threads 3 and 4 can't read updates to x in conflicting order
2+
.global x;
3+
4+
d0.b0.t0 {
5+
st.relaxed.sys [x], 1;
6+
}
7+
8+
d0.b0.t1 {
9+
st.relaxed.sys [x], 2;
10+
}
11+
12+
d0.b0.t2 {
13+
ld.acquire.sys r0, [x];
14+
ld.acquire.sys r1, [x];
15+
}
16+
17+
d0.b0.t3 {
18+
ld.acquire.sys r2, [x];
19+
ld.acquire.sys r3, [x];
20+
}
21+
22+
assert(r0 != 1 || r1 != 2 || r2 != 2 || r3 != 1) as coherence;

0 commit comments

Comments
 (0)