From ab51330e8c0c515221db828346729de2176e9e01 Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Wed, 20 Nov 2013 18:25:42 -0800 Subject: [PATCH] fixed minor bugs --- benchmark/ms-queue/my_queue.c | 166 +++++++++++++++++- benchmark/ms-queue/my_queue.h | 31 ++-- grammer/spec_compiler.jj | 36 ++++ .../codeGenerator/CodeGenerator.java | 8 +- .../codeGenerator/CodeVariables.java | 14 ++ .../codeGenerator/SemanticsChecker.java | 15 ++ .../specExtraction/ConditionalInterface.java | 15 +- 7 files changed, 255 insertions(+), 30 deletions(-) diff --git a/benchmark/ms-queue/my_queue.c b/benchmark/ms-queue/my_queue.c index 634a051..3b1784b 100644 --- a/benchmark/ms-queue/my_queue.c +++ b/benchmark/ms-queue/my_queue.c @@ -1,9 +1,63 @@ #include #include +#include #include "librace.h" #include "model-assert.h" -#include "my_queue.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(); + #define relaxed memory_order_relaxed #define release memory_order_release @@ -68,7 +122,7 @@ void init_queue(queue_t *q, int num_threads) /* Initialize each thread's free list with INITIAL_FREE pointers */ /* The actual nodes are initialized with poison indexes */ - free_lists = malloc(num_threads * sizeof(*free_lists)); + free_lists = (unsigned int**) 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; @@ -84,7 +138,16 @@ void init_queue(queue_t *q, int num_threads) /** @Begin - @Interface_define: Enqueue + @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); @End */ void enqueue(queue_t *q, unsigned int val) @@ -123,7 +186,7 @@ void enqueue(queue_t *q, unsigned int val) &tail, value, release, release); /** @Begin - @Commit_point_define_check: __ATOMIC_RET__ == true + @Commit_point_define_check: commit_success == true @Label: Enqueue_Success_Point @End */ @@ -137,10 +200,16 @@ void enqueue(queue_t *q, unsigned int val) release, release); } - /** @Begin - @Interface_define: Dequeue + @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__ @End */ unsigned int dequeue(queue_t *q) @@ -177,7 +246,7 @@ unsigned int dequeue(queue_t *q) release, release); /** @Begin - @Commit_point_define_check: __ATOMIC_RET__ == true + @Commit_point_define_check: success == true @Label: Dequeue_Success_Point @End */ @@ -189,3 +258,86 @@ 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 4161b33..cc10de4 100644 --- a/benchmark/ms-queue/my_queue.h +++ b/benchmark/ms-queue/my_queue.h @@ -1,3 +1,6 @@ +#ifndef _MY_QUEUE_H +#define _MY_QUEUE_H + #include #define MAX_NODES 0xf @@ -27,6 +30,8 @@ typedef struct { void init_queue(queue_t *q, int num_threads); +#include +using namespace std; /** @Begin @Global_define: @@ -34,18 +39,14 @@ void init_queue(queue_t *q, int num_threads); typedef struct tag_elem { Tag id; unsigned int data; - - tag_elem(Tag _id, unsigned int _data) { - id = _id; - data = _data; - } } tag_elem_t; + @DeclareVar: - spec_queue queue; + list __queue; Tag tag; @InitVar: - queue = spec_queue(); - tag = Tag(); + __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 @@ -60,11 +61,14 @@ void init_queue(queue_t *q, int num_threads); @Begin @Interface: Enqueue @Commit_point_set: Enqueue_Success_Point - @ID: __sequential.tag.getCurAndInc() + @ID: tag++ @Action: # __ID__ is an internal macro that refers to the id of the current # interface call - __sequential.queue.enqueue(tag_elem_t(__ID__, val)); + tag_elem_t elem; + elem.id = __ID__; + elem.data = val; + __queue.push_back(elem); @End */ void enqueue(queue_t *q, unsigned int val); @@ -73,12 +77,15 @@ void enqueue(queue_t *q, unsigned int val); @Begin @Interface: Dequeue @Commit_point_set: Dequeue_Success_Point - @ID: __sequential.queue.peak().tag + @ID: __queue.back().id @Action: - unsigned int _Old_Val = __sequential.queue.dequeue().data; + unsigned int _Old_Val = __queue.front().data; + __queue.pop_front(); @Post_check: _Old_Val == __RET__ @End */ unsigned int dequeue(queue_t *q); int get_thread_num(); + +#endif diff --git a/grammer/spec_compiler.jj b/grammer/spec_compiler.jj index 6a4f61b..24accc9 100644 --- a/grammer/spec_compiler.jj +++ b/grammer/spec_compiler.jj @@ -392,6 +392,29 @@ SKIP : { | +| + +| + >"> +| + >>"> +| + +| + | @@ -667,6 +690,19 @@ ArrayList C_CPP_CODE(ArrayList headers) : t = | t = | t = | t = | t = | t = | t = | t = | t = | t = | + t = | + t = | + t = | + + t = | + t = | + t = | + t = | + t = | + t = | + t = | + t = | + (t = { newLine = true; } ) | t = | t = | t = | t = | diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java index 008ef66..39e3f3b 100644 --- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java @@ -206,12 +206,12 @@ public class CodeGenerator { public static void main(String[] argvs) { 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(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/ms-queue/my_queue.c"), - // new File(homeDir + "/benchmark/ms-queue/my_queue.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") }; CodeGenerator gen = new CodeGenerator(srcFiles); gen.generateCode(); diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java index 4abd569..f98250d 100644 --- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java @@ -545,6 +545,19 @@ public class CodeVariables { newCode.add("}"); newCode.add(""); } + // Also add the true condition if any + if (semantics.containsConditionalInterface(new ConditionalInterface(interfaceName, ""))) { + structName = "hb_condition"; + newCode.add(STRUCT_NEW_DECLARE_DEFINE(ANNO_HB_CONDITION, structName)); + newCode.add(ASSIGN_TO_PTR(structName, "interface_num", interfaceNum)); + newCode.add(ASSIGN_TO_PTR(structName, "hb_condition_num", "0")); + anno = "annotation_hb_condition"; + newCode.add(STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno)); + newCode.add(ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_HB_CONDITION)); + newCode.add(ASSIGN_TO_PTR(anno, "annotation", structName)); + newCode.add(ANNOTATE(anno)); + newCode.add(""); + } // Interface end String infoStructType = null, infoName = null; if (!header.returnType.equals("void") || header.args.size() > 0) { @@ -620,6 +633,7 @@ public class CodeVariables { newCode.add(COMMENT("Include redundant headers")); newCode.add(INCLUDE(HEADER_STDINT)); newCode.add(INCLUDE(HEADER_CDSANNOTATE)); + newCode.add(INCLUDE(HEADER_SPECANNOTATION)); newCode.add(""); // Add annotation newCode.add("if (" + construct.condition + ") {"); diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java b/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java index ae53d3b..6073230 100644 --- a/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java @@ -100,6 +100,21 @@ public class SemanticsChecker { public HashMap> getHBConditions() { return this.hbConditions; } + + /** + * Check if the conditional interface is in the HB checking list + * @param condInterface + * @return + */ + public boolean containsConditionalInterface(ConditionalInterface condInterface) { + if (hbConditions.containsKey(condInterface)) + return true; + for (ConditionalInterface key : hbConditions.keySet()) { + if (hbConditions.get(key).contains(condInterface)) + return true; + } + return false; + } public String getOption(String key) { return options.get(key); diff --git a/src/edu/uci/eecs/specCompiler/specExtraction/ConditionalInterface.java b/src/edu/uci/eecs/specCompiler/specExtraction/ConditionalInterface.java index 791a205..2ef95a6 100644 --- a/src/edu/uci/eecs/specCompiler/specExtraction/ConditionalInterface.java +++ b/src/edu/uci/eecs/specCompiler/specExtraction/ConditionalInterface.java @@ -3,24 +3,25 @@ package edu.uci.eecs.specCompiler.specExtraction; public class ConditionalInterface { public final String interfaceName; public final String hbConditionLabel; - + public ConditionalInterface(String interfaceName, String hbConditionLabel) { this.interfaceName = interfaceName; this.hbConditionLabel = hbConditionLabel; } - - public boolean equals(ConditionalInterface other) { + + public boolean equals(Object other) { if (!(other instanceof ConditionalInterface)) return false; ConditionalInterface another = (ConditionalInterface) other; - return another.interfaceName.equals(interfaceName) && - another.hbConditionLabel.equals(hbConditionLabel); + return another.interfaceName.equals(interfaceName) + && (another.hbConditionLabel.equals(hbConditionLabel) || another.hbConditionLabel + .equals("")); } - + public int hashCode() { return interfaceName.hashCode() << 5 ^ hbConditionLabel.hashCode(); } - + public String toString() { if (hbConditionLabel.equals("")) return interfaceName + "(true)"; -- 2.34.1