From: Peizhao Ou <peizhaoo@uci.edu>
Date: Wed, 11 Feb 2015 02:11:00 +0000 (-0800)
Subject: edits
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=faf43225ff0d1a0091f5e489714de0c26d24d02f;p=model-checker-benchmarks.git

edits
---

diff --git a/benchmarks.mk b/benchmarks.mk
index 7f82f92..819248e 100644
--- a/benchmarks.mk
+++ b/benchmarks.mk
@@ -9,7 +9,7 @@ LIB_NAME = model
 LIB_SO = lib$(LIB_NAME).so
 
 BASE = ../..
-INCLUDE = -I$(BASE)/include -I../include
+INCLUDE = -I$(BASE)/include -I../include -I$(BASE)/scfence -I$(BASE)
 
 # C preprocessor flags
 CPPFLAGS += $(INCLUDE) -g
diff --git a/concurrent-hashmap/Makefile b/concurrent-hashmap/Makefile
index 4db5bca..d39e831 100644
--- a/concurrent-hashmap/Makefile
+++ b/concurrent-hashmap/Makefile
@@ -1,11 +1,17 @@
 include ../benchmarks.mk
 
-TESTS := table 
+TESTS := table table_wildcard1
 
 all: $(TESTS)
 
 table: main.cc hashmap.h
 	$(CXX) -o $@ $^ $(SPEC_OBJ) $(CXXFLAGS) -std=c++0x $(LDFLAGS)
 
+table_wildcard1: main_wildcard1.cc hashmap_wildcard.h
+	$(CXX) -o $@ $^ $(SPEC_OBJ) $(CXXFLAGS) -std=c++0x $(LDFLAGS)
+
+table_wildcard2: main_wildcard1.cc hashmap_wildcard.h
+	$(CXX) -o $@ $^ $(SPEC_OBJ) $(CXXFLAGS) -std=c++0x $(LDFLAGS)
+
 clean:
 	rm -f *.o *.d $(TESTS)
diff --git a/concurrent-hashmap/hashmap.h b/concurrent-hashmap/hashmap.h
index a66005c..936f284 100644
--- a/concurrent-hashmap/hashmap.h
+++ b/concurrent-hashmap/hashmap.h
@@ -14,7 +14,7 @@
 #include <stdlib.h>
 #include <mutex>
 
-#include "cdsannotate.h"
+#include "sc_annotation.h"
 
 #define relaxed memory_order_relaxed
 #define release memory_order_release
@@ -164,7 +164,11 @@ class HashMap {
 		// lock, we ignore this operation for the SC analysis, and otherwise we
 		// take it into consideration
 		
+		SC_BEGIN();
 		Entry *firstPtr = first->load(acquire);
+		SC_KEEP();
+		SC_END();
+
 		e = firstPtr;
 		while (e != NULL) {
 			if (e->hash == hash && eq(key, e->key)) {
diff --git a/concurrent-hashmap/hashmap_wildcard.h b/concurrent-hashmap/hashmap_wildcard.h
new file mode 100644
index 0000000..557a918
--- /dev/null
+++ b/concurrent-hashmap/hashmap_wildcard.h
@@ -0,0 +1,307 @@
+#ifndef _HASHMAP_H
+#define _HASHMAP_H
+
+#include <iostream>
+#include <atomic>
+#include "stdio.h" 
+//#include <common.h>
+#ifdef STANDALONE
+#include <assert.h>
+#define MODEL_ASSERT assert 
+#else
+#include <model-assert.h>
+#endif
+#include <stdlib.h>
+#include <mutex>
+
+#include "sc_annotation.h"
+#include "wildcard.h"
+
+#define relaxed memory_order_relaxed
+#define release memory_order_release
+#define acquire memory_order_acquire
+#define acq_rel memory_order_acq_rel
+#define seq_cst memory_order_seq_cst
+
+using namespace std;
+
+/**
+	For the sake of simplicity, we do not use template but some toy structs to
+	represent the Key and Value.
+*/
+struct Key {
+	// Probably represent the coordinate (x, y, z)
+	int x;
+	int y;
+	int z;
+
+	int hashCode() {
+		return x + 31 * y + 31 * 31 * z;
+	}
+
+	bool equals(Key *other) {
+		if (!other)
+			return false;
+		return x == other->x && y == other->y && z == other->z;
+	}
+
+	Key(int x, int y, int z) :
+		x(x),
+		y(y),
+		z(z)
+	{
+
+	}
+};
+
+struct Value {
+	// Probably represent the speed vector (vX, vY, vZ)
+	int vX;
+	int vY;
+	int vZ;
+
+	Value(int vX, int vY, int vZ) :
+		vX(vX),
+		vY(vY),
+		vZ(vZ)
+	{
+
+	}
+
+	bool equals(Value *other) {
+		if (!other)
+			return false;
+		return vX == other->vX && vY == other->vY && vZ == other->vZ;
+	}
+};
+
+class Entry {
+	public:
+	Key *key;
+	atomic<Value*> value;
+	int hash;
+	atomic<Entry*> next;
+
+	Entry(int h, Key *k, Value *v, Entry *n) {
+		this->hash = h;
+		this->key = k;
+		this->value.store(v, wildcard(1)); // relaxed
+		this->next.store(n, wildcard(2)); // relaxed
+	}
+};
+
+class Segment {
+	public:
+	int count;
+	mutex segMutex;
+
+	void lock() {
+		segMutex.lock();
+	}
+
+	void unlock() {
+		segMutex.unlock();
+	}
+
+	Segment() {
+		this->count = 0;
+	}
+};
+
+class HashMap {
+	public:
+	atomic<Entry*> *table;
+
+	int capacity;
+	int size;
+
+	static const int CONCURRENCY_LEVEL = 16;
+
+	static const int SEGMENT_MASK = CONCURRENCY_LEVEL - 1;
+
+	Segment *segments[CONCURRENCY_LEVEL];
+
+	static const int DEFAULT_INITIAL_CAPACITY = 16;
+
+	// Not gonna consider resize now...
+	
+	HashMap() {
+		this->size = 0;
+		this->capacity = DEFAULT_INITIAL_CAPACITY;
+		this->table = new atomic<Entry*>[capacity];
+		for (int i = 0; i < capacity; i++) {
+			atomic_init(&table[i], NULL);
+		}
+		for (int i = 0; i < CONCURRENCY_LEVEL; i++) {
+			segments[i] = new Segment;
+		}
+	}
+
+	int hashKey(Key *x) {
+		int h = x->hashCode();
+		// Use logical right shift
+		unsigned int tmp = (unsigned int) h;
+		return ((h << 7) - h + (tmp >> 9) + (tmp >> 17));
+	}
+
+	bool eq(Key *x, Key *y) {
+		return x == y || x->equals(y);
+	}
+
+	Value* get(Key *key) {
+		MODEL_ASSERT (key);
+		int hash = hashKey(key);
+
+		// Try first without locking...
+		atomic<Entry*> *tab = table;
+		int index = hash & (capacity - 1);
+		atomic<Entry*> *first = &tab[index];
+		Entry *e;
+		Value *res = NULL;
+
+		// Should be a load acquire
+		// This load action here makes it problematic for the SC analysis, what
+		// we need to do is as follows: if the get() method ever acquires the
+		// lock, we ignore this operation for the SC analysis, and otherwise we
+		// take it into consideration
+		
+		SC_BEGIN();
+		Entry *firstPtr = first->load(wildcard(3)); // acquire
+		SC_KEEP();
+		SC_END();
+
+		e = firstPtr;
+		while (e != NULL) {
+			if (e->hash == hash && eq(key, e->key)) {
+				res = e->value.load(wildcard(4)); // seq_cst
+				if (res != NULL)
+					return res;
+				else
+					break;
+				// Loading the next entry
+				e = e->next.load(wildcard(5)); // acquire
+			}
+		}
+	
+		// Recheck under synch if key apparently not there or interference
+		Segment *seg = segments[hash & SEGMENT_MASK];
+		seg->lock(); // Critical region begins
+		// Not considering resize now, so ignore the reload of table...
+
+		// Synchronized by locking, no need to be load acquire
+		Entry *newFirstPtr = first->load(wildcard(6)); // relaxed
+		if (e != NULL || firstPtr != newFirstPtr) {
+			e = newFirstPtr;
+			while (e != NULL) {
+				if (e->hash == hash && eq(key, e->key)) {
+					res = e->value.load(wildcard(7)); // seq_cst
+					seg->unlock(); // Critical region ends
+					return res;
+				}
+				// Synchronized by locking
+				e = e->next.load(wildcard(8)); // relaxed
+			}
+		}
+		seg->unlock(); // Critical region ends
+		return NULL;
+	}
+
+	Value* put(Key *key, Value *value) {
+		// Don't allow NULL key or value
+		MODEL_ASSERT (key && value);
+
+		int hash = hashKey(key);
+		Segment *seg = segments[hash & SEGMENT_MASK];
+		atomic<Entry*> *tab;
+
+		seg->lock(); // Critical region begins
+		tab = table;
+		int index = hash & (capacity - 1);
+
+		atomic<Entry*> *first = &tab[index];
+		Entry *e;
+		Value *oldValue = NULL;
+	
+		// The written of the entry is synchronized by locking
+		Entry *firstPtr = first->load(wildcard(9)); // relaxed
+		e = firstPtr;
+		while (e != NULL) {
+			if (e->hash == hash && eq(key, e->key)) {
+				// FIXME: This could be a relaxed (because locking synchronize
+				// with the previous put())?? 
+				oldValue = e->value.load(wildcard(10)); // acquire
+				e->value.store(value, wildcard(11)); // seq_cst
+				seg->unlock(); // Don't forget to unlock before return
+				return oldValue;
+			}
+			// Synchronized by locking
+			e = e->next.load(wildcard(12)); // relaxed
+		}
+
+		// Add to front of list
+		Entry *newEntry = new Entry(hash, key, value, firstPtr);
+		// Publish the newEntry to others
+		first->store(newEntry, wildcard(13)); // release
+		seg->unlock(); // Critical region ends
+		return NULL;
+	}
+
+	Value* remove(Key *key, Value *value) {
+		MODEL_ASSERT (key);
+		int hash = hashKey(key);
+		Segment *seg = segments[hash & SEGMENT_MASK];
+		atomic<Entry*> *tab;
+
+		seg->lock(); // Critical region begins
+		tab = table;
+		int index = hash & (capacity - 1);
+
+		atomic<Entry*> *first = &tab[index];
+		Entry *e;
+		Value *oldValue = NULL;
+	
+		// The written of the entry is synchronized by locking
+		Entry *firstPtr = first->load(relaxed);
+		e = firstPtr;
+
+		while (true) {
+			if (e != NULL) {
+				seg->unlock(); // Don't forget to unlock
+				return NULL;
+			}
+			if (e->hash == hash && eq(key, e->key))
+				break;
+			// Synchronized by locking
+			e = e->next.load(relaxed);
+		}
+
+		// FIXME: This could be a relaxed (because locking synchronize
+		// with the previous put())?? 
+		oldValue = e->value.load(acquire);
+		// If the value parameter is NULL, we will remove the entry anyway
+		if (value != NULL && value->equals(oldValue)) {
+			seg->unlock();
+			return NULL;
+		}
+
+		// Force the get() to grab the lock and retry
+		e->value.store(NULL, relaxed);
+
+		// The strategy to remove the entry is to keep the entries after the
+		// removed one and copy the ones before it
+		Entry *head = e->next.load(relaxed);
+		Entry *p;
+		p = first->load(relaxed);
+		while (p != e) {
+			head = new Entry(p->hash, p->key, p->value.load(relaxed), head);
+			p = p->next.load(relaxed);
+		}
+
+		// Publish the new head to readers 
+		first->store(head, release);
+		seg->unlock(); // Critical region ends
+		return oldValue;
+	}
+};
+
+#endif
diff --git a/concurrent-hashmap/main_wildcard.cc b/concurrent-hashmap/main_wildcard.cc
new file mode 100644
index 0000000..4a6f904
--- /dev/null
+++ b/concurrent-hashmap/main_wildcard.cc
@@ -0,0 +1,58 @@
+#include <iostream>
+#include <threads.h>
+#include "hashmap_wildcard.h"
+
+HashMap *table;
+
+Key *k1, *k2;
+Value *r1, *r2, *r3, *r4, *v1, *v2;
+
+void printKey(Key *key) {
+	if (key)
+		printf("pos = (%d, %d, %d)\n", key->x, key->y, key->z);
+	else
+		printf("pos = NULL\n");
+}
+
+void printValue(Value *value) {
+	if (value)
+		printf("velocity = (%d, %d, %d)\n", value->vX, value->vY, value->vZ);
+	else
+		printf("velocity = NULL\n");
+}
+
+void threadA(void *arg) {
+	k1 = new Key(1, 1, 1);
+	k2 = new Key(3, 4, 5);
+	v1 = new Value(10, 10, 10);
+	r1 = table->put(k1, v1);
+	//printValue(r1);
+	r2 = table->get(k2);
+	printf("Thrd A:\n");
+	printValue(r2);
+}
+
+void threadB(void *arg) {
+	k1 = new Key(1, 1, 1);
+	k2 = new Key(3, 4, 5);
+	v2 = new Value(30, 40, 50);
+	r3 = table->put(k2, v2);
+	//printValue(r3);
+	r4 = table->get(k1);
+	printf("Thrd B:\n");
+	printValue(r4);
+}
+
+int user_main(int argc, char *argv[]) {
+	thrd_t t1, t2;
+	table = new HashMap;
+
+	thrd_create(&t1, threadA, NULL);
+	thrd_create(&t2, threadB, NULL);
+	thrd_join(t1);
+	thrd_join(t2);
+	
+	return 0;
+}
+
+
diff --git a/mpmc-queue/note.txt b/mpmc-queue/note.txt
new file mode 100644
index 0000000..e8597d3
--- /dev/null
+++ b/mpmc-queue/note.txt
@@ -0,0 +1,20 @@
+#1 Why this data structure is non-SC (but it's SC at abstraction).
+
+The underlying pattern of the non-SCness are as the following:
+
+T1				T2
+x = 1;			y = 1;
+r1 = y;			r2 = x;
+
+Suppose there are two identical threads, both having a writer followed by a
+reader, as follows:
+
+T1							T2
+m_written.CAS;				m_rdwr.CAS;
+
+m_rdwr.CAS;					m_written.CAS; // In write_publish()
+
+m_written.load; // a		m_rdwr.load; // The first in the read_fetch() // b
+
+a & b can both read old value and it's non-SC. However, the later loads and CAS
+in the loops will finally fix this problem.