10 data.store(d, memory_order_normal);
11 next.store(0, wildcard(1));
18 atomic<node*> head, tail;/*@ \label{line:spscBegin} @*/
21 head = tail = new node(-1);
23 void enqueue(int val) {
24 node* n = new node(val);
25 node *h = head.load(wildcard(2));
26 h->next.store(n, wildcard(3));/*@ \label{line:spscRelease} @*/
27 head.store(n, wildcard(4));
29 bool dequeue(int *v) {
30 node* t = tail.load(wildcard(5));
31 node* n = t->next.load(wildcard(6));/*@ \label{line:spscAcquire} @*/
34 *v = n->data.load(memory_order_normal);
35 tail.store(n, wildcard(7));
42 spsc_queue *q;/*@ \label{line:testcaseBegin} @*/
44 void thrd1() { // Thread 1/*@ \label{line:thrd1} @*/
45 arr[1].store(47, relaxed);
48 void thrd2() { // Thread 2/*@ \label{line:thrd2} @*/
51 arr[idx].load(relaxed);
54 int user_main(int argc, char **argv)
58 thrd_create(&A, (thrd_start_t)&thrd1, NULL);
59 thrd_create(&B, (thrd_start_t)&thrd2, NULL);