From: Brian Norris <banorris@uci.edu>
Date: Tue, 5 Mar 2013 01:00:52 +0000 (-0800)
Subject: deque: add "proven correct" work-stealing Chase-Lev deque
X-Git-Tag: oopsla2013-final~45
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker-benchmarks.git;a=commitdiff_plain;h=e7fb1d3fca70b9f871b961f2f3c3443d4955a3b4

deque: add "proven correct" work-stealing Chase-Lev deque

From the PPoPP 2013 paper "Correct and efficient work-stealing for weak
memory models"

By:

  Nhat Minh Lê
  Antoniu Pop
  Albert Cohen
  Francesco Zappa Nardelli

Citation URL:

  http://dl.acm.org/citation.cfm?id=2442524
---

diff --git a/chase-lev-deque/deque.c b/chase-lev-deque/deque.c
new file mode 100644
index 0000000..956e8e0
--- /dev/null
+++ b/chase-lev-deque/deque.c
@@ -0,0 +1,60 @@
+typedef struct {
+	atomic_size_t size;
+	atomic_int buffer[];
+} Array;
+
+typedef struct {
+	atomic_size_t top, bottom;
+	Atomic(Array *) array;
+} Deque;
+
+int take(Deque *q) {
+	size_t b = load_explicit(&q->bottom, relaxed) - 1;
+	Array *a = load_explicit(&q->array, relaxed);
+	store_explicit(&q->bottom, b, relaxed);
+	thread_fence(seq_cst);
+	size_t t = load_explicit(&q->top, relaxed);
+	int x;
+	if (t <= b) {
+		/* Non-empty queue. */
+		x = load_explicit(&a->buffer[b % a->size], relaxed);
+		if (t == b) {
+			/* Single last element in queue. */
+			if (!compare_exchange_strong_explicit(&q->top, &t, t + 1, seq_cst, relaxed))
+				/* Failed race. */
+				x = EMPTY;
+			store_explicit(&q->bottom, b + 1, relaxed);
+		}
+	} else { /* Empty queue. */
+		x = EMPTY;
+		store_explicit(&q->bottom, b + 1, relaxed);
+	}
+	return x;
+}
+
+void push(Deque *q, int x) {
+	size_t b = load_explicit(&q->bottom, relaxed);
+	size_t t = load_explicit(&q->top, acquire);
+	Array *a = load_explicit(&q->array, relaxed);
+	if (b - t > a->size - 1) /* Full queue. */
+		resize(q);
+	store_explicit(&a->buffer[b % a->size], x, relaxed);
+	thread_fence(release);
+	store_explicit(&q->bottom, b + 1, relaxed);
+}
+
+int steal(Deque *q) {
+	size_t t = load_explicit(&q->top, acquire);
+	thread_fence(seq_cst);
+	size_t b = load_explicit(&q->bottom, acquire);
+	int x = EMPTY;
+	if (t < b) {
+		/* Non-empty queue. */
+		Array *a = load_explicit(&q->array, relaxed);
+		x = load_explicit(&a->buffer[t % a->size], relaxed);
+		if (!compare_exchange_strong_explicit(&q->top, &t, t + 1, seq_cst, relaxed))
+			/* Failed race. */
+			return ABORT;
+	}
+	return x;
+}