From: Peizhao Ou <peizhaoo@uci.edu>
Date: Wed, 4 Mar 2015 20:23:57 +0000 (-0800)
Subject: changes to the example
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=c465f23ec3cc17ca6396ec4da0ff67a574eb6f50;p=model-checker-benchmarks.git

changes to the example
---

diff --git a/spsc-example/spsc-queue.cc b/spsc-example/spsc-queue.cc
index cfb34ec..dc2a53c 100644
--- a/spsc-example/spsc-queue.cc
+++ b/spsc-example/spsc-queue.cc
@@ -1,37 +1,68 @@
 #include <threads.h>
+#include <atomic>
 
-#include "queue.h"
+//#include "queue.h"
 
-spsc_queue *q;
-atomic_int arr[2];
+using namespace std;
+#define acquire memory_order_acquire
+#define release memory_order_release
+#define relaxed memory_order_relaxed
 
-void thread(unsigned thread_index)
-{
-	if (0 == thread_index)
-	{
-		arr[1].store(memory_order_relaxed);
-		q->enqueue(1);
+struct node {
+	node(int d): data(d) {
+		next.store(0, relaxed);
+	}
+	atomic<node*> next;
+	int data;
+};
+
+class spsc_queue { 
+	atomic<node*> head, tail;/*@ \label{line:spscBegin} @*/
+	public:
+	spsc_queue() {
+		head = tail = new node(0);
+	}
+	void enqueue(int val) {
+		node* n = new node(val);
+		node *h = head.load(relaxed); 
+		h->next.store(n, release);/*@ \label{line:spscRelease} @*/
+		head.store(n, relaxed);
 	}
-	else
-	{
-		int val = 0;
-		bool succ = q->dequeue(&val);
-		arr[val].load(memory_order_relaxed);
+	bool dequeue(int *v) {
+		node* t = tail.load(relaxed);
+		node* n = t->next.load(acquire);/*@ \label{line:spscAcquire} @*/
+		if (0 == n)
+			return false;
+		*v = n->data;
+		tail.store(n, relaxed);
+		delete (t);
+		return true;
 	}
+};
+
+
+spsc_queue *q;/*@ \label{line:testcaseBegin} @*/
+atomic_int arr[2];
+void thrd1() { // Thread 1/*@ \label{line:thrd1} @*/
+	arr[1].store(47, relaxed);
+	q->enqueue(1);
+}
+void thrd2() { // Thread 2/*@ \label{line:thrd2} @*/
+	int idx;
+	if (q->dequeue(&idx))
+		arr[idx].load(relaxed);
 }
 
 int user_main(int argc, char **argv)
 {
 	thrd_t A, B;
-
-	q = new spsc_queue();
-
-	thrd_create(&A, (thrd_start_t)&thread, (void *)0);
-	thrd_create(&B, (thrd_start_t)&thread, (void *)1);
+	q = new spsc_queue;
+	thrd_create(&A, (thrd_start_t)&thrd1, NULL);
+	thrd_create(&B, (thrd_start_t)&thrd2, NULL);
 	thrd_join(A);
 	thrd_join(B);
 
-	delete q;
+	//delete q;
 
 	return 0;
 }