From: Peizhao Ou Date: Tue, 17 Nov 2015 04:12:06 +0000 (-0800) Subject: edits X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=48fb6334c3bc1e63a33a80cce2ab50a08348d272 edits --- diff --git a/benchmark/concurrent-hashmap/Makefile b/benchmark/concurrent-hashmap/Makefile index 4c0a7dc..d379912 100644 --- a/benchmark/concurrent-hashmap/Makefile +++ b/benchmark/concurrent-hashmap/Makefile @@ -1,26 +1,14 @@ include ../benchmarks.mk BENCH := hashmap -NORMAL_TESTS := testcase1 testcase2 - -WILDCARD_TESTS := $(patsubst %, %_wildcard, $(NORMAL_TESTS)) - -TESTS := $(NORMAL_TESTS) $(WILDCARD_TESTS) +TESTS := testcase1 testcase2 all: $(TESTS) -$(WILDCARD_TESTS): CXXFLAGS += -DWILDCARD - $(BENCH).o : $(BENCH).h $(CXX) -o $@ $< $(CXXFLAGS) -c $(LDFLAGS) -$(BENCH)_wildcard.o : $(BENCH)_wildcard.h - $(CXX) -o $@ $< $(CXXFLAGS) -c $(LDFLAGS) - -$(WILDCARD_TESTS): %_wildcard : %.cc $(BENCH)_wildcard.o - $(CXX) -o $@ $< $(CXXFLAGS) $(LDFLAGS) - -$(NORMAL_TESTS): % : %.cc $(BENCH).o +$(TESTS): % : %.cc $(BENCH).o $(CXX) -o $@ $< $(CXXFLAGS) $(LDFLAGS) clean: diff --git a/benchmark/ms-queue/my_queue.c b/benchmark/ms-queue/my_queue.c index e30535c..b8189c9 100644 --- a/benchmark/ms-queue/my_queue.c +++ b/benchmark/ms-queue/my_queue.c @@ -22,11 +22,11 @@ static unsigned int new_node() int i; int t = get_thread_num(); for (i = 0; i < MAX_FREELIST; i++) { - unsigned int node = load_32(&free_lists[t][i]); - //unsigned int node = free_lists[t][i]; + //unsigned int node = load_32(&free_lists[t][i]); + unsigned int node = free_lists[t][i]; if (node) { - store_32(&free_lists[t][i], 0); - //free_lists[t][i] = 0; + //store_32(&free_lists[t][i], 0); + free_lists[t][i] = 0; return node; } } @@ -46,8 +46,8 @@ static void reclaim(unsigned int node) for (i = 0; i < MAX_FREELIST; i++) { /* Should never race with our own thread here */ - unsigned int idx = load_32(&free_lists[t][i]); - //unsigned int idx = free_lists[t][i]; + //unsigned int idx = load_32(&free_lists[t][i]); + unsigned int idx = free_lists[t][i]; /* Found empty spot in free list */ if (idx == 0) { @@ -97,8 +97,8 @@ void enqueue(queue_t *q, unsigned int val) pointer tmp; node = new_node(); - store_32(&q->nodes[node].value, val); - //q->nodes[node].value = val; + //store_32(&q->nodes[node].value, val); + q->nodes[node].value = val; tmp = atomic_load_explicit(&q->nodes[node].next, relaxed); set_ptr(&tmp, 0); // NULL atomic_store_explicit(&q->nodes[node].next, tmp, relaxed); @@ -226,8 +226,8 @@ bool dequeue(queue_t *q, int *retVal) //printf("miss4_dequeue\n"); thrd_yield(); } else { - value = load_32(&q->nodes[get_ptr(next)].value); - //value = q->nodes[get_ptr(next)].value; + //value = load_32(&q->nodes[get_ptr(next)].value); + value = q->nodes[get_ptr(next)].value; /**** correctness error ****/ success = atomic_compare_exchange_strong_explicit(&q->head, &head, diff --git a/benchmark/ms-queue/my_queue.h b/benchmark/ms-queue/my_queue.h index 2da355a..3d54e77 100644 --- a/benchmark/ms-queue/my_queue.h +++ b/benchmark/ms-queue/my_queue.h @@ -42,52 +42,19 @@ void init_queue(queue_t *q, int num_threads); @Options: LANG = C; @Global_define: - @DeclareStruct: - typedef struct tag_elem { - call_id_t id; - unsigned int data; - } tag_elem_t; - @DeclareVar: - spec_list *__queue; - id_tag_t *tag; + IntegerList *__queue; @InitVar: - __queue = new_spec_list(); - tag = new_id_tag(); // Beginning of available id - //@Cleanup: - // if (__queue) - // free_spec_list(__queue); - // if (tag) - // free_id_tag(tag); - @DefineFunc: - tag_elem_t* new_tag_elem(call_id_t id, unsigned int data) { - tag_elem_t *e = (tag_elem_t*) CMODEL_MALLOC(sizeof(tag_elem_t)); - e->id = id; - e->data = data; - return e; - } - //@DefineFunc: - // void free_tag_elem(tag_elem_t *e) { - // free(e); - // } - @DefineFunc: - call_id_t get_id(void *wrapper) { - // if (wrapper == NULL) - // return 0; - // return ((tag_elem_t*) wrapper)->id; - return wrapper == NULL ? 0 : ((tag_elem_t*) wrapper)->id; - } - @DefineFunc: - unsigned int get_data(void *wrapper) { - return ((tag_elem_t*) wrapper)->data; - } + __queue = createIntegerList(); + @Finalize: + if (__queue) + destroyIntegerList(__queue); + return true; @Happens_before: Enqueue -> Dequeue - # 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. @Commutativity: Enqueue <-> Dequeue: true - @Commutativity: Enqueue <-> Enqueue: _Method1.q != _Method2.q - @Commutativity: Dequeue <-> Dequeue: _Method1.q != _Method2.q + @Commutativity: Dequeue <-> Dequeue: !_Method1.__RET__ || !_Method2.__RET__ + //@Commutativity: Enqueue <-> Enqueue: _Method1.q != _Method2.q + //@Commutativity: Dequeue <-> Dequeue: _Method1.q != _Method2.q @End */ @@ -97,13 +64,12 @@ void init_queue(queue_t *q, int num_threads); @Begin @Interface: Enqueue @Commit_point_set: EnqueueUpdateNext - @ID: get_and_inc(tag) + @ID: val @Action: # __ID__ is an internal macro that refers to the id of the current # interface call - tag_elem_t *elem = new_tag_elem(__ID__, val); - push_back(__queue, elem); - //model_print("Enqueue: input=%d\n", val); + push_back(__queue, val); + //model_print("Enqueue: val=%d\n", val); @End */ void enqueue(queue_t *q, unsigned int val); @@ -112,15 +78,16 @@ void enqueue(queue_t *q, unsigned int val); @Begin @Interface: Dequeue @Commit_point_set: DequeueReadHead | DequeueUpdateHead | DequeueReadNextVerify - @ID: get_id(front(__queue)) + @ID: __RET__ ? *retVal : 0 @Action: - unsigned int _Old_Val = 0; - if (size(__queue) > 0) { - _Old_Val = get_data(front(__queue)); + int elem = 0; + if (__RET__) { + elem = front(__queue); pop_front(__queue); } - // model_print("Dequeue: __RET__=%d, retVal=%d, Old_Val=%d\n", __RET__, *retVal, _Old_Val); - @Post_check: _Old_Val == 0 ? !__RET__ : _Old_Val == *retVal + //model_print("Dequeue: __RET__=%d, retVal=%d, elem=%d, \n", __RET__, *retVal, elem); + //model_print("Result: %d\n", __RET__ ? *retVal == elem : true); + @Post_check: __RET__ ? *retVal == elem : true @End */ bool dequeue(queue_t *q, int *retVal); diff --git a/benchmark/ms-queue/testcase1.c b/benchmark/ms-queue/testcase1.c index 0e5b20d..8987567 100644 --- a/benchmark/ms-queue/testcase1.c +++ b/benchmark/ms-queue/testcase1.c @@ -35,9 +35,9 @@ static void main_task(void *param) output1 = 1; succ1 = dequeue(queue, &output1); if (succ1) - printf("Thrd 2: Dequeue %d.\n", output1); + printf("Thrd 1: Dequeue %d.\n", output1); else - printf("Thrd 2: Dequeue NULL.\n"); + printf("Thrd 1: Dequeue NULL.\n"); } else if (pid % 4 == 1) { enqueue(queue, 2); } diff --git a/grammer/spec_compiler.jj b/grammer/spec_compiler.jj index 62b098e..9195e13 100644 --- a/grammer/spec_compiler.jj +++ b/grammer/spec_compiler.jj @@ -373,7 +373,7 @@ SKIP : { | | - + | | diff --git a/output/ms-queue/testcase1.c b/output/ms-queue/testcase1.c new file mode 100644 index 0000000..8731a0e --- /dev/null +++ b/output/ms-queue/testcase1.c @@ -0,0 +1,75 @@ +#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; + return -1; +} + + +bool succ1, succ2; +unsigned int output1, output2; + +static void main_task(void *param) +{ + int pid = *((int *)param); + if (pid % 4 == 0) { + output1 = 1; + succ1 = dequeue(queue, &output1); + if (succ1) + printf("Thrd 1: Dequeue %d.\n", output1); + else + printf("Thrd 1: Dequeue NULL.\n"); + } else if (pid % 4 == 1) { + enqueue(queue, 2); + } +} + +int user_main(int argc, char **argv) +{ + __sequential_init(); + + int i; + int *param; + unsigned int in_sum = 0, out_sum = 0; + + queue = calloc(1, sizeof(*queue)); + + num_threads = procs; + threads = malloc(num_threads * sizeof(thrd_t)); + param = malloc(num_threads * sizeof(*param)); + input = calloc(num_threads, sizeof(*input)); + output = 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]); + + + free(param); + free(threads); + free(queue); + + return 0; +} + diff --git a/output/ms-queue/testcase2.c b/output/ms-queue/testcase2.c new file mode 100644 index 0000000..f5b2133 --- /dev/null +++ b/output/ms-queue/testcase2.c @@ -0,0 +1,81 @@ +#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; + return -1; +} + + +bool succ1, succ2; +unsigned int output1, output2; + +static void main_task(void *param) +{ + int pid = *((int *)param); + if (pid % 4 == 0) { + output1 = 1; + succ1 = dequeue(queue, &output1); + if (succ1) + printf("Thrd 1: Dequeue %d.\n", output1); + else + printf("Thrd 1: Dequeue NULL.\n"); + } else if (pid % 4 == 1) { + enqueue(queue, 2); + output2 = 1; + succ2 = dequeue(queue, &output2); + if (succ2) + printf("Thrd 2: Dequeue %d.\n", output2); + else + printf("Thrd 2: Dequeue NULL.\n"); + } +} + +int user_main(int argc, char **argv) +{ + __sequential_init(); + + int i; + int *param; + unsigned int in_sum = 0, out_sum = 0; + + queue = calloc(1, sizeof(*queue)); + + num_threads = procs; + threads = malloc(num_threads * sizeof(thrd_t)); + param = malloc(num_threads * sizeof(*param)); + input = calloc(num_threads, sizeof(*input)); + output = 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]); + + + free(param); + free(threads); + free(queue); + + return 0; +} +