From: Peizhao Ou <peizhaoo@uci.edu>
Date: Wed, 4 Dec 2013 03:28:36 +0000 (-0800)
Subject: tweak
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=0a6651b877d4303c94fb0a2a9c5632acbd574f32;p=cdsspec-compiler.git

tweak
---

diff --git a/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h b/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h
index a52d238..d30c4ab 100644
--- a/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h
+++ b/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h
@@ -95,14 +95,16 @@ class cliffc_hashtable {
 				map = spec_hashtable<TypeK, TypeV*>();
 				id_map = spec_hashtable<TypeK, TypeV*>();
 				tag = Tag();
-			static bool equals_val(TypeV *ptr1, TypeV *ptr2) {
+			@DefineFunc:
+			bool equals_val(TypeV *ptr1, TypeV *ptr2) {
 				// ...
 			}
 			
+			@DefineFunc:
 			# Update the tag for the current key slot if the corresponding tag
 			# is NULL, otherwise just return that tag. It will update the next
 			# available tag too if it requires a new tag for that key slot.
-			static Tag getKeyTag(TypeK &key) {
+			Tag getKeyTag(TypeK &key) {
 				if (id_map.get(key) == NULL) {
 					Tag cur_tag = tag.current();
 					id_map.put(key, cur_tag);
diff --git a/benchmark/ms-queue/my_queue.c b/benchmark/ms-queue/my_queue.c
index 3b1784b..9db5efe 100644
--- a/benchmark/ms-queue/my_queue.c
+++ b/benchmark/ms-queue/my_queue.c
@@ -1,63 +1,9 @@
 #include <threads.h>
 #include <stdlib.h>
-#include <stdatomic.h>
 #include "librace.h"
 #include "model-assert.h"
 
-
-typedef unsigned long long pointer;
-typedef atomic_ullong pointer_t;
-
-#define MAKE_POINTER(ptr, count)	((((pointer)count) << 32) | ptr)
-#define PTR_MASK 0xffffffffLL
-#define COUNT_MASK (0xffffffffLL << 32)
-
-static inline void set_count(pointer *p, unsigned int val) { *p = (*p & ~COUNT_MASK) | ((pointer)val << 32); }
-static inline void set_ptr(pointer *p, unsigned int val) { *p = (*p & ~PTR_MASK) | val; }
-static inline unsigned int get_count(pointer p) { return (p & COUNT_MASK) >> 32; }
-static inline unsigned int get_ptr(pointer p) { return p & PTR_MASK; }
-
-typedef struct node {
-	unsigned int value;
-	pointer_t next;
-} node_t;
-
-typedef struct {
-	pointer_t head;
-	pointer_t tail;
-	node_t nodes[MAX_NODES + 1];
-} queue_t;
-
-void init_queue(queue_t *q, int num_threads);
-
-#include <list>
-using namespace std;
-/**
-	@Begin
-	@Global_define:
-		@DeclareStruct:
-		typedef struct tag_elem {
-			Tag id;
-			unsigned int data;
-		} tag_elem_t;
-		
-		@DeclareVar:
-		list<tag_elem_t> __queue;
-		Tag tag;
-		@InitVar:
-			__queue = list<tag_elem_t>();
-			tag = 1; // Beginning of available id
-	@Happens_before:
-		# Only check the happens-before relationship according to the id of the
-		# commit_point_set. For commit_point_set that has same ID, A -> B means
-		# B happens after the previous A.
-		Enqueue -> Dequeue
-	@End
-*/
-
-
-int get_thread_num();
-
+#include "my_queue.h"
 
 #define relaxed memory_order_relaxed
 #define release memory_order_release
@@ -112,17 +58,11 @@ static void reclaim(unsigned int node)
 
 void init_queue(queue_t *q, int num_threads)
 {
-	/**
-		@Begin
-		@Entry_point
-		@End
-	*/
-
 	int i, j;
 
 	/* Initialize each thread's free list with INITIAL_FREE pointers */
 	/* The actual nodes are initialized with poison indexes */
-	free_lists = (unsigned int**) malloc(num_threads * sizeof(*free_lists));
+	free_lists = malloc(num_threads * sizeof(*free_lists));
 	for (i = 0; i < num_threads; i++) {
 		for (j = 0; j < INITIAL_FREE; j++) {
 			free_lists[i][j] = 2 + i * MAX_FREELIST + j;
@@ -138,16 +78,30 @@ void init_queue(queue_t *q, int num_threads)
 
 /**
 	@Begin
-	@Interface: Enqueue
-	@Commit_point_set: Enqueue_Success_Point
-	@ID: tag++
-	@Action:
-		# __ID__ is an internal macro that refers to the id of the current
-		# interface call
-		tag_elem_t elem;
-		elem.id = __ID__;
-		elem.data = val;
-		__queue.push_back(elem);
+	@Global_define:
+		typedef struct tag_elem {
+			Tag id;
+			unsigned int data;
+			
+			tag_elem(Tag _id, unsigned int _data) {
+				id = _id;
+				data = _data;
+			}
+		} tag_elem_t;
+
+		spec_queue<tag_elem_t> __queue;
+		Tag __tag;
+	@Happens_before:
+		# Only check the happens-before relationship according to the id of the
+		# commit_point_set. For commit_point_set that has same ID, A -> B means
+		# B happens after the previous A.
+		Enqueue -> Dequeue
+	@End
+*/
+
+/**
+	@Begin
+	@Interface_define: Enqueue
 	@End
 */
 void enqueue(queue_t *q, unsigned int val)
@@ -202,14 +156,7 @@ void enqueue(queue_t *q, unsigned int val)
 
 /**
 	@Begin
-	@Interface: Dequeue
-	@Commit_point_set: Dequeue_Success_Point
-	@ID: __queue.back().id
-	@Action:
-		unsigned int _Old_Val = __queue.front().data;
-		__queue.pop_front();
-	@Post_check:
-		_Old_Val == __RET__
+	@Interface_define: Dequeue
 	@End
 */
 unsigned int dequeue(queue_t *q)
@@ -258,86 +205,3 @@ unsigned int dequeue(queue_t *q)
 	reclaim(get_ptr(head));
 	return value;
 }
-
-
-
-#include <stdlib.h>
-#include <stdio.h>
-#include <threads.h>
-
-#include "my_queue.h"
-#include "model-assert.h"
-
-static int procs = 2;
-static queue_t *queue;
-static thrd_t *threads;
-static unsigned int *input;
-static unsigned int *output;
-static int num_threads;
-
-int get_thread_num()
-{
-	thrd_t curr = thrd_current();
-	int i;
-	for (i = 0; i < num_threads; i++)
-		if (curr.priv == threads[i].priv)
-			return i;
-	MODEL_ASSERT(0);
-	return -1;
-}
-
-static void main_task(void *param)
-{
-	unsigned int val;
-	int pid = *((int *)param);
-
-	if (!pid) {
-		input[0] = 17;
-		enqueue(queue, input[0]);
-		output[0] = dequeue(queue);
-	} else {
-		input[1] = 37;
-		enqueue(queue, input[1]);
-		output[1] = dequeue(queue);
-	}
-}
-
-int user_main(int argc, char **argv)
-{
-	int i;
-	int *param;
-	unsigned int in_sum = 0, out_sum = 0;
-
-	queue = (queue_t*) calloc(1, sizeof(*queue));
-	MODEL_ASSERT(queue);
-
-	num_threads = procs;
-	threads = (thrd_t*) malloc(num_threads * sizeof(thrd_t));
-	param = (int*) malloc(num_threads * sizeof(*param));
-	input = (unsigned int*) calloc(num_threads, sizeof(*input));
-	output = (unsigned int*) calloc(num_threads, sizeof(*output));
-
-	init_queue(queue, num_threads);
-	for (i = 0; i < num_threads; i++) {
-		param[i] = i;
-		thrd_create(&threads[i], main_task, &param[i]);
-	}
-	for (i = 0; i < num_threads; i++)
-		thrd_join(threads[i]);
-
-	for (i = 0; i < num_threads; i++) {
-		in_sum += input[i];
-		out_sum += output[i];
-	}
-	for (i = 0; i < num_threads; i++)
-		printf("input[%d] = %u\n", i, input[i]);
-	for (i = 0; i < num_threads; i++)
-		printf("output[%d] = %u\n", i, output[i]);
-	MODEL_ASSERT(in_sum == out_sum);
-
-	free(param);
-	free(threads);
-	free(queue);
-
-	return 0;
-}
diff --git a/benchmark/ms-queue/my_queue.h b/benchmark/ms-queue/my_queue.h
index cc10de4..2459b9c 100644
--- a/benchmark/ms-queue/my_queue.h
+++ b/benchmark/ms-queue/my_queue.h
@@ -30,23 +30,41 @@ typedef struct {
 
 void init_queue(queue_t *q, int num_threads);
 
-#include <list>
-using namespace std;
 /**
 	@Begin
 	@Global_define:
 		@DeclareStruct:
 		typedef struct tag_elem {
-			Tag id;
+			call_id_t id;
 			unsigned int data;
 		} tag_elem_t;
 		
 		@DeclareVar:
-		list<tag_elem_t> __queue;
-		Tag tag;
+		spec_list *__queue;
+		id_tag_t *tag;
 		@InitVar:
-			__queue = list<tag_elem_t>();
-			tag = 1; // Beginning of available id
+			__queue = new_spec_list();
+			tag = new_id_tag(); // Beginning of available id
+		@DefineFunc:
+			tag_elem_t* new_tag_elem(call_id_t id, unsigned int data) {
+				tag_elem_t *e = (tag_elem_t*) malloc(sizeof(tag_elem_t));
+				e->id = id;
+				e->data = data;
+				return e;
+			}
+
+			void free_tag_elem(tag_elem_t *e) {
+				free(e);
+			}
+
+			call_id_t get_id(void *wrapper) {
+				return ((tag_elem_t*) wrapper)->id;
+			}
+
+			unsigned int get_data(void *wrapper) {
+				return ((tag_elem_t*) wrapper)->data;
+			}
+
 	@Happens_before:
 		# Only check the happens-before relationship according to the id of the
 		# commit_point_set. For commit_point_set that has same ID, A -> B means
@@ -61,14 +79,12 @@ using namespace std;
 	@Begin
 	@Interface: Enqueue
 	@Commit_point_set: Enqueue_Success_Point
-	@ID: tag++
+	@ID: get_and_inc(tag);
 	@Action:
 		# __ID__ is an internal macro that refers to the id of the current
 		# interface call
-		tag_elem_t elem;
-		elem.id = __ID__;
-		elem.data = val;
-		__queue.push_back(elem);
+		tag_elem_t elem = new_tag_elem(__ID__, val);
+		push_back(__queue, elem);
 	@End
 */
 void enqueue(queue_t *q, unsigned int val);
@@ -77,10 +93,10 @@ void enqueue(queue_t *q, unsigned int val);
 	@Begin
 	@Interface: Dequeue
 	@Commit_point_set: Dequeue_Success_Point
-	@ID: __queue.back().id
+	@ID: get_id(back(__queue))
 	@Action:
-		unsigned int _Old_Val = __queue.front().data;
-		__queue.pop_front();
+		unsigned int _Old_Val = get_data(front(__queue));
+		pop_front(__queue);
 	@Post_check:
 		_Old_Val == __RET__
 	@End
diff --git a/notes/interesting_examples.txt b/notes/interesting_examples.txt
new file mode 100644
index 0000000..e69de29
diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
index 39e3f3b..d38bba7 100644
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
@@ -207,9 +207,9 @@ public class CodeGenerator {
 		String homeDir = Environment.HOME_DIRECTORY;
 		File[] srcFiles = {
 //				new File(Environment.MODEL_CHECKER_TEST_DIR + "/backup_linuxrwlocks.c") };
-		 new File(homeDir + "/benchmark/linuxrwlocks/linuxrwlocks.c") };
-//		new File(homeDir
-//				+ "/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h"), };
+//		 new File(homeDir + "/benchmark/linuxrwlocks/linuxrwlocks.c") };
+		new File(homeDir
+				+ "/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h"), };
 //		 new File(homeDir + "/benchmark/ms-queue/my_queue.c"),
 //		 new File(homeDir + "/benchmark/ms-queue/my_queue.c") };
 //		new File(homeDir + "/benchmark/test/test.c") };