From: Peizhao Ou Date: Thu, 22 Jan 2015 23:22:59 +0000 (-0800) Subject: changes with lines of spec counted X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=7f2fd73fe54a04e0f795e7b8f6e28b3a7708df03;p=cdsspec-compiler.git changes with lines of spec counted --- diff --git a/benchmark/chase-lev-deque-bugfix/deque.h b/benchmark/chase-lev-deque-bugfix/deque.h index 0e2fb2b..837df89 100644 --- a/benchmark/chase-lev-deque-bugfix/deque.h +++ b/benchmark/chase-lev-deque-bugfix/deque.h @@ -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 diff --git a/benchmark/cliffc-hashtable/cliffc_hashtable.h b/benchmark/cliffc-hashtable/cliffc_hashtable.h index 1160c13..c09b7a1 100644 --- a/benchmark/cliffc-hashtable/cliffc_hashtable.h +++ b/benchmark/cliffc-hashtable/cliffc_hashtable.h @@ -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 diff --git a/benchmark/linuxrwlocks/linuxrwlocks.c b/benchmark/linuxrwlocks/linuxrwlocks.c index 936a16a..b97c45b 100644 --- a/benchmark/linuxrwlocks/linuxrwlocks.c +++ b/benchmark/linuxrwlocks/linuxrwlocks.c @@ -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) diff --git a/benchmark/mcs-lock/mcs-lock.h b/benchmark/mcs-lock/mcs-lock.h index 46c6530..bf49631 100644 --- a/benchmark/mcs-lock/mcs-lock.h +++ b/benchmark/mcs-lock/mcs-lock.h @@ -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) { diff --git a/benchmark/mpmc-queue/mpmc-queue.h b/benchmark/mpmc-queue/mpmc-queue.h index 6f1bac6..aa10129 100644 --- a/benchmark/mpmc-queue/mpmc-queue.h +++ b/benchmark/mpmc-queue/mpmc-queue.h @@ -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 diff --git a/benchmark/ms-queue/my_queue.h b/benchmark/ms-queue/my_queue.h index ce87b1d..ce6fd06 100644 --- a/benchmark/ms-queue/my_queue.h +++ b/benchmark/ms-queue/my_queue.h @@ -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); diff --git a/benchmark/read-copy-update/rcu.cc b/benchmark/read-copy-update/rcu.cc index b665480..5523882 100644 --- a/benchmark/read-copy-update/rcu.cc +++ b/benchmark/read-copy-update/rcu.cc @@ -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; } diff --git a/benchmark/spsc-bugfix/queue.h b/benchmark/spsc-bugfix/queue.h index 0a38e8f..67be1b7 100644 --- a/benchmark/spsc-bugfix/queue.h +++ b/benchmark/spsc-bugfix/queue.h @@ -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 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