add seqlock
authorPeizhao Ou <peizhaoo@uci.edu>
Wed, 18 Nov 2015 23:59:19 +0000 (15:59 -0800)
committerPeizhao Ou <peizhaoo@uci.edu>
Wed, 18 Nov 2015 23:59:19 +0000 (15:59 -0800)
benchmark/Makefile [new file with mode: 0644]
benchmark/seqlock/seqlock.cc
benchmark/seqlock/seqlock.h
output/seqlock/Makefile [new file with mode: 0644]
src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java

diff --git a/benchmark/Makefile b/benchmark/Makefile
new file mode 100644 (file)
index 0000000..3980f68
--- /dev/null
@@ -0,0 +1,17 @@
+include ../benchmarks.mk
+
+TESTNAME = main testcase1 testcase2
+
+HEADERS = deque.h
+OBJECTS = deque.o
+
+all: $(TESTNAME)
+
+$(TESTNAME): % : %.c $(OBJECTS)
+       $(CC) -o $@ $^ $(CPPFLAGS) $(LDFLAGS)
+
+%.o: %.c
+       $(CC) -c -o $@ $< $(CPPFLAGS)
+
+clean:
+       rm -f $(TESTNAME) *.o
index f25434d..4d35fba 100644 (file)
@@ -1,53 +1,41 @@
 #include <iostream>
-#include <thread>
+#include <threads.h>
 
 #include "seqlock.h"
 
-class IntWrapper {
-       private:
-           int _val;
-               public:
+seqlock *lock;
 
-               IntWrapper(int val) : _val(val) {}
-
-               IntWrapper() : _val(0) {}
-
-               IntWrapper(IntWrapper& copy) : _val(copy._val) {}
-
-               int get() {
-                       return _val;
-               }
-};
-
-static void* read_int(void *int_wrapper) {
-       IntWrapper *ptr = (IntWrapper*) int_wrapper;
-       return (void*) new int(ptr->get());
+int *readD1;
+int *readD2;
+static void read_thrd(void *obj) {
+       readD1 = new int;
+       readD2 = new int;
+       lock->read(readD1, readD2);
+       cout << "Read: d1 = " << *readD1 << ", d2 = " << *readD2 << endl;
 }
 
-
-static IntWrapper *shared_int = new IntWrapper(10);
-static seqlock<IntWrapper> my_lock(shared_int);
-
-static void read_thrd(void *obj) {
-       void *res = my_lock.read(read_int);
-       cout << "Thread read: " << *((int*) res) << endl;
+static void write_thrd1(void *obj) {
+       int d1 = 1, d2 = 0;
+       lock->write(1, 0);
+       cout << "Write: d1 = " << d1 << ", d2 = " << d2 << endl;
 }
 
-static void write_thrd(void *obj) {
-       IntWrapper *new_int = new IntWrapper(1024);
-       my_lock.write(new_int);
-       cout << "Thread write: " << new_int->get() << endl;
+static void write_thrd2(void *obj) {
+       int d1 = 1, d2 = 2;
+       lock->write(1, 2);
+       cout << "Write: d1 = " << d1 << ", d2 = " << d2 << endl;
 }
 
-int main(int argc, char *argv[]) {
-       /*
+int user_main(int argc, char *argv[]) {
+       lock = new seqlock;
        thrd_t t1, t2, t3;
-       thrd_create(&t1, (thrd_start_t) &read_thrd, NULL);
-       thrd_create(&t2, (thrd_start_t) &write_thrd, NULL);
-       thrd_create(&t3, (thrd_start_t) &read_thrd, NULL);
-       */
-       read_thrd(NULL);
-       write_thrd(NULL);
-       read_thrd(NULL);
+       thrd_create(&t1, &read_thrd, NULL);
+       thrd_create(&t2, &write_thrd1, NULL);
+       thrd_create(&t3, &write_thrd2, NULL);
+
+       thrd_join(t1);
+       thrd_join(t2);
+       thrd_join(t3);
        
+       return 0;
 }
index 92a3b63..777b685 100644 (file)
@@ -1,7 +1,15 @@
 #ifndef _SEQLOCK_H
 #define _SEQLOCK_H
 
-#include <atomic>
+#include <stdatomic.h>
+#include <unrelacy.h>
+
+#include <spec_lib.h>
+#include <stdlib.h>
+#include <cdsannotate.h>
+#include <specannotation.h>
+#include <model_memory.h>
+#include "common.h"
 
 using namespace std;
 
@@ -13,25 +21,6 @@ typedef void* (*read_func_ptr_t)(void*);
        writing.
 */
 
-
-/**
-       @Begin
-       @Global_define:
-               Type *__data_ptr = NULL;
-               bool __is_writing = false;
-
-       static bool _is_equals(void* ptr1, void* ptr2) {
-               //... Should be defined to check if the internal data equals
-       }
-
-       @Happens-before:
-               Init -> Read
-               Init -> Write
-               Write -> Write
-               Write -> Read
-       @End
-*/
-
 /**
        Fixed the write to be lock-free. Use a CAS in the write instead of using the
        mutex. There are a couple options for the implementation according to Hans
@@ -44,42 +33,99 @@ typedef void* (*read_func_ptr_t)(void*);
        with C++ fences.
 */
 
-template<typename Type>
+typedef struct Data {
+       int data1, data2;
+} Data;
+
+bool equal(int64_t p1, int64_t p2) {
+       if (!p1 || !p2)
+               return false;
+       Data *d1 = (Data*) p1;
+       Data *d2 = (Data*) p2;
+       if (d1->data1 == d2->data1 &&
+               d1->data2 == d2->data2) {
+               return true;
+       } else {
+               return false;
+       }
+}
+
+
+/**
+    @Begin
+       @Class_begin
+       @End
+*/
 class seqlock {
        private:
-       // To make the write lock-free, we don't need the mutex here.
-       // Mutex to write exclusively
-
        // Sequence for reader consistency check
        atomic_int _seq;
+       
        // The shared data structure to be protected;
        // It needs to be atomic to avoid data races
-       atomic<Type*> _data;
-       
-       // This function is to check if the objects pointed by the two pointer are
-       // the same; it is only used for checking the correctness
-       bool is_equal(void *ptr1, void *ptr2) {
-               // return ptr1 == NULL ? false : ptr1->equals(ptr2);
-       }
+       atomic_int _data1;
+       atomic_int _data2;
 
-       public:
        /**
                @Begin
-               @Interface: Init
-               @Commit_point_set: Init_Point
-               @Action:
-                       @Code:
-                       __data_ptr = data;
+               @Options:
+                       LANG = CPP;
+                       CLASS = seqlock;
+               @Global_define:
+                       @DeclareVar:
+                               IntegerList *set;
+                       @InitVar:
+                               set = createIntegerList();
+                               Data *d = (Data*) MODEL_MALLOC(sizeof(Data));
+                               d->data1 = 0;
+                               d->data2 = 0;
+                               push_back(set, (int64_t) d);
+                       @Finalize: 
+                               if (set)
+                                       destroyIntegerList(set);
+                               return true;
+               @DefineFunc:
+                       // This is a trick to get unique id
+                       // The testcase should have a unique sum
+                       call_id_t getID(int64_t d1, int64_t d2) {
+                               return d1 + d2;
+                       }
+                       @DefineFunc:
+                       bool print(int64_t p) {
+                               Data *d = (Data*) p;
+                               model_print("Elem-> d1 = %d, d2 = %d\n", d->data1, d->data2);
+                       }
+               @DefineFunc:
+                       void _write(int64_t d1, int64_t d2) {
+                               Data *d = (Data*) MODEL_MALLOC(sizeof(Data));
+                               d->data1 = d1;
+                               d->data2 = d2;
+                               push_back(set, (int64_t) d);
+                       }
+               @DefineFunc:
+                       bool _read(int d1, int d2) {
+                               Data *d = (Data*) MODEL_MALLOC(sizeof(Data));
+                               d->data1 = d1;
+                               d->data2 = d2;
+                               bool hasElem = has_elem_by_value(set, (int64_t) d, &equal);
+                               return hasElem;
+                       }
+               @Happens_before:
+                       Write -> Write
+                       Write -> Read
+               @Commutativity: Write <-> Read: true
                @End
        */
-       seqlock(Type *data) {
-               _data.store(data, memory_order_relaxed);
-               _seq.store(0, memory_order_release);
+
+       public:
+       seqlock() {
+               _data1.store(0, memory_order_relaxed);
+               _data2.store(0, memory_order_relaxed);
+               _seq.store(0, memory_order_relaxed);
+
                /**
-                       # Initialization code
-                       @Begin
-                       @Commit_point_check_define: true
-                       @Label: Init_Point
+                   @Begin
+                       @Entry_point
                        @End
                */
        }
@@ -89,74 +135,99 @@ class seqlock {
        /**
                @Begin
                @Interface: Read
-               @Commit_point_set: Read_Success_Point
-               @Action:
-                       @Code:
-                       void *_Old_data_ptr = __data_ptr;
+               @Commit_point_set: ReadPoint
+               @ID: getID(*d1, *d2)
+               //@Action:
+                       //model_print("Read_ID = %d, d1 = %d, d2 = %d\n", getID(*d1, *d2),
+                       //      *d1, *d2);
+                       //do_by_value(set, &print);
                @Post_check:
-                       _is_equal(read_func(_Old_data_ptr), __RET__)
+                       _read(*d1, *d2);
                @End
        */
-       void* read(read_func_ptr_t read_func) {
+       void read(int *d1, int *d2) {
                while (true) {
-                       int old_seq = _seq.load(memory_order_acquire);
-                       if (old_seq % 2 == 1) continue;
-                       // A customized read of something return a pointer to it
-                       // Potential data race, should be atomic
-                       void *res = read_func(_data.load(memory_order_relaxed));
-                       // This is subtle to use an acquire fence here
-                       // What we actually need is a #LoadLoad fence
+                       /**** SPEC (sequential) ****/
+                       int seq1 = _seq.load(memory_order_acquire);
+                       printf("seq1=%d\n", seq1);
+                       if (seq1 & 0x1 == 1) {
+                               thrd_yield();
+                               continue;
+                       }
+                       // Try to read the data
+                       *d1 = _data1.load(memory_order_relaxed);
+                       *d2 = _data2.load(memory_order_relaxed);
+                       /**** SPEC (sequential) ****/
                        atomic_thread_fence(memory_order_acquire);
-                       int new_seq;
-                       if ((new_seq = _seq.load(memory_order_relaxed)) == old_seq) {
-                               /**
-                                       @Begin
-                                       @Commit_point_check_define: __ATOMIC_RET__ == old_seq
-                                       @Label: Read_Success_Point
-                                       @End
-                               */
-                               return res;
+                       
+                       printf("d1=%d\n", *d1);
+                       printf("d2=%d\n", *d2);
+                       // Now doulbe check nothing got updated
+                       int seq2 = _seq.load(memory_order_relaxed);
+                       /**
+                               @Begin
+                               @Commit_point_define_check: seq1 == seq2
+                               @Label: ReadPoint
+                               @End
+                       */
+                       printf("seq2=%d\n", seq1);
+                       if (seq1 == seq2) { // Good to go
+                               printf("Result: d1=%d, d2=%d\n", *d1, *d2);
+                               return;
+                       } else {
+                               thrd_yield();
                        }
-                       // _data has been updated, read should retry
                }
        }
        
        /**
                @Begin
                @Interface: Write
-               @Commit_point_set: Write_Success_Point
+               @Commit_point_set: WritePoint
+               @ID: getID(d1, d2);
                @Action:
-                       @Code:
-                       __data_ptr = new_data;
+                       //model_print("Write_ID = %d, d1=%d, d2=%d\n", getID(d1, d2), d1, d2);
+                       _write(d1, d2);
+                       //do_by_value(set, &print);
                @End
        */
-
-       void write(Type *new_data) {
+       void write(int d1, int d2) {
+               int seq;
                while (true) {
-                       // This might be a relaxed too
-                       // Should think about how to read the lo
-                       int old_seq = _seq.load(memory_order_acquire);
-                       if (old_seq % 2 == 1) {
-                               // Backoff, another thread is writing
-                               //thrd_yield();
-                               continue; // Retry
+                       /**** admissibility ****/
+                       seq = _seq.load(memory_order_acquire);
+                       if (seq & 0x1) {
+                               thrd_yield();
+                               continue;
                        }
-                       // Should be relaxed!!! 
-                       if (_seq.compare_exchange_strong(old_seq, old_seq + 1,
-                               memory_order_relaxed, memory_order_relaxed))
+                       bool succ = _seq.compare_exchange_strong(seq, seq + 1,
+                               memory_order_relaxed, memory_order_relaxed);
+                       if (succ) {
                                break;
+                       } else {
+                               thrd_yield();
+                       }
                }
-               // Should be a store release, to synchronize with the fence!!!
-               _data.store(new_data, memory_order_release);
+               /**** SPEC (sequential) ****/
+               atomic_thread_fence(memory_order_release);
+               _data1.store(d1, memory_order_relaxed);
+               _data2.store(d2, memory_order_relaxed); 
+               // Should be a store release!!!
+               /**** admissibility ****/
                _seq.fetch_add(1, memory_order_release);
                /**
                        @Begin
-                       @Commit_point_define: true
-                       @Label: Write_Success_Point
+                       @Commit_point_define_check: true 
+                       @Label: WritePoint
                        @End
                */
        }
 };
+/**
+    @Begin
+       @Class_end
+       @End
+*/
 
 
 #endif
diff --git a/output/seqlock/Makefile b/output/seqlock/Makefile
new file mode 100644 (file)
index 0000000..e4ec9a3
--- /dev/null
@@ -0,0 +1,9 @@
+include ../benchmarks.mk
+
+all: seqlock
+
+seqlock: seqlock.cc
+       $(CXX) -o seqlock seqlock.cc $(CXXFLAGS) $(LDFLAGS)
+
+clean:
+       rm -f $(TESTNAME) *.o seqlock
index 28609e6..dd5f803 100644 (file)
@@ -317,6 +317,12 @@ public class CodeGenerator {
 //             
                File[] srcTrylock = { new File(homeDir
                                + "/benchmark/trylock/trylock.c") };
+               
+               File[] srcSeqlock = { new File(homeDir
+                               + "/benchmark/seqlock/seqlock.h"),
+                               new File(homeDir
+                                               + "/benchmark/seqlock/seqlock.cc")              
+               };
 
                File[] srcDeque = {
                                new File(homeDir + "/benchmark/chase-lev-deque-bugfix/deque.c"),
@@ -344,8 +350,9 @@ public class CodeGenerator {
 //             File[][] sources = {srcLinuxRWLock1 , srcMSQueue, srcRCU,
 //                             srcDeque, srcMCSLock, srcSPSCQueue, srcMPMCQueue, srcHashtable };
 
-                File[][] sources = {srcDeque, srcLinuxRWLock1, srcLinuxRWLock2, srcLinuxRWLock3, srcMCSLock, srcHashtable, srcRCU, srcMSQueue, srcSPSCQueue, srcMPMCQueue};
-//              File[][] sources = {srcMSQueue};
+                File[][] sources = {srcDeque, srcLinuxRWLock1, srcLinuxRWLock2, srcLinuxRWLock3, srcMCSLock, srcHashtable, srcRCU, srcMSQueue, srcSPSCQueue, srcMPMCQueue, srcSeqlock};
+               
+//              File[][] sources = {srcSeqlock};
                // Compile all the benchmarks
                for (int i = 0; i < sources.length; i++) {
                        CodeGenerator gen = new CodeGenerator(sources[i]);