tweak
authorPeizhao Ou <peizhaoo@uci.edu>
Wed, 4 Dec 2013 03:28:36 +0000 (19:28 -0800)
committerPeizhao Ou <peizhaoo@uci.edu>
Wed, 4 Dec 2013 03:28:36 +0000 (19:28 -0800)
benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h
benchmark/ms-queue/my_queue.c
benchmark/ms-queue/my_queue.h
notes/interesting_examples.txt [new file with mode: 0644]
src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java

index a52d238..d30c4ab 100644 (file)
@@ -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);
index 3b1784b..9db5efe 100644 (file)
@@ -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;
-}
index cc10de4..2459b9c 100644 (file)
@@ -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 (file)
index 0000000..e69de29
index 39e3f3b..d38bba7 100644 (file)
@@ -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") };