4 void spsc_queue<T>::enqueue(T data)
6 node* n = new node (data);
7 /********** Detected Correctness **********/
8 //head($)->next.store(n, std::memory_order_release);
9 head->next.store(n, std::memory_order_release);
10 /** @OPDefine: true */
17 T spsc_queue<T>::dequeue()
19 T data = try_dequeue();
35 T spsc_queue<T>::try_dequeue()
39 /********** Detected Correctness **********/
40 node* n = t->next.load(std::memory_order_acquire);
41 /** @OPClearDefine: true */
44 //T data = n->data($);
51 /** @DeclareState: IntList *q; */
53 /** @Transition: STATE(q)->push_back(data); */
54 void enqueue(spsc_queue<int> *q, int data) {
58 /** @PreCondition: return STATE(q)->empty() ? !C_RET : STATE(q)->front() == C_RET;
59 @Transition: if (!C_RET) STATE(q)->pop_front(); */
60 int dequeue(spsc_queue<int> *q) {