From: Peizhao Ou Date: Wed, 4 Dec 2013 03:28:36 +0000 (-0800) Subject: tweak X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=0a6651b877d4303c94fb0a2a9c5632acbd574f32 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(); id_map = spec_hashtable(); 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 #include -#include #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 -using namespace std; -/** - @Begin - @Global_define: - @DeclareStruct: - typedef struct tag_elem { - Tag id; - unsigned int data; - } tag_elem_t; - - @DeclareVar: - list __queue; - Tag tag; - @InitVar: - __queue = list(); - 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 __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 -#include -#include - -#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, ¶m[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 -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 __queue; - Tag tag; + spec_list *__queue; + id_tag_t *tag; @InitVar: - __queue = list(); - 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") };