changes with lines of spec counted
authorPeizhao Ou <peizhaoo@uci.edu>
Thu, 22 Jan 2015 23:22:59 +0000 (15:22 -0800)
committerPeizhao Ou <peizhaoo@uci.edu>
Thu, 22 Jan 2015 23:22:59 +0000 (15:22 -0800)
benchmark/chase-lev-deque-bugfix/deque.h
benchmark/cliffc-hashtable/cliffc_hashtable.h
benchmark/linuxrwlocks/linuxrwlocks.c
benchmark/mcs-lock/mcs-lock.h
benchmark/mpmc-queue/mpmc-queue.h
benchmark/ms-queue/my_queue.h
benchmark/read-copy-update/rcu.cc
benchmark/spsc-bugfix/queue.h
note.txt [new file with mode: 0644]

index 0e2fb2b..837df89 100644 (file)
@@ -37,15 +37,15 @@ typedef struct {
         id_tag_t *tag;
         @InitVar:
             __deque = new_spec_list();
-                       model_print("init_list\n");
+                       //model_print("init_list\n");
             tag = new_id_tag(); // Beginning of available id
-               @Cleanup:
-                       if (__deque) {
+               //@Cleanup:
+                       //if (__deque) {
                                //free_spec_list(__deque);
-                               model_print("free_list\n");
-                       }
-                       if (tag)
-                               free_id_tag(tag);
+                               //model_print("free_list\n");
+                       //}
+                       //if (tag)
+                               //free_id_tag(tag);
         @DefineFunc:
             tag_elem_t* new_tag_elem(call_id_t id, int data) {
                 tag_elem_t *e = (tag_elem_t*) CMODEL_MALLOC(sizeof(tag_elem_t));
@@ -55,17 +55,19 @@ typedef struct {
             }
         @DefineFunc:
             call_id_t get_id(void *wrapper) {
-                               tag_elem_t *res = (tag_elem_t*) wrapper;
-                               if (res == NULL) {
+                               //tag_elem_t *res = (tag_elem_t*) wrapper;
+                               return res == NULL ? 0 : ((tag_elem_t*) wrapper)->id;
+                               //if (res == NULL) {
                                        //model_print("wrong id here\n");
-                                       return 0;
-                               }
-                return res->id;
+                                       //return 0;
+                               //}
+                //return res->id;
             }
         @DefineFunc:
             int get_data(void *wrapper) {
-                               tag_elem_t *res = (tag_elem_t*) wrapper;
-                return res->data;
+                               //tag_elem_t *res = (tag_elem_t*) wrapper;
+                //return res->data;
+                               return ((tag_elem_t*) wrapper)->data;
             }
     @Happens_before:
         Push -> Steal
@@ -85,14 +87,11 @@ void resize(Deque *q);
     @ID: __RET__ == EMPTY ? DEFAULT_CALL_ID : get_id(back(__deque))
     @Action:
         int _Old_Val = EMPTY;
-               if (__RET__ != EMPTY) {
-                       if (size(__deque) > 0) {
-                               _Old_Val = get_data(back(__deque));
-                       pop_back(__deque);
-                       }       
+               if (__RET__ != EMPTY && size(__deque) > 0) {
+                       _Old_Val = get_data(back(__deque));
+               pop_back(__deque);
                }
-    @Post_check:
-        _Old_Val == __RET__
+    @Post_check: _Old_Val == __RET__
     @End
 */
 int take(Deque *q);
@@ -102,9 +101,7 @@ int take(Deque *q);
     @Interface: Push 
     @Commit_point_set: Push_Update_Bottom 
     @ID: get_and_inc(tag);
-    @Action:
-        tag_elem_t *elem = new_tag_elem(__ID__, x);
-        push_back(__deque, elem);
+    @Action: push_back(__deque, new_tag_elem(__ID__, x));
     @End
 */
 void push(Deque *q, int x);
@@ -117,11 +114,9 @@ void push(Deque *q, int x);
     @ID: (__RET__ == EMPTY || __RET__ == ABORT) ? DEFAULT_CALL_ID : get_id(front(__deque))
     @Action:
         int _Old_Val = EMPTY;
-               if (__RET__ != EMPTY && __RET__ != ABORT) {
-                       if (size(__deque) > 0) {
-                               _Old_Val = get_data(front(__deque));
-                               pop_front(__deque);
-                       }
+               if (__RET__ != EMPTY && __RET__ != ABORT && size(__deque) > 0) {
+                       _Old_Val = get_data(front(__deque));
+                       pop_front(__deque);
                }
     @Post_check:
         _Old_Val == __RET__ || __RET__ == EMPTY || __RET__ == ABORT
index 1160c13..c09b7a1 100644 (file)
@@ -111,8 +111,7 @@ class cliffc_hashtable {
                        //      model_print("cleaning up\n");
                        @DefineFunc:
                        bool equals_key(void *ptr1, void *ptr2) {
-                               TypeK *key1 = (TypeK*) ptr1,
-                                       *key2 = (TypeK*) ptr2;
+                               TypeK *key1 = (TypeK*) ptr1, *key2 = (TypeK*) ptr2;
                                if (key1 == NULL || key2 == NULL)
                                        return false;
                                return key1->equals(key2);
@@ -122,8 +121,7 @@ class cliffc_hashtable {
                        bool equals_val(void *ptr1, void *ptr2) {
                                if (ptr1 == ptr2)
                                        return true;
-                               TypeV *val1 = (TypeV*) ptr1,
-                                       *val2 = (TypeV*) ptr2;
+                               TypeV *val1 = (TypeV*) ptr1, *val2 = (TypeV*) ptr2;
                                if (val1 == NULL || val2 == NULL)
                                        return false;
                                return val1->equals(val2);
@@ -131,8 +129,7 @@ class cliffc_hashtable {
 
                        @DefineFunc:
                        bool equals_id(void *ptr1, void *ptr2) {
-                               id_tag_t *id1 = (id_tag_t*) ptr1,
-                                       *id2 = (id_tag_t*) ptr2;
+                               id_tag_t *id1 = (id_tag_t*) ptr1, *id2 = (id_tag_t*) ptr2;
                                if (id1 == NULL || id2 == NULL)
                                        return false;
                                return (*id1).tag == (*id2).tag;
@@ -422,13 +419,13 @@ friend class CHM;
                @Action:
                        TypeV *_Old_Val = (TypeV*) spec_table_get(map, key);
                        //bool passed = equals_val(_Old_Val, __RET__);
-                       bool passed = false;
-                       if (!passed) {
-                               int old = _Old_Val == NULL ? 0 : _Old_Val->_val;
-                               int ret = __RET__ == NULL ? 0 : __RET__->_val;
+                       //bool passed = false;
+                       //if (!passed) {
+                               //int old = _Old_Val == NULL ? 0 : _Old_Val->_val;
+                               //int ret = __RET__ == NULL ? 0 : __RET__->_val;
                                //model_print("Get: key: %d, _Old_Val: %d, RET: %d\n",
                                //key->_val, old, ret);
-                       }
+                       //}
                @Post_check:
                        //__RET__ == NULL ? true : equals_val(_Old_Val, __RET__)
                        equals_val(_Old_Val, __RET__)
@@ -462,13 +459,13 @@ friend class CHM;
                        TypeV *_Old_Val = (TypeV*) spec_table_get(map, key);
                        spec_table_put(map, key, val);
                        //bool passed = equals_val(__RET__, _Old_Val);
-                       bool passed = false;
-                       if (!passed) {
-                               int old = _Old_Val == NULL ? 0 : _Old_Val->_val;
-                               int ret = __RET__ == NULL ? 0 : __RET__->_val;
+                       //bool passed = false;
+                       //if (!passed) {
+                               //int old = _Old_Val == NULL ? 0 : _Old_Val->_val;
+                               //int ret = __RET__ == NULL ? 0 : __RET__->_val;
                                //model_print("Put: key: %d, val: %d, _Old_Val: %d, RET: %d\n",
                                //      key->_val, val->_val, old, ret);
-                       }
+                       //}
                @Post_check:
                        equals_val(__RET__, _Old_Val)
                @End
index 936a16a..b97c45b 100644 (file)
@@ -88,12 +88,9 @@ static inline int write_can_lock(rwlock_t *lock)
 /**
        @Begin
        @Interface: Read_Lock
-       @Commit_point_set:
-               Read_Lock_Success_1 | Read_Lock_Success_2
-       @Check:
-               !writer_lock_acquired
-       @Action:
-               reader_lock_cnt++;
+       @Commit_point_set: Read_Lock_Success_1 | Read_Lock_Success_2
+       @Check: !writer_lock_acquired
+       @Action: reader_lock_cnt++;
        @End
 */
 static inline void read_lock(rwlock_t *rw)
@@ -124,12 +121,9 @@ static inline void read_lock(rwlock_t *rw)
 /**
        @Begin
        @Interface: Write_Lock
-       @Commit_point_set:
-               Write_Lock_Success_1 | Write_Lock_Success_2
-       @Check:
-               !writer_lock_acquired && reader_lock_cnt == 0
-       @Action:
-               writer_lock_acquired = true;
+       @Commit_point_set: Write_Lock_Success_1 | Write_Lock_Success_2
+       @Check: !writer_lock_acquired && reader_lock_cnt == 0
+       @Action: writer_lock_acquired = true;
        @End
 */
 static inline void write_lock(rwlock_t *rw)
@@ -159,17 +153,13 @@ static inline void write_lock(rwlock_t *rw)
 /**
        @Begin
        @Interface: Read_Trylock
-       @Commit_point_set:
-               Read_Trylock_Succ_Point | Read_Trylock_Fail_Point
-       @Condition:
-               writer_lock_acquired == false
-       @HB_condition:
-               HB_Read_Trylock_Succ :: __RET__ == 1
+       @Commit_point_set: Read_Trylock_Succ_Point | Read_Trylock_Fail_Point
+       //@Condition: writer_lock_acquired == false
+       @HB_condition: HB_Read_Trylock_Succ :: __RET__ == 1
        @Action:
                if (__COND_SAT__)
                        reader_lock_cnt++;
-       @Post_check:
-               __COND_SAT__ ? __RET__ == 1 : __RET__ == 0
+       @Post_check: __COND_SAT__ ? __RET__ == 1 : __RET__ == 0
        @End
 */
 static inline int read_trylock(rwlock_t *rw)
@@ -205,10 +195,8 @@ static inline int read_trylock(rwlock_t *rw)
 /**
        @Begin
        @Interface: Write_Trylock
-       @Commit_point_set:
-               Write_Trylock_Succ_Point | Write_Trylock_Fail_Point
-       @HB_condition:
-               HB_Write_Trylock_Succ :: __RET__ == 1
+       @Commit_point_set: Write_Trylock_Succ_Point | Write_Trylock_Fail_Point
+       @HB_condition: HB_Write_Trylock_Succ :: __RET__ == 1
        @Action:
                if (__RET__ == 1)
                        writer_lock_acquired = true;
@@ -249,10 +237,8 @@ static inline int write_trylock(rwlock_t *rw)
        @Begin
        @Interface: Read_Unlock
        @Commit_point_set: Read_Unlock_Point
-       @Check:
-               reader_lock_cnt > 0 && !writer_lock_acquired
-       @Action: 
-               reader_lock_cnt--;
+       @Check: reader_lock_cnt > 0 && !writer_lock_acquired
+       @Action: reader_lock_cnt--;
        @End
 */
 static inline void read_unlock(rwlock_t *rw)
@@ -270,10 +256,8 @@ static inline void read_unlock(rwlock_t *rw)
        @Begin
        @Interface: Write_Unlock
        @Commit_point_set: Write_Unlock_Point | Write_Unlock_Clear
-       @Check:
-               reader_lock_cnt == 0 && writer_lock_acquired
-       @Action: 
-               writer_lock_acquired = false;
+       @Check: reader_lock_cnt == 0 && writer_lock_acquired
+       @Action: writer_lock_acquired = false;
        @End
 */
 static inline void write_unlock(rwlock_t *rw)
index 46c6530..bf49631 100644 (file)
@@ -54,12 +54,9 @@ public:
                        LANG = CPP;
                        CLASS = mcs_mutex;
                @Global_define:
-                       @DeclareVar:
-                               bool _lock_acquired;
-                       @InitVar:
-                               _lock_acquired = false;
-               @Happens_before:
-                       Unlock -> Lock
+                       @DeclareVar: bool _lock_acquired;
+                       @InitVar: _lock_acquired = false;
+               @Happens_before: Unlock -> Lock
                @End
        */
 
@@ -67,10 +64,8 @@ public:
                @Begin
                @Interface: Lock
                @Commit_point_set: Lock_Enqueue_Point1 | Lock_Enqueue_Point2
-               @Check:
-                       _lock_acquired == false;
-               @Action:
-                       _lock_acquired = true;
+               @Check: _lock_acquired == false;
+               @Action: _lock_acquired = true;
                @End
        */
        void lock(guard * I) {
@@ -125,12 +120,9 @@ public:
        /**
                @Begin
                @Interface: Unlock
-               @Commit_point_set:
-                       Unlock_Point_Success_1 | Unlock_Point_Success_2
-               @Check:
-                       _lock_acquired == true
-               @Action:
-                       _lock_acquired = false;
+               @Commit_point_set: Unlock_Point_Success_1 | Unlock_Point_Success_2
+               @Check: _lock_acquired == true
+               @Action: _lock_acquired = false;
                @End
        */
        void unlock(guard * I) {
index 6f1bac6..aa10129 100644 (file)
@@ -48,23 +48,23 @@ public:
                        LANG = CPP;
                        CLASS = mpmc_boundq_1_alt;
                @Global_define:
-               @DeclareStruct:
-                       typedef struct elem {
-                               t_element *pos;
-                               bool written;
-                               thread_id_t tid;
-                               thread_id_t fetch_tid;
-                               call_id_t id;
-                       } elem;
-               @DeclareVar:
-                       spec_list *list;
+               //@DeclareStruct:
+                       //typedef struct elem {
+                       //      t_element *pos;
+                       //      bool written;
+                       //      thread_id_t tid;
+                       //      thread_id_t fetch_tid;
+                       //      call_id_t id;
+               //      } elem;
+       //      @DeclareVar:
+       //              spec_list *list;
                        //id_tag_t *tag;
-               @InitVar:
-                       list = new_spec_list();
+       //      @InitVar:
+       //              list = new_spec_list();
                        //tag = new_id_tag();
-               @Cleanup:
-                       if (list)
-                               free_spec_list();
+       //      @Cleanup:
+//                     if (list)
+//                             free_spec_list();
        @Happens_before:
                Publish -> Fetch
                Consume -> Prepare
index ce87b1d..ce6fd06 100644 (file)
@@ -49,16 +49,16 @@ void init_queue(queue_t *q, int num_threads);
                } tag_elem_t;
                
                @DeclareVar:
-               spec_list *__queue;
-               id_tag_t *tag;
+                       spec_list *__queue;
+                       id_tag_t *tag;
                @InitVar:
                        __queue = new_spec_list();
                        tag = new_id_tag(); // Beginning of available id
-               @Cleanup:
-                       if (__queue)
-                               free_spec_list(__queue);
-                       if (tag)
-                               free_id_tag(tag);
+               //@Cleanup:
+               //      if (__queue)
+               //              free_spec_list(__queue);
+               //      if (tag)
+               //              free_id_tag(tag);
                @DefineFunc:
                        tag_elem_t* new_tag_elem(call_id_t id, unsigned int data) {
                                tag_elem_t *e = (tag_elem_t*) CMODEL_MALLOC(sizeof(tag_elem_t));
@@ -66,25 +66,25 @@ void init_queue(queue_t *q, int num_threads);
                                e->data = data;
                                return e;
                        }
-               @DefineFunc:
-                       void free_tag_elem(tag_elem_t *e) {
-                               free(e);
-                       }
+               //@DefineFunc:
+               //      void free_tag_elem(tag_elem_t *e) {
+               //              free(e);
+               //      }
                @DefineFunc:
                        call_id_t get_id(void *wrapper) {
-                               if (wrapper == NULL)
-                                       return 0;
-                               return ((tag_elem_t*) wrapper)->id;
+               //              if (wrapper == NULL)
+               //                      return 0;
+               //              return ((tag_elem_t*) wrapper)->id;
+                               return wrapper == NULL ? 0 : ((tag_elem_t*) wrapper)->id;
                        }
                @DefineFunc:
                        unsigned int get_data(void *wrapper) {
                                return ((tag_elem_t*) wrapper)->data;
                        }
-       @Happens_before:
+       @Happens_before: Enqueue -> Dequeue
                # Only check the happens-before relationship according to the id of the
                # commit_point_set. For commit_point_set that has same ID, A -> B means
                # B happens after the previous A.
-               Enqueue -> Dequeue
        @End
 */
 
@@ -117,8 +117,7 @@ void enqueue(queue_t *q, unsigned int val);
                        pop_front(__queue);
                }
        //      model_print("Dequeue: __RET__=%d, retVal=%d, Old_Val=%d\n", __RET__, *retVal, _Old_Val);
-       @Post_check:
-               _Old_Val == 0 ? !__RET__ : _Old_Val == *retVal
+       @Post_check: _Old_Val == 0 ? !__RET__ : _Old_Val == *retVal
        @End
 */
 bool dequeue(queue_t *q, int *retVal);
index b665480..5523882 100644 (file)
@@ -87,7 +87,7 @@ Data* write(int d1, int d2, int d3) {
            tmp->data2 = prev->data2 + d2;
            tmp->data3 = prev->data3 + d3;
         succ = data.compare_exchange_strong(prev, tmp,
-            memory_order_acq_rel, memory_order_relaxed);
+            memory_order_release, memory_order_acquire);
                /**
                        @Begin
                        @Commit_point_define_check: succ
@@ -133,13 +133,13 @@ int user_main(int argc, char **argv) {
 
        thrd_create(&t1, threadA, NULL);
        thrd_create(&t2, threadB, NULL);
-       thrd_create(&t3, threadC, NULL);
-       thrd_create(&t4, threadD, NULL);
+       //thrd_create(&t3, threadC, NULL);
+       //thrd_create(&t4, threadD, NULL);
 
        thrd_join(t1);
        thrd_join(t2);
-       thrd_join(t3);
-       thrd_join(t4);
+       //thrd_join(t3);
+       //thrd_join(t4);
 
        return 0;
 }
index 0a38e8f..67be1b7 100644 (file)
@@ -78,8 +78,7 @@ public:
                        unsigned int get_data(void *wrapper) {
                                return ((tag_elem_t*) wrapper)->data;
                        }
-               @Happens_before:
-                       Enqueue -> Dequeue              
+               @Happens_before: Enqueue -> Dequeue             
                @End
        */
 
@@ -89,9 +88,9 @@ public:
                @Interface: Enqueue
                @Commit_point_set: Enqueue_Point
                @ID: get_and_inc(tag)
-               @Action:
-                       tag_elem_t *elem = new_tag_elem(__ID__, data);
-                       push_back(__queue, elem);
+               @Action: push_back(__queue, new_tag_elem(__ID__, data));
+                       //tag_elem_t *elem = new_tag_elem(__ID__, data);
+                       //push_back(__queue, elem);
                @End
        */
        void enqueue(T data)
@@ -116,8 +115,7 @@ public:
                @Action:
                        T _Old_Val = get_data(front(__queue));
                        pop_front(__queue);
-               @Post_check:
-                       _Old_Val == __RET__
+               @Post_check: _Old_Val == __RET__
                @End
        */
        T dequeue()
diff --git a/note.txt b/note.txt
new file mode 100644 (file)
index 0000000..b0fa4a5
--- /dev/null
+++ b/note.txt
@@ -0,0 +1,19 @@
+#1 Some metrics to show how difficult to write specifications for the
+benchmarks.
+ELOC --- Essential Lines of Code (Without counting blanks and comments)
+LOES --- Lines of Essential Specificaitons (Without counting the "/** @Begin" and "@End */")
+SDS --- Sequential Data Structure
+OP --- Ordering Points
+PS --- Pre/post-conditions and SideEffects
+
+Benchmark              ELOC    #API methods    #OP     LOES for SDS    LOES for PS     LOES for OP     LOES for Synchronization        total LOES      LOES (OP + Sync)
+Chase-Lev Deque                92      3               5       27              19              13              6                               65              19
+SPSC Queue             129     2               2       27              7               6               3                               43              9
+ReadCopyUpdate         26      2               2       3               5               6               3                               17              9
+Lockfree Hashtable     421     2               4       44              11              22              5                               82              27
+MCS Lock               151     2               4       3               6               10              1                               20              11
+MPMC Queue             65      4               8       0               0               32              5                               37              37
+M&S Queue              59      2               6       27              10              22              3                               62              25
+Linux RW Lock          90      6               11      6               21              28              10                              65              38
+
+Total                  1033    23              42      137             79              139             36                              391             175