add seqlock

diff --git a/Makefile b/Makefile
index e988a49df3d81c24a7310253e9268876de538cf0..f47efe7e9b0eca05b38bf71d2c3c7132965538df 100644 (file)
--- 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 7f82f920f3c4df24d5ee651a5b7daccc628c55c9..4f0031f6b79ad79919a746b4d67c788fa3da5827 100644 (file)
--- 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 (executable)
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 (file)
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 (file)
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 (executable)
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 (file)
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;
+}