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));
}
@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
@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);
@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);
@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
// 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);
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);
@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;
@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__)
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
/**
@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)
/**
@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)
/**
@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)
/**
@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;
@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)
@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)
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
*/
@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) {
/**
@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) {
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
} 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));
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
*/
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);
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
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;
}
unsigned int get_data(void *wrapper) {
return ((tag_elem_t*) wrapper)->data;
}
- @Happens_before:
- Enqueue -> Dequeue
+ @Happens_before: Enqueue -> Dequeue
@End
*/
@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)
@Action:
T _Old_Val = get_data(front(__queue));
pop_front(__queue);
- @Post_check:
- _Old_Val == __RET__
+ @Post_check: _Old_Val == __RET__
@End
*/
T dequeue()
--- /dev/null
+#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
projects / cdsspec-compiler.git / commitdiff