From: Brian Norris <banorris@uci.edu>
Date: Sat, 9 Mar 2013 00:50:51 +0000 (-0800)
Subject: litmus: seq-lock: add MODEL_ASSERT() for the important behavior
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=49dd0f6c667d9ab2a92301f230de60890f8c0c57

litmus: seq-lock: add MODEL_ASSERT() for the important behavior
---

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 <threads.h>
 #include <atomic>
 
+#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)