bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t +
1, memory_order_seq_cst, memory_order_relaxed);
/**
- @Begin
+ //@Begin
@Commit_point_define_check: succ
@Label: Take_CAS_Top
@End
/**
@Begin
- @Additional_ordering_point_define_check: !succ
+ @Additional_ordering_point_define_check: true
@Label: Take_Additional_Point
@End
*/
bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1,
memory_order_seq_cst, memory_order_relaxed);
/**
- @Begin
+ //@Begin
@Commit_point_define_check: succ
@Label: Steal_CAS_Top
@End
/**
@Begin
- @Additional_ordering_point_define_check: !succ
+ @Additional_ordering_point_define_check: true
@Label: Steal_Additional_Point
@End
*/
/**
@Begin
@Interface: Take
- @Commit_point_set: Take_Read_Bottom | Take_CAS_Top |Take_Additional_Point
+ //@Commit_point_set: Take_Read_Bottom | Take_CAS_Top | Take_Additional_Point
+ @Commit_point_set: Take_Read_Bottom | Take_Additional_Point
@ID: __RET__ == EMPTY ? DEFAULT_CALL_ID : get_id(back(__deque))
@Action:
int _Old_Val = EMPTY;
/**
@Begin
@Interface: Steal
- @Commit_point_set: Steal_Read_Bottom | Steal_CAS_Top | Steal_Additional_Point
+ //@Commit_point_set: Steal_Read_Bottom | Steal_CAS_Top | Steal_Additional_Point
+ @Commit_point_set: Steal_Read_Bottom | Steal_Additional_Point
@ID: (__RET__ == EMPTY || __RET__ == ABORT) ? DEFAULT_CALL_ID : get_id(front(__deque))
@Action:
int _Old_Val = EMPTY;
int c;
static void task(void * param) {
- //a=steal(q);
a=steal(q);
if (a == ABORT) {
printf("Steal NULL\n");
} else {
printf("Steal %d\n", a);
}
+ int x=steal(q);
+ if (x == ABORT) {
+ printf("Steal NULL\n");
+ } else {
+ printf("Steal %d\n", x);
+ }
}
int user_main(int argc, char **argv)