Skip to content

Commit 9e2e65c

Browse files
Add a todo comment to the litmus test 6 (it fails which is correct, but some sc graph edges seem to be wrong)
1 parent b350839 commit 9e2e65c

2 files changed

Lines changed: 7 additions & 4 deletions

File tree

verifying/targets/wmm_litmus/CMakeLists.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ add_wmm_litmus(litmus2_relaxed_sc FALSE)
1818
add_wmm_litmus(litmus3_sc FALSE)
1919
add_wmm_litmus(litmus4_relaxed TRUE)
2020
add_wmm_litmus(litmus5_ra FALSE)
21-
# add_wmm_litmus(litmus6_mixed TRUE) # TODO: requires a fix, see comment in the file
21+
add_wmm_litmus(litmus6_mixed TRUE) # TODO: requires a fix, see comment in the file
2222
add_wmm_litmus(litmus7_rmw_sc FALSE)
2323
add_wmm_litmus(litmus8_rmw_sc FALSE)
2424
add_wmm_litmus(litmus9_weak_rmw TRUE)

verifying/targets/wmm_litmus/litmus6_mixed.cpp

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,9 +6,12 @@
66
#include "verifying/targets/wmm_litmus/litmus_common.h"
77

88
// Example 6 (TODO: fix mixed memory order accesses, see
9-
// https://gcc.gnu.org/wiki/Atomic/GCCMM/AtomicSync) Note: Requires further
10-
// investigation, because it seems that sc support is not sound right now.
11-
// Fix it.
9+
// https://gcc.gnu.org/wiki/Atomic/GCCMM/AtomicSync)
10+
// Note: Requires further investigation,
11+
// because it seems that sc support is not sound right now. Fix it.
12+
// The article says that the test should not fail, but it seems to be wrong.
13+
// TODO: However, the sc-edges seem to be incorrect anyway, check that out
14+
// later.
1215
struct Exp6Test {
1316
std::atomic<int> x{0}, y{0};
1417

0 commit comments

Comments
 (0)