From 49dd0f6c667d9ab2a92301f230de60890f8c0c57 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Fri, 8 Mar 2013 16:50:51 -0800 Subject: [PATCH 1/1] litmus: seq-lock: add MODEL_ASSERT() for the important behavior --- test/litmus/seq-lock.cc | 23 +++++++++++++++++++---- 1 file changed, 19 insertions(+), 4 deletions(-) diff --git a/test/litmus/seq-lock.cc b/test/litmus/seq-lock.cc index 447123cf..03724e6f 100644 --- a/test/litmus/seq-lock.cc +++ b/test/litmus/seq-lock.cc @@ -3,6 +3,13 @@ #include #include +#include "model-assert.h" + +/* + * This 'seqlock' example should never trigger the MODEL_ASSERT() for + * release/acquire; it may trigger the MODEL_ASSERT() for release/consume + */ + std::atomic_int x; std::atomic_int y; std::atomic_int z; @@ -21,10 +28,18 @@ static void a(void *obj) static void b(void *obj) { - printf("x: %d\n", x.load(std::memory_order_acquire)); - printf("y: %d\n", y.load(std::memory_order_acquire)); - printf("z: %d\n", z.load(std::memory_order_acquire)); - printf("x: %d\n", x.load(std::memory_order_acquire)); + int x1, y1, z1, x2; + x1 = x.load(std::memory_order_acquire); + y1 = y.load(std::memory_order_acquire); + z1 = z.load(std::memory_order_acquire); + x2 = x.load(std::memory_order_acquire); + printf("x: %d\n", x1); + printf("y: %d\n", y1); + printf("z: %d\n", z1); + printf("x: %d\n", x2); + + /* If x1 and x2 are the same, even value, then y1 must equal z1 */ + MODEL_ASSERT(x1 != x2 || x1 & 0x1 || y1 == z1); } int user_main(int argc, char **argv) -- 2.34.1