From: Peizhao Ou <peizhaoo@uci.edu>
Date: Thu, 7 Aug 2014 01:39:41 +0000 (-0700)
Subject: add seqlock
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker-benchmarks.git;a=commitdiff_plain;h=cec79cfe07dea7f730f0f0c928a34689f2119809

add seqlock
---

diff --git a/Makefile b/Makefile
index e988a49..f47efe7 100644
--- a/Makefile
+++ b/Makefile
@@ -1,5 +1,5 @@
 DIRS := barrier mcs-lock mpmc-queue spsc-queue spsc-bugfix linuxrwlocks \
-	dekker-fences chase-lev-deque ms-queue chase-lev-deque-bugfix
+	dekker-fences chase-lev-deque ms-queue chase-lev-deque-bugfix seqlock
 
 .PHONY: $(DIRS)
 
diff --git a/benchmarks.mk b/benchmarks.mk
index 7f82f92..4f0031f 100644
--- a/benchmarks.mk
+++ b/benchmarks.mk
@@ -8,7 +8,8 @@ UNAME = $(shell uname)
 LIB_NAME = model
 LIB_SO = lib$(LIB_NAME).so
 
-BASE = ../..
+#BASE = ../..
+BASE = $(CDS_DIR)
 INCLUDE = -I$(BASE)/include -I../include
 
 # C preprocessor flags
diff --git a/build.sh b/build.sh
new file mode 100755
index 0000000..d78b2e0
--- /dev/null
+++ b/build.sh
@@ -0,0 +1,11 @@
+#!/bin/bash
+
+CHECKER_DIR=~/model-checker-priv/model-checker-priv
+
+if [ -z $1 ] ; then
+	echo "Use default CDS checker directory"
+else
+	CHECKER_DIR=$1
+fi
+
+make CDS_DIR=$CHECKER_DIR
diff --git a/doc/scanalysis_result.txt b/doc/scanalysis_result.txt
new file mode 100644
index 0000000..c93472a
--- /dev/null
+++ b/doc/scanalysis_result.txt
@@ -0,0 +1,11 @@
+Chase-Lev (buggy)	65		24	0.0021	0.13	68	3.2*10^-5
+Chase-Lev (correct)	49		1	0.0016	0.06	75	3.2*10^-5
+SPSC (buggy)		10		2	0.0002	0.03	26	1.7*10^-5
+SPSC (correct)		15		0	0.0004	0.03	29	2.7*10^-5
+Barrier				7		0	0.0002	0.01	23	2.9*10^-5
+Dekker				2313	0	0.0793	10.19	52	3.4*10^-5	
+MCS lock			12609	0	0.3409	4.85	65	2.7*10^-5
+MPMC queue			11306
+M&S queue			114
+Linux RW lock		1348
+Seqlock				9124	0	0.4895	3.818	38	5.3*10^-5
diff --git a/seqlock/Makefile b/seqlock/Makefile
new file mode 100644
index 0000000..98375f9
--- /dev/null
+++ b/seqlock/Makefile
@@ -0,0 +1,9 @@
+include ../benchmarks.mk
+
+all: seqlock
+
+seqlock: seqlock.c
+	$(CXX) -o $@ $< $(CXXFLAGS) $(LDFLAGS)
+
+clean:
+	rm -f seqlock
diff --git a/seqlock/seqlock b/seqlock/seqlock
new file mode 100755
index 0000000..32a01ab
Binary files /dev/null and b/seqlock/seqlock differ
diff --git a/seqlock/seqlock.c b/seqlock/seqlock.c
new file mode 100644
index 0000000..3762374
--- /dev/null
+++ b/seqlock/seqlock.c
@@ -0,0 +1,75 @@
+#include <stdatomic.h>
+#include <threads.h>
+
+typedef struct seqlock {
+	// Sequence for reader consistency check
+	atomic_int _seq;
+	// It needs to be atomic to avoid data races
+	atomic_int _data;
+
+	seqlock() {
+		atomic_init(&_seq, 0);
+		atomic_init(&_data, 0);
+	}
+
+	int read() {
+		while (true) {
+			int old_seq = _seq.load(memory_order_acquire); // acquire
+			if (old_seq % 2 == 1) continue;
+
+			int res = _data.load(memory_order_acquire); // acquire
+			if (_seq.load(memory_order_relaxed) == old_seq) { // relaxed
+				return res;
+			}
+		}
+	}
+	
+	void write(int new_data) {
+		while (true) {
+			// This might be a relaxed too
+			int old_seq = _seq.load(memory_order_acquire); // acquire
+			if (old_seq % 2 == 1)
+				continue; // Retry
+
+			// Should be relaxed!!! 
+			if (_seq.compare_exchange_strong(old_seq, old_seq + 1,
+				memory_order_relaxed, memory_order_relaxed)) // relaxed 
+				break;
+		}
+
+		// Update the data
+		_data.store(new_data, memory_order_release); // release
+
+		_seq.fetch_add(1, memory_order_release); // release
+	}
+
+} seqlock_t;
+
+
+seqlock_t *lock;
+
+static void a(void *obj) {
+	lock->write(3);
+}
+
+static void b(void *obj) {
+	lock->write(2);
+}
+
+static void c(void *obj) {
+	int r1 = lock->read();
+}
+
+int user_main(int argc, char **argv) {
+	thrd_t t1, t2, t3, t4;
+	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_join(t1);
+	thrd_join(t2);
+	thrd_join(t3);
+	return 0;
+}