From: Brian Norris <banorris@uci.edu>
Date: Mon, 8 Oct 2012 06:30:48 +0000 (-0700)
Subject: test: add "double release sequence" test
X-Git-Tag: pldi2013~97^2
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=07d9e344693c6d2b85f821447be80deaee118b65

test: add "double release sequence" test

This test uses two separate load-acquire's to establish the same release
sequence. This can cause problems with the current release sequence
fixups, so that we find an execution where one synchronizes and the
other doesn't, even when reading from the same sequence.
---

diff --git a/test/double-relseq.c b/test/double-relseq.c
new file mode 100644
index 0000000..5b220eb
--- /dev/null
+++ b/test/double-relseq.c
@@ -0,0 +1,57 @@
+/*
+ * This test performs some relaxed, release, acquire opeations on a single
+ * atomic variable. It can give some rough idea of release sequence support but
+ * probably should be improved to give better information.
+ *
+ * This test tries to establish two release sequences, where we should always
+ * either establish both or establish neither. (Note that this is only true for
+ * a few executions of interest, where both load-acquire's read from the same
+ * write.)
+ */
+
+#include <stdio.h>
+
+#include "libthreads.h"
+#include "librace.h"
+#include "stdatomic.h"
+
+atomic_int x;
+int var = 0;
+
+static void a(void *obj)
+{
+	store_32(&var, 1);
+	atomic_store_explicit(&x, 1, memory_order_release);
+	atomic_store_explicit(&x, 42, memory_order_relaxed);
+}
+
+static void b(void *obj)
+{
+	int r = atomic_load_explicit(&x, memory_order_acquire);
+	printf("r = %u\n", r);
+	printf("load %d\n", load_32(&var));
+}
+
+static void c(void *obj)
+{
+	atomic_store_explicit(&x, 2, memory_order_relaxed);
+}
+
+void user_main()
+{
+	thrd_t t1, t2, t3, t4;
+
+	atomic_init(&x, 0);
+
+	printf("Thread %d: creating 4 threads\n", thrd_current());
+	thrd_create(&t1, (thrd_start_t)&a, NULL);
+	thrd_create(&t2, (thrd_start_t)&b, NULL);
+	thrd_create(&t3, (thrd_start_t)&b, NULL);
+	thrd_create(&t4, (thrd_start_t)&c, NULL);
+
+	thrd_join(t1);
+	thrd_join(t2);
+	thrd_join(t3);
+	thrd_join(t4);
+	printf("Thread %d is finished\n", thrd_current());
+}