From: Brian Norris <banorris@uci.edu>
Date: Wed, 16 Jan 2013 08:24:48 +0000 (-0800)
Subject: litmus: iriw: allow command-line switch 's' for seq_cst
X-Git-Tag: oopsla2013~356
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=342a2b1b8cf1bb74bf2b35bfd217a9c21818668f;p=model-checker.git

litmus: iriw: allow command-line switch 's' for seq_cst

The IRIW litmus test fails if we make it seq_cst; we don't see all 15
potential behaviors. Run with:

  # release/acquire litmus test
  ./run.sh test/litmus/iriw.o -v

  # seq_cst litmus test
  ./run.sh test/litmus/iriw.o -v -- s
---

diff --git a/test/litmus/iriw.cc b/test/litmus/iriw.cc
index 80ee8b9..fa4a034 100644
--- a/test/litmus/iriw.cc
+++ b/test/litmus/iriw.cc
@@ -5,32 +5,39 @@
 std::atomic_int x;
 std::atomic_int y;
 
+std::memory_order store_mo = std::memory_order_release;
+std::memory_order load_mo = std::memory_order_acquire;
+
 static void a(void *obj)
 {
-	x.store(1, std::memory_order_release);
+	x.store(1, store_mo);
 }
 
 static void b(void *obj)
 {
-	y.store(1, std::memory_order_release);
+	y.store(1, store_mo);
 }
 
 static void c(void *obj)
 {
-	printf("x1: %d\n", x.load(std::memory_order_acquire));
-	printf("y1: %d\n", y.load(std::memory_order_acquire));
+	printf("x1: %d\n", x.load(load_mo));
+	printf("y1: %d\n", y.load(load_mo));
 }
 
 static void d(void *obj)
 {
-	printf("y2: %d\n", y.load(std::memory_order_acquire));
-	printf("x2: %d\n", x.load(std::memory_order_acquire));
+	printf("y2: %d\n", y.load(load_mo));
+	printf("x2: %d\n", x.load(load_mo));
 }
 
 int user_main(int argc, char **argv)
 {
 	thrd_t t1, t2, t3, t4;
 
+	/* Command-line argument 's' enables seq_cst test */
+	if (argc > 1 && *argv[1] == 's')
+		store_mo = load_mo = std::memory_order_seq_cst;
+
 	atomic_init(&x, 0);
 	atomic_init(&y, 0);