From 49dd0f6c667d9ab2a92301f230de60890f8c0c57 Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Fri, 8 Mar 2013 16:50:51 -0800
Subject: [PATCH] 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 447123c..03724e6 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)
--
2.34.1