From: Peizhao Ou <peizhaoo@uci.edu>
Date: Tue, 17 Mar 2015 01:35:44 +0000 (-0700)
Subject: changes
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=7a518b9b39c286f0e6904d4573be3545d232e36e;p=model-checker-benchmarks.git

changes
---

diff --git a/Makefile b/Makefile
index b681de1..e89a8f2 100644
--- a/Makefile
+++ b/Makefile
@@ -1,6 +1,6 @@
 DIRS := barrier mcs-lock mpmc-queue spsc-queue spsc-bugfix linuxrwlocks \
 	dekker-fences chase-lev-deque ms-queue chase-lev-deque-bugfix \
-	concurrent-hashmap seqlock
+	concurrent-hashmap seqlock spsc-example
 
 .PHONY: $(DIRS)
 
diff --git a/spsc-example/queue.h b/spsc-example/queue.h
index 76430e7..94f98e2 100644
--- a/spsc-example/queue.h
+++ b/spsc-example/queue.h
@@ -1,14 +1,16 @@
 #include <unrelacy.h>
 #include <atomic>
+#include "wildcard.h"
 
 using namespace std;
 
 struct node {
-	node(int d): data(d) {
-		next.store(0, memory_order_relaxed);
+	node(int d) {
+		data.store(0, memory_order_normal);
+		next.store(0, wildcard(1));
 	}
 	atomic<node*> next;
-	int data;
+	atomic_int data;
 };
 
 class spsc_queue
@@ -21,18 +23,18 @@ class spsc_queue
 
 	void enqueue(int val) {
 		node* n = new node(val);
-		node *h = head.load(memory_order_relaxed); 
-		h->next.store(n, memory_order_release);
-		head.store(n, memory_order_relaxed);
+		node *h = head.load(wildcard(2)); 
+		h->next.store(n, wildcard(3));
+		head.store(n, wildcard(4));
 	}
 
 	bool dequeue(int *v) {
-		node* t = tail.load(memory_order_relaxed);
-		node* n = t->next.load(memory_order_acquire);
+		node* t = tail.load(wildcard(5));
+		node* n = t->next.load(wildcard(6));
 		if (0 == n)
 			return false;
-		*v = n->data;
-		tail.store(n, memory_order_relaxed);
+		*v = n->data.load(memory_order_normal);
+		tail.store(n, wildcard(7));
 		delete (t);
 		return true;
 	}
diff --git a/spsc-example/spsc-queue.cc b/spsc-example/spsc-queue.cc
index dc2a53c..9f688c4 100644
--- a/spsc-example/spsc-queue.cc
+++ b/spsc-example/spsc-queue.cc
@@ -1,40 +1,38 @@
 #include <threads.h>
 #include <atomic>
 
-//#include "queue.h"
+#include "wildcard.h" 
 
 using namespace std;
-#define acquire memory_order_acquire
-#define release memory_order_release
-#define relaxed memory_order_relaxed
 
 struct node {
-	node(int d): data(d) {
-		next.store(0, relaxed);
+	node(int d) {
+		data.store(d, memory_order_normal);
+		next.store(0, wildcard(1));
 	}
 	atomic<node*> next;
-	int data;
+	atomic_int data;
 };
 
 class spsc_queue { 
 	atomic<node*> head, tail;/*@ \label{line:spscBegin} @*/
 	public:
 	spsc_queue() {
-		head = tail = new node(0);
+		head = tail = new node(-1);
 	}
 	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);
+		node *h = head.load(wildcard(2)); 
+		h->next.store(n, wildcard(3));/*@ \label{line:spscRelease} @*/
+		head.store(n, wildcard(4));
 	}
 	bool dequeue(int *v) {
-		node* t = tail.load(relaxed);
-		node* n = t->next.load(acquire);/*@ \label{line:spscAcquire} @*/
+		node* t = tail.load(wildcard(5));
+		node* n = t->next.load(wildcard(6));/*@ \label{line:spscAcquire} @*/
 		if (0 == n)
 			return false;
-		*v = n->data;
-		tail.store(n, relaxed);
+		*v = n->data.load(memory_order_normal);
+		tail.store(n, wildcard(7));
 		delete (t);
 		return true;
 	}