From: Peizhao Ou <peizhaoo@uci.edu>
Date: Fri, 13 Feb 2015 08:03:10 +0000 (-0800)
Subject: add seqlock
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=0b1066fc15508eb5a3e8b2d4785d46a05e6a0972;p=model-checker-benchmarks.git

add seqlock
---

diff --git a/seqlock/note.txt b/seqlock/note.txt
new file mode 100644
index 0000000..6f27983
--- /dev/null
+++ b/seqlock/note.txt
@@ -0,0 +1,6 @@
+Inference results for this benchmark are consistent with the manual analysis.
+In the write() function, either the load of _seq at the very beginning or the CAS
+of the _seq when it succeeds must be acquire such that it establishes
+synchronization between two contiguous write(). If not, the two _data.store
+operations are not ordered by hb, and the next read() can read either, thus
+allowing reading the wrong (old) value.
diff --git a/seqlock/seqlock-wildcard.h b/seqlock/seqlock-wildcard.h
index 62b7583..c7d0634 100644
--- a/seqlock/seqlock-wildcard.h
+++ b/seqlock/seqlock-wildcard.h
@@ -27,14 +27,14 @@ typedef struct seqlock {
 	}
 	
 	void write(int new_data) {
-		int old_seq = _seq.load(wildcard(4)); // acquire
 		while (true) {
+			int old_seq = _seq.load(wildcard(4)); // acquire
 			if (old_seq % 2 == 1)
 				continue; // Retry
 
 			// Should be relaxed!!! 
 			if (_seq.compare_exchange_strong(old_seq, old_seq + 1,
-				wildcard(5), wildcard(6))) // relaxed 
+				wildcard(5), wildcard(6))) // relaxed  
 				break;
 		}
 
diff --git a/seqlock/seqlock.h b/seqlock/seqlock.h
index c5a965c..73e471f 100644
--- a/seqlock/seqlock.h
+++ b/seqlock/seqlock.h
@@ -1,5 +1,6 @@
 #include <stdatomic.h>
 #include <threads.h>
+#include "common.h"
 
 typedef struct seqlock {
 	// Sequence for reader consistency check
@@ -25,14 +26,16 @@ typedef struct seqlock {
 	}
 	
 	void write(int new_data) {
-		int old_seq = _seq.load(memory_order_acquire); // acquire
 		while (true) {
+			// #1: either here or #2 must be acquire
+			int old_seq = _seq.load(memory_order_acquire); // acquire
 			// This might be a relaxed too
 			if (old_seq % 2 == 1)
 				continue; // Retry
 
+			// #2
 			if (_seq.compare_exchange_strong(old_seq, old_seq + 1,
-				memory_order_acq_rel, memory_order_acquire)) 
+				memory_order_relaxed, memory_order_relaxed)) 
 				break;
 		}
 
diff --git a/seqlock/testcase1.c b/seqlock/testcase1.c
index 8441972..0c9e49c 100644
--- a/seqlock/testcase1.c
+++ b/seqlock/testcase1.c
@@ -11,10 +11,10 @@ static void a(void *obj) {
 
 static void b(void *obj) {
 	lock->write(2);
+	int r1 = lock->read();
 }
 
 static void c(void *obj) {
-	lock->write(2);
 	int r1 = lock->read();
 }
 
@@ -23,11 +23,11 @@ int user_main(int argc, char **argv) {
 	lock = new seqlock_t();
 
 	thrd_create(&t1, (thrd_start_t)&a, NULL);
-	//thrd_create(&t2, (thrd_start_t)&b, NULL);
-	thrd_create(&t3, (thrd_start_t)&c, NULL);
+	thrd_create(&t2, (thrd_start_t)&b, NULL);
+	//thrd_create(&t3, (thrd_start_t)&c, NULL);
 
 	thrd_join(t1);
-	//thrd_join(t2);
-	thrd_join(t3);
+	thrd_join(t2);
+	//thrd_join(t3);
 	return 0;
 }