add seqlock

diff --git a/benchmark/Makefile b/benchmark/Makefile
new file mode 100644 (file)
index 0000000..3980f68
--- /dev/null
+++ b/benchmark/Makefile
@@ -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

diff --git a/benchmark/seqlock/seqlock.cc b/benchmark/seqlock/seqlock.cc
index f25434d9d564d8de6c79ff574b3bfdc443c7f575..4d35fba698c29a9a6a3d4b0d66ef1a8dfff6298b 100644 (file)
--- a/benchmark/seqlock/seqlock.cc
+++ b/benchmark/seqlock/seqlock.cc
@@ -1,53 +1,41 @@
 #include <iostream>
 #include <iostream>

-#include <thread>
+#include <threads.h>

 
 #include "seqlock.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_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;

 }
 }

diff --git a/benchmark/seqlock/seqlock.h b/benchmark/seqlock/seqlock.h
index 92a3b636a57f3cba17f690b9add08e261e661c18..777b685c5486355b9b05c6c27f283b294223515b 100644 (file)
--- a/benchmark/seqlock/seqlock.h
+++ b/benchmark/seqlock/seqlock.h
@@ -1,7 +1,15 @@
 #ifndef _SEQLOCK_H
 #define _SEQLOCK_H
 
 #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;
 
 
 using namespace std;
 


@@ -13,25 +21,6 @@ typedef void* (*read_func_ptr_t)(void*);
        writing.
 */
 
        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
 /**
        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.
 */
 
        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:
 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;
        // Sequence for reader consistency check
        atomic_int _seq;

+       

        // The shared data structure to be protected;
        // It needs to be atomic to avoid data races
        // 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
        /**
                @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
        */
                @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
                */
        }
                        @End
                */
        }


@@ -89,74 +135,99 @@ class seqlock {
        /**
                @Begin
                @Interface: Read
        /**
                @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:
                @Post_check:

-                       _is_equal(read_func(_Old_data_ptr), __RET__)
+                       _read(*d1, *d2);

                @End
        */
                @End
        */

-       void* read(read_func_ptr_t read_func) {
+       void read(int *d1, int *d2) {

                while (true) {
                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);
                        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
                }
        }
        
        /**
                @Begin
                @Interface: Write

-               @Commit_point_set: Write_Success_Point
+               @Commit_point_set: WritePoint
+               @ID: getID(d1, d2);

                @Action:
                @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
        */
                @End
        */

-
-       void write(Type *new_data) {
+       void write(int d1, int d2) {
+               int seq;

                while (true) {
                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;
                                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
                _seq.fetch_add(1, memory_order_release);
                /**
                        @Begin

-                       @Commit_point_define: true
-                       @Label: Write_Success_Point
+                       @Commit_point_define_check: true 
+                       @Label: WritePoint

                        @End
                */
        }
 };
                        @End
                */
        }
 };

+/**
+    @Begin
+       @Class_end
+       @End
+*/

 
 
 #endif
 
 
 #endif

diff --git a/output/seqlock/Makefile b/output/seqlock/Makefile
new file mode 100644 (file)
index 0000000..e4ec9a3
--- /dev/null
+++ b/output/seqlock/Makefile
@@ -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

diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
index 28609e6de8c3a47262adaed1e4ca4b9d714ddada..dd5f803a083b143bea623282fc4c002a2a283a7d 100644 (file)
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
@@ -317,6 +317,12 @@ public class CodeGenerator {
 //             
                File[] srcTrylock = { new File(homeDir
                                + "/benchmark/trylock/trylock.c") };
 //             
                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"),
 
                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 = {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]);
                // Compile all the benchmarks
                for (int i = 0; i < sources.length; i++) {
                        CodeGenerator gen = new CodeGenerator(sources[i]);