edits
authorPeizhao Ou <peizhaoo@uci.edu>
Tue, 17 Nov 2015 04:12:06 +0000 (20:12 -0800)
committerPeizhao Ou <peizhaoo@uci.edu>
Tue, 17 Nov 2015 04:12:06 +0000 (20:12 -0800)
benchmark/concurrent-hashmap/Makefile
benchmark/ms-queue/my_queue.c
benchmark/ms-queue/my_queue.h
benchmark/ms-queue/testcase1.c
grammer/spec_compiler.jj
output/ms-queue/testcase1.c [new file with mode: 0644]
output/ms-queue/testcase2.c [new file with mode: 0644]

index 4c0a7dc..d379912 100644 (file)
@@ -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:
index e30535c..b8189c9 100644 (file)
@@ -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,
index 2da355a..3d54e77 100644 (file)
@@ -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);
index 0e5b20d..8987567 100644 (file)
@@ -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);
        }
index 62b098e..9195e13 100644 (file)
@@ -373,7 +373,7 @@ SKIP : {
 |
        <INIT_VAR: "@InitVar:">
 |
-       <CLEANUP: "@Cleanup:">
+       <CLEANUP: "@Finalize:">
 |
        <DEFINE_FUNC: "@DefineFunc:">
 |
diff --git a/output/ms-queue/testcase1.c b/output/ms-queue/testcase1.c
new file mode 100644 (file)
index 0000000..8731a0e
--- /dev/null
@@ -0,0 +1,75 @@
+#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;
+               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, &param[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 (file)
index 0000000..f5b2133
--- /dev/null
@@ -0,0 +1,81 @@
+#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;
+               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, &param[i]);
+       }
+       for (i = 0; i < num_threads; i++)
+               thrd_join(threads[i]);
+
+
+       free(param);
+       free(threads);
+       free(queue);
+
+       return 0;
+}
+