edits
authorPeizhao Ou <peizhaoo@uci.edu>
Wed, 18 Nov 2015 01:12:13 +0000 (17:12 -0800)
committerPeizhao Ou <peizhaoo@uci.edu>
Wed, 18 Nov 2015 01:12:13 +0000 (17:12 -0800)
benchmark/include/unrelacy.h [new file with mode: 0644]
benchmark/mcs-lock/mcs-lock.h
benchmark/read-copy-update/Makefile
benchmark/read-copy-update/rcu.cc
output/Makefile
src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java

diff --git a/benchmark/include/unrelacy.h b/benchmark/include/unrelacy.h
new file mode 100644 (file)
index 0000000..729d76f
--- /dev/null
@@ -0,0 +1,96 @@
+#ifndef __UNRELACY_H__
+#define __UNRELACY_H__
+
+#include <stdatomic.h>
+#include <stdlib.h>
+#include <stdio.h>
+#include <mutex>
+#include <condition_variable>
+
+#include <model-assert.h>
+#include <librace.h>
+
+#define $
+
+#define ASSERT(expr) MODEL_ASSERT(expr)
+#define RL_ASSERT(expr) MODEL_ASSERT(expr)
+
+#define RL_NEW new
+#define RL_DELETE(expr) delete expr
+
+#define mo_seqcst memory_order_relaxed
+#define mo_release memory_order_release
+#define mo_acquire memory_order_acquire
+#define mo_acq_rel memory_order_acq_rel
+#define mo_relaxed memory_order_relaxed
+
+namespace rl {
+
+       /* This 'useless' struct is declared just so we can use partial template
+        * specialization in our store and load functions. */
+       template <typename T, size_t n>
+       struct useless {
+               static void store(void *addr, T val);
+               static T load(const void *addr);
+       };
+
+       template <typename T>
+       struct useless<T, 1> {
+               static void store(void *addr, T val) { store_8(addr, (uint8_t)val); }
+               static T load(const void *addr) { return (T)load_8(addr); }
+       };
+
+       template <typename T>
+       struct useless<T, 2> {
+               static void store(void *addr, T val) { store_16(addr, (uint16_t)val); }
+               static T load(const void *addr) { return (T)load_16(addr); }
+       };
+
+       template <typename T>
+       struct useless<T, 4> {
+               static void store(void *addr, T val) { store_32(addr, (uint32_t)val); }
+               static T load(const void *addr) { return (T)load_32(addr); }
+       };
+
+       template <typename T>
+       struct useless<T, 8> {
+               static void store(void *addr, T val) { store_64(addr, (uint64_t)val); }
+               static T load(const void *addr) { return (T)load_64(addr); }
+       };
+
+       template <typename T>
+       struct var {
+               var() { useless<T, sizeof(T)>::store(&value, 0); }
+               var(T v) { useless<T, sizeof(T)>::store(&value, v); }
+               var(var const& r) {
+                       value = r.value;
+               }
+               ~var() { }
+
+               void operator = (T v) { useless<T, sizeof(T)>::store(&value, v); }
+               T operator () () { return useless<T, sizeof(T)>::load(&value); }
+               void operator += (T v) {
+                       useless<T, sizeof(T)>::store(&value,
+                                       useless<T, sizeof(T)>::load(&value) + v);
+               }
+               bool operator == (const struct var<T> v) const { return useless<T, sizeof(T)>::load(&value) == useless<T, sizeof(T)>::load(&v.value); }
+
+               T value;
+       };
+
+       class backoff_t
+       {
+        public:
+               typedef int debug_info_param;
+               void yield(debug_info_param info) { }
+               void yield() { }
+       };
+
+
+       typedef backoff_t backoff;
+       typedef backoff_t linear_backoff;
+       typedef backoff_t exp_backoff;
+
+}
+
+#endif /* __UNRELACY_H__ */
index bf49631..9f47812 100644 (file)
@@ -76,6 +76,7 @@ public:
                me->next.store(NULL, std::mo_relaxed );
                me->gate.store(1, std::mo_relaxed );
 
+               /**********  Inadmissible  **********/
                /** Run this in the -Y mode to expose the HB bug */
                // publish my node as the new tail :
                mcs_node * pred = m_tail.exchange(me, std::mo_acq_rel);
@@ -103,6 +104,7 @@ public:
                        rl::linear_backoff bo;
                        int my_gate = 1;
                        while (my_gate ) {
+                               /**********  Inadmissibility  *********/
                                my_gate = me->gate.load(std::mo_acquire);
                                //if (my_gate == 0)
                                        //printf("lock at gate!\n");
@@ -135,6 +137,8 @@ public:
                {
                        mcs_node * tail_was_me = me;
                        bool success;
+
+                       /**********  Inadmissible  **********/
                        success = m_tail.compare_exchange_strong(
                                tail_was_me,NULL,std::mo_acq_rel);
                        /**
@@ -164,6 +168,7 @@ public:
                // (*2) - store to next must be done,
                //  so no locker can be viewing my node any more        
 
+               /**********  Inadmissible  **********/
                // let next guy in :
                next->gate.store( 0, std::mo_release );
                /**
index 08941cf..1ddd57f 100644 (file)
@@ -1,10 +1,8 @@
 include ../benchmarks.mk
 
-TESTNAME = rcu 
+all: rcu 
 
-all: $(TESTNAME)
-
-$(TESTNAME): $(TESTNAME).cc $(TESTNAME).h
+rcp: rcu.cc 
        $(CXX) -o $@ $< $(CXXFLAGS) $(LDFLAGS)
 
 clean:
index 5523882..2d517bc 100644 (file)
@@ -21,7 +21,6 @@
 typedef struct Data {
        int data1;
        int data2;
-       int data3;
 } Data;
 
 atomic<Data*> data;
@@ -30,16 +29,56 @@ atomic<Data*> data;
        @Begin
        @Global_define:
                @DeclareVar:
-                       int data1;
-                       int data2;
-                       int data3;
+                       IntegerList *set;
                @InitVar:
-                       data1 = 0;
-                       data2 = 0;
-                       data3 = 0;
+                       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);
+               }
+               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;
+                       }
+               }
+       @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(Data *res) {
+                       bool hasElem = has_elem_by_value(set, (int64_t) res, &equal);
+                       return hasElem;
+               }
        @Happens_before:
                Write -> Read
                Write -> Write
+       @Commutativity: Write <-> Read: true
        @End
 */
 
@@ -47,14 +86,17 @@ atomic<Data*> data;
        @Begin
        @Interface: Read
        @Commit_point_set: Read_Success_Point
-       //@ID: isOriginalRead(__RET__) ? 1 : DEFAULT_CALL_ID
+       @ID: getID(__RET__->data1, __RET__->data2)
+       //@Action:
+               //model_print("Read_ID = %d, d1 = %d, d2 = %d\n", getID(__RET__->data1,
+               //      __RET__->data2), __RET__->data1, __RET__->data2);
+               //do_by_value(set, &print);
        @Post_check:
-               data1 == __RET__->data1 &&
-               data2 == __RET__->data2 &&
-               data3 == __RET__->data3
+               _read(__RET__);
        @End
 */
 Data* read() {
+       /**********    SPEC (sync)    **********/
        Data *res = data.load(memory_order_acquire);
        //load_32(&res->data1);
        /**
@@ -63,7 +105,6 @@ Data* read() {
                @Label: Read_Success_Point
                @End
        */
-       //model_print("Read: %d, %d, %d\n", res->data1, res->data2, res->data3);
        return res;
 }
 
@@ -71,23 +112,24 @@ Data* read() {
        @Begin
        @Interface: Write
        @Commit_point_set: Write_Success_Point
+       @ID: getID(d1, d2);
        @Action:
-               data1 += d1;
-               data2 += d2;
-               data3 += d3;
+               //model_print("Write_ID = %d\n", getID(d1, d2));
+               _write(d1, d2);
        @End
 */
-Data* write(int d1, int d2, int d3) {
+Data* write(int d1, int d2) {
        bool succ = false;
        Data *tmp = (Data*) malloc(sizeof(Data));
-       Data *prev = data.load(memory_order_acquire);
        do {
         //store_32(&tmp->data1, prev->data1 + d1);
-        tmp->data1 = prev->data1 + d1;
-           tmp->data2 = prev->data2 + d2;
-           tmp->data3 = prev->data3 + d3;
+               /**********   Inadmissibility    **********/
+               Data *prev = data.load(memory_order_acquire);
+        tmp->data1 = d1;
+           tmp->data2 = d2;
+               /**********   Inadmissibility    **********/
         succ = data.compare_exchange_strong(prev, tmp,
-            memory_order_release, memory_order_acquire);
+            memory_order_release, memory_order_relaxed);
                /**
                        @Begin
                        @Commit_point_define_check: succ
@@ -101,19 +143,20 @@ Data* write(int d1, int d2, int d3) {
 
 
 void threadA(void *arg) {
-       write(1, 0, 0);
+       write(1, 0);
 }
 
 void threadB(void *arg) {
-       write(0, 1, 0);
+       write(0, 2);
 }
 
 void threadC(void *arg) {
-       write(0, 0, 1);
+       write(2, 2);
 }
 
 void threadD(void *arg) {
-       Data *dataC = read();
+       Data *d = read();
+       printf("ThreadD: d1=%d, d2=%d\n", d->data1, d->data2);
 }
 
 int user_main(int argc, char **argv) {
@@ -127,19 +170,17 @@ int user_main(int argc, char **argv) {
        Data *dataInit = (Data*) malloc(sizeof(Data));
        dataInit->data1 = 0;
        dataInit->data2 = 0;
-       dataInit->data3 = 0;
        atomic_init(&data, dataInit);
-       write(0, 0, 0);
 
        thrd_create(&t1, threadA, NULL);
        thrd_create(&t2, threadB, NULL);
        //thrd_create(&t3, threadC, NULL);
-       //thrd_create(&t4, threadD, NULL);
+       thrd_create(&t4, threadD, NULL);
 
        thrd_join(t1);
        thrd_join(t2);
        //thrd_join(t3);
-       //thrd_join(t4);
+       thrd_join(t4);
 
        return 0;
 }
index c232475..7877016 100644 (file)
@@ -3,7 +3,7 @@
        concurrent-hashmap seqlock spsc-example spsc-queue-scfence \
        treiber-stack
 
-DIRS := ms-queue concurrent-hashmap linuxrwlocks 
+DIRS := ms-queue concurrent-hashmap linuxrwlocks mcs-lock read-copy-update
 
 .PHONY: $(DIRS)
 
index 4e74668..c75fd81 100644 (file)
@@ -312,8 +312,8 @@ public class CodeGenerator {
                                new File(homeDir + "/benchmark/ms-queue/main.c"),
                                new File(homeDir + "/benchmark/ms-queue/my_queue.h") };
 
-//             File[] srcRCU = { new File(homeDir
-//                             + "/benchmark/read-copy-update/rcu.cc") };
+               File[] srcRCU = { new File(homeDir
+                               + "/benchmark/read-copy-update/rcu.cc") };
 //             
                File[] srcTrylock = { new File(homeDir
                                + "/benchmark/trylock/trylock.c") };
@@ -324,9 +324,9 @@ public class CodeGenerator {
 //                             new File(homeDir + "/benchmark/chase-lev-deque-bugfix/testcase.c"),
 //                             new File(homeDir + "/benchmark/chase-lev-deque-bugfix/deque.h") };
 //
-//             File[] srcMCSLock = {
-//                             new File(homeDir + "/benchmark/mcs-lock/mcs-lock.cc"),
-//                             new File(homeDir + "/benchmark/mcs-lock/mcs-lock.h") };
+               File[] srcMCSLock = {
+                               new File(homeDir + "/benchmark/mcs-lock/mcs-lock.cc"),
+                               new File(homeDir + "/benchmark/mcs-lock/mcs-lock.h") };
 //
 //             File[] srcSPSCQueue = {
 //                             new File(homeDir + "/benchmark/spsc-bugfix/spsc-queue.cc"),
@@ -340,7 +340,7 @@ public class CodeGenerator {
 //             File[][] sources = { srcLinuxRWLocks,  srcMSQueue, srcRCU,
 //                             srcDeque, srcMCSLock, srcSPSCQueue, srcMPMCQueue, srcHashtable };
 
-                File[][] sources = {srcLinuxRWLock1, srcLinuxRWLock2, srcLinuxRWLock3};
+                File[][] sources = {srcRCU};
                // Compile all the benchmarks
                for (int i = 0; i < sources.length; i++) {
                        CodeGenerator gen = new CodeGenerator(sources[i]);