From: Peizhao Ou Date: Sun, 15 Nov 2015 04:26:21 +0000 (-0800) Subject: edits X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=733e0543b9eac173556602ce4b65837feaab6230 edits --- diff --git a/benchmark/ms-queue/my_queue.c b/benchmark/ms-queue/my_queue.c index a4fcbdb..9cd2f8e 100644 --- a/benchmark/ms-queue/my_queue.c +++ b/benchmark/ms-queue/my_queue.c @@ -112,12 +112,6 @@ void enqueue(queue_t *q, unsigned int val) */ /**** detected UL ****/ tail = atomic_load_explicit(&q->tail, acquire); - /** - @Begin - @Commit_point_define_check: true - @Label: Enqueue_Read_Tail - @End - */ /****FIXME: miss ****/ next = atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire); //printf("miss1_enqueue\n"); @@ -135,7 +129,7 @@ void enqueue(queue_t *q, unsigned int val) /** @Begin @Commit_point_define_check: success - @Label: Enqueue_UpdateNext + @Label: Enqueue_Update_Next @End */ } @@ -166,8 +160,8 @@ void enqueue(queue_t *q, unsigned int val) release, relaxed); /** @Begin - @Additional_ordering_point_define_check: true - @Label: Enqueue_Additional_Tail_LoadOrCAS + @Commit_point_define_check: true + @Label: Enqueue_Update_Tail @End */ @@ -217,25 +211,17 @@ bool dequeue(queue_t *q, int *retVal) next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, acquire); /** @Begin - @Potential_commit_point_define: true - @Label: Dequeue_Potential_LoadNext + @Potential_commit_point_define: true + @Label: Dequeue_Potential_Read_Next @End */ - if (atomic_load_explicit(&q->head, relaxed) == head) { if (get_ptr(head) == get_ptr(tail)) { /* Check for uninitialized 'next' */ //MODEL_ASSERT(get_ptr(next) != POISON_IDX); - if (get_ptr(next) == 0) { // NULL - /** - @Begin - @Commit_point_define: true - @Potential_commit_point_label: Dequeue_Potential_Read_Tail - @Label: Dequeue_Read_Tail - @End - */ + if (get_ptr(next) == 0) { // NULL return false; // NULL } /**** Detected UL (testcase1.c) ****/ @@ -261,8 +247,8 @@ bool dequeue(queue_t *q, int *retVal) /** @Begin @Commit_point_define: success - @Potential_commit_point_label: Dequeue_Potential_LoadNext - @Label: Dequeue_LoadNext + @Potential_commit_point_label: Dequeue_Potential_Read_Next + @Label: Dequeue_Read_Next @End */ if (!success) diff --git a/benchmark/ms-queue/my_queue.h b/benchmark/ms-queue/my_queue.h index e678378..2f18fbc 100644 --- a/benchmark/ms-queue/my_queue.h +++ b/benchmark/ms-queue/my_queue.h @@ -85,7 +85,7 @@ void init_queue(queue_t *q, int num_threads); # 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: _Method1.__RET__ == NULL + @Commutativity: Enqueue <-> Dequeue: _Method2.__RET__ == NULL @Commutativity: Enqueue <-> Dequeue: _Method1.q != _Method2.q @End */ @@ -95,7 +95,7 @@ void init_queue(queue_t *q, int num_threads); /** @Begin @Interface: Enqueue - @Commit_point_set: Enqueue_Read_Tail | Enqueue_UpdateNext | Enqueue_Additional_Tail_LoadOrCAS + @Commit_point_set: Enqueue_Update_Next | Enqueue_Update_Tail @ID: get_and_inc(tag) @Action: # __ID__ is an internal macro that refers to the id of the current @@ -110,7 +110,7 @@ void enqueue(queue_t *q, unsigned int val); /** @Begin @Interface: Dequeue - @Commit_point_set: Dequeue_Read_Head | Dequeue_Read_Tail | Dequeue_LoadNext + @Commit_point_set: Dequeue_Read_Head | Dequeue_Read_Tail | Dequeue_Read_Next @ID: get_id(front(__queue)) @Action: unsigned int _Old_Val = 0; diff --git a/output/Makefile b/output/Makefile new file mode 100644 index 0000000..4d432e9 --- /dev/null +++ b/output/Makefile @@ -0,0 +1,18 @@ +#DIRS := barrier mcs-lock mpmc-queue spsc-queue spsc-bugfix linuxrwlocks \ + dekker-fences chase-lev-deque ms-queue chase-lev-deque-bugfix \ + concurrent-hashmap seqlock spsc-example spsc-queue-scfence \ + treiber-stack + +DIRS := ms-queue + +.PHONY: $(DIRS) + +all: $(DIRS) + +clean: $(DIRS:%=clean-%) + +$(DIRS): + $(MAKE) -C $@ + +clean-%: + -$(MAKE) -C $* clean diff --git a/output/benchmarks.mk b/output/benchmarks.mk new file mode 100644 index 0000000..20a76d8 --- /dev/null +++ b/output/benchmarks.mk @@ -0,0 +1,33 @@ +# A few common Makefile items + +CC = gcc +CXX = g++ + +UNAME = $(shell uname) + +LIB_NAME = model +LIB_SO = lib$(LIB_NAME).so + +BASE = $(HOME)/model-checker-priv/model-checker-priv +INCLUDE = -I$(BASE)/include -I../include -I$(BASE)/spec-analysis -I$(BASE) + +# C preprocessor flags +CPPFLAGS += $(INCLUDE) -g + +# C++ compiler flags +CXXFLAGS += $(CPPFLAGS) + +# C compiler flags +CFLAGS += $(CPPFLAGS) + +# Linker flags +LDFLAGS += -L$(BASE) -l$(LIB_NAME) -rdynamic + +# Mac OSX options +ifeq ($(UNAME), Darwin) +MACFLAGS = -D_XOPEN_SOURCE -DMAC +CPPFLAGS += $(MACFLAGS) +CXXFLAGS += $(MACFLAGS) +CFLAGS += $(MACFLAGS) +LDFLAGS += $(MACFLAGS) +endif diff --git a/output/ms-queue/Makefile b/output/ms-queue/Makefile new file mode 100644 index 0000000..da3a0e4 --- /dev/null +++ b/output/ms-queue/Makefile @@ -0,0 +1,17 @@ +include ../benchmarks.mk + +TESTNAME = main + +HEADERS = my_queue.h +OBJECTS = main.o my_queue.o + +all: $(TESTNAME) + +$(TESTNAME): $(HEADERS) $(OBJECTS) + $(CC) -o $@ $(OBJECTS) $(CFLAGS) $(LDFLAGS) + +%.o: %.c + $(CC) -c -o $@ $< $(CFLAGS) + +clean: + rm -f $(TESTNAME) *.o diff --git a/output/run.sh b/output/run.sh new file mode 100755 index 0000000..e2fcd8f --- /dev/null +++ b/output/run.sh @@ -0,0 +1,29 @@ +#!/bin/sh +# +# Runs a simple test (default: ./test/userprog.o) +# Syntax: +# ./run.sh [test program] [OPTIONS] +# ./run.sh [OPTIONS] +# ./run.sh [gdb [test program]] +# +# If you include a 'gdb' argument, the your program will be launched with gdb. +# You can also supply a test program argument to run something besides the +# default program. +# + +# Get the directory in which this script and the binaries are located +#BINDIR="${0%/*}" +BINDIR=${HOME}/model-checker-priv/model-checker-priv + +BIN=${BINDIR}/test/userprog.o +PREFIX= + +export LD_LIBRARY_PATH=${BINDIR} +# For Mac OSX +export DYLD_LIBRARY_PATH=${BINDIR} + +[ $# -gt 0 ] && [ "$1" = "gdb" ] && PREFIX=gdb && shift +[ $# -gt 0 ] && [ -e "$1" ] && BIN="$1" && shift + +set -xe +$PREFIX $BIN $@ diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java index bb572c1..bcc6e41 100644 --- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java @@ -52,7 +52,7 @@ public class CodeVariables { public static final String SPEC_ANNO_TYPE = "spec_anno_type"; public static final String SPEC_ANNO_TYPE_INIT = "INIT"; - public static final String SPEC_ANNO_TYPE_HB_INIT = "HB_INIT"; + public static final String SPEC_ANNO_TYPE_HB_RULE = "HB_RULE"; public static final String SPEC_ANNO_TYPE_INTERFACE_BEGIN = "INTERFACE_BEGIN"; public static final String SPEC_ANNO_TYPE_HB_CONDITION = "HB_CONDITION"; public static final String SPEC_ANNO_TYPE_INTERFACE_END = "INTERFACE_END"; @@ -65,8 +65,8 @@ public class CodeVariables { public static final String SPEC_ANNOTATION_FIELD_ANNO = "annotation"; public static final String ANNO_INIT = "anno_init"; - public static final String ANNO_HB_INIT = "anno_hb_init"; - public static final String ANNO_COMMUTATIVITY_RULE = "anno_commutativity_rule"; + public static final String HB_RULE = "hb_rule"; + public static final String COMMUTATIVITY_RULE = "commutativity_rule"; public static final String ANNO_INTERFACE_BEGIN = "anno_interface_begin"; public static final String ANNO_INTERFACE_END = "anno_interface_end"; public static final String ANNO_POTENTIAL_CP_DEFINE = "anno_potential_cp_define"; @@ -418,10 +418,11 @@ public class CodeVariables { newCode.add("static " + DECLARE("void**", "func_ptr_table")); // Happens-before initialization rules // Should make it static - newCode.add("static " + DECLARE(ANNO_HB_INIT + "**", "hb_init_table")); - + newCode.add("static " + DECLARE(HB_RULE + "**", "hb_rule_table")); + // Declare the Commutativity Rule table - newCode.add("static " + DECLARE(ANNO_COMMUTATIVITY_RULE + "**", "commutativity_rule_table")); + newCode.add("static " + + DECLARE(COMMUTATIVITY_RULE + "**", "commutativity_rule_table")); // Define the Commutativity Rule condition functions ArrayList rules = semantics.getGlobalConstruct().commutativityRules; for (int i = 0; i < rules.size(); i++) { @@ -429,21 +430,32 @@ public class CodeVariables { String infoStructType1 = rule.method1 + "_info"; String infoStructType2 = rule.method2 + "_info"; String condition = rule.condition; - - // Declare - + String conditionFuncName = "CommutativityCondition" + + Integer.toString(i); + // Replace the "_M1." and "_M2." with the actual info struct - condition.replaceAll("_M1\\.", infoStructType1 + "->"); - condition.replaceAll("_M2\\.", infoStructType2 + "->"); - + condition = condition.replaceAll("_Method1 \\.", "_info1->"); + condition = condition.replaceAll("_Method2 \\.", "_info2->"); + + // Declare the signature of the condition function + newCode.add("inline static bool " + conditionFuncName + + "(void *info1, void *info2) {"); + // Cast the "void*" type to the actual info type - - newCode.add(e) + newCode.add("\t" + + DECLARE_DEFINE(infoStructType1, "*_info1", "(" + + infoStructType1 + "*) info1")); + newCode.add("\t" + + DECLARE_DEFINE(infoStructType2, "*_info2", "(" + + infoStructType2 + "*) info2")); + newCode.add("\treturn " + condition + ";"); + + // End of the condition function + newCode.add("}"); } - newCode.add(""); - + // Beginning initialization // Define the __SPEC_INIT__ function to initialize user-defined // variables @@ -459,10 +471,10 @@ public class CodeVariables { addAllCodeWithIndent(newCode, construct.code.cleanupCode, "\t"); newCode.add("}"); newCode.add(""); - + newCode.add(COMMENT("Define function for sequential code initialization")); newCode.add("inline static void __sequential_init() {"); - + // Init func_ptr_table newCode.add("\t" + COMMENT("Init func_ptr_table")); newCode.add("\t" @@ -478,13 +490,10 @@ public class CodeVariables { + ASSIGN("func_ptr_table[2 * " + interfaceNum + " + 1]", "(void*) &" + interfaceName + "_check_action")); } - - // Init Commutativity rules table - - + // Init Happens-before rules table newCode.addAll(generateHBInitAnnotation(semantics)); - + // Init Commutativity rules table newCode.addAll(generateCommutativityAnnotation(semantics)); @@ -494,25 +503,27 @@ public class CodeVariables { String structName = "anno_init", anno = "init"; newCode.add("\t" + STRUCT_NEW_DECLARE_DEFINE(ANNO_INIT, structName)); newCode.add("\t" - + ASSIGN_TO_PTR(structName, "init_func", "(void*) __SPEC_INIT__")); + + ASSIGN_TO_PTR(structName, "init_func", + "(void_func_t*) __SPEC_INIT__")); newCode.add("\t" - + ASSIGN_TO_PTR(structName, "cleanup_func", "(void*) __SPEC_CLEANUP__")); + + ASSIGN_TO_PTR(structName, "cleanup_func", + "(void_func_t*) __SPEC_CLEANUP__")); newCode.add("\t" + ASSIGN_TO_PTR(structName, "func_table", "func_ptr_table")); newCode.add("\t" + ASSIGN_TO_PTR(structName, "func_table_size", "INTERFACE_SIZE")); newCode.add("\t" - + ASSIGN_TO_PTR(structName, "hb_init_table", "hb_init_table")); + + ASSIGN_TO_PTR(structName, "hb_rule_table", "hb_rule_table")); newCode.add("\t" - + ASSIGN_TO_PTR(structName, "hb_init_table_size", - "HB_INIT_TABLE_SIZE")); - + + ASSIGN_TO_PTR(structName, "hb_rule_table_size", + "HB_RULE_TABLE_SIZE")); newCode.add("\t" - + ASSIGN_TO_PTR(structName, "commutativity_rule_table", "hb_init_table")); + + ASSIGN_TO_PTR(structName, "commutativity_rule_table", + "commutativity_rule_table")); newCode.add("\t" - + ASSIGN_TO_PTR(structName, "hb_init_table_size", - "HB_INIT_TABLE_SIZE")); - + + ASSIGN_TO_PTR(structName, "commutativity_rule_table_size", + Integer.toString(rules.size()))); + newCode.add("\t" + STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno)); newCode.add("\t" + ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_INIT)); newCode.add("\t" + ASSIGN_TO_PTR(anno, "annotation", structName)); @@ -544,7 +555,7 @@ public class CodeVariables { String templateDecl = semantics.getTemplateFullStr(); if (templateList == null) { newCode.add(DECLARE("void**", varPrefix + "func_ptr_table")); - newCode.add(DECLARE("anno_hb_init**", varPrefix + "hb_init_table")); + newCode.add(DECLARE("hb_rule**", varPrefix + "hb_rule_table")); for (int i = 0; i < construct.code.declareVar.size(); i++) { VariableDeclaration varDecl = construct.code.declareVar.get(i); newCode.add(DECLARE(varDecl.type, varPrefix + varDecl.name)); @@ -553,7 +564,7 @@ public class CodeVariables { newCode.add(templateDecl); newCode.add(DECLARE("void**", varPrefix + "func_ptr_table")); newCode.add(templateDecl); - newCode.add(DECLARE("anno_hb_init**", varPrefix + "hb_init_table")); + newCode.add(DECLARE("hb_rule**", varPrefix + "hb_rule_table")); for (int i = 0; i < construct.code.declareVar.size(); i++) { VariableDeclaration varDecl = construct.code.declareVar.get(i); newCode.add(templateDecl); @@ -572,7 +583,7 @@ public class CodeVariables { for (ConditionalInterface right : semantics.getHBConditions().get( left)) { String structVarName = "hbConditionInit" + hbConditionInitIdx; - // String annotationVarName = "hb_init" + hbConditionInitIdx; + // String annotationVarName = "hb_rule" + hbConditionInitIdx; hbConditionInitIdx++; String interfaceNumBefore = Integer .toString(semantics.interface2Num @@ -586,7 +597,7 @@ public class CodeVariables { newCode.add("\t" + COMMENT(left + " -> " + right)); newCode.add("\t" - + STRUCT_NEW_DECLARE_DEFINE(ANNO_HB_INIT, structVarName)); + + STRUCT_NEW_DECLARE_DEFINE(HB_RULE, structVarName)); newCode.add("\t" + ASSIGN_TO_PTR(structVarName, "interface_num_before", interfaceNumBefore) @@ -605,19 +616,19 @@ public class CodeVariables { + SHORT_COMMENT(right.hbConditionLabel)); } } - // Init hb_init_table - newCode.add("\t" + COMMENT("Init hb_init_table")); + // Init hb_rule_table + newCode.add("\t" + COMMENT("Init hb_rule_table")); newCode.add("\t" - + ASSIGN("hb_init_table", "(" + ANNO_HB_INIT - + "**) malloc(sizeof(" + ANNO_HB_INIT + "*) * " + + ASSIGN("hb_rule_table", "(" + HB_RULE + + "**) malloc(sizeof(" + HB_RULE + "*) * " + hbConditionInitIdx + ")")); - // Define HB_INIT_TABLE_SIZE + // Define HB_RULE_TABLE_SIZE newCode.add("\t" - + DEFINE("HB_INIT_TABLE_SIZE", + + DEFINE("HB_RULE_TABLE_SIZE", Integer.toString(hbConditionInitIdx))); for (int i = 0; i < hbConditionInitIdx; i++) { newCode.add("\t" - + ASSIGN("hb_init_table[" + i + "]", "hbConditionInit" + i)); + + ASSIGN("hb_rule_table[" + i + "]", "hbConditionInit" + i)); } return newCode; } @@ -626,24 +637,48 @@ public class CodeVariables { SemanticsChecker semantics) { ArrayList newCode = new ArrayList(); ArrayList rules = semantics.getGlobalConstruct().commutativityRules; - for (CommutativityRule rule : rules) { - - } // Init commutativity_rule_table newCode.add("\t" + COMMENT("Init commutativity_rule_table")); + + // Users have not defined any commutativity rules + if (rules.size() == 0) + return newCode; + newCode.add("\t" - + ASSIGN("hb_init_table", "(" + ANNO_HB_INIT - + "**) malloc(sizeof(" + ANNO_HB_INIT + "*) * " - + hbConditionInitIdx + ")")); - // Define HB_INIT_TABLE_SIZE - newCode.add("\t" - + DEFINE("HB_INIT_TABLE_SIZE", - Integer.toString(hbConditionInitIdx))); - for (int i = 0; i < hbConditionInitIdx; i++) { + + ASSIGN("commutativity_rule_table", "(" + COMMUTATIVITY_RULE + + "**) malloc(sizeof(" + COMMUTATIVITY_RULE + "*) * " + + rules.size() + ")")); + + // Declare a rule pointer + newCode.add("\t" + DECLARE("commutativity_rule*", "rule")); + + for (int i = 0; i < rules.size(); i++) { + CommutativityRule rule = rules.get(i); + String interfaceNumBefore = Integer + .toString(semantics.interface2Num.get(rule.method1)); + String interfaceNumAfter = Integer.toString(semantics.interface2Num + .get(rule.method2)); + String conditionFuncName = "CommutativityCondition" + i; + + // Construct a new rule + newCode.add("\t" + + ASSIGN("rule", + "(commutativity_rule*) malloc (sizeof(commutativity_rule))")); + newCode.add("\t" + + ASSIGN_TO_PTR("rule", "interface_num_before", + interfaceNumBefore)); + newCode.add("\t" + + ASSIGN_TO_PTR("rule", "interface_num_after", + interfaceNumAfter)); newCode.add("\t" - + ASSIGN("hb_init_table[" + i + "]", "hbConditionInit" + i)); + + ASSIGN_TO_PTR("rule", "condition", conditionFuncName)); + + // Assign the rule to the corresponding commutativity table slot + newCode.add("\t" + + ASSIGN("commutativity_rule_table[" + i + "]", "rule")); } + return newCode; } @@ -858,13 +893,7 @@ public class CodeVariables { newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "label_name", "\"" + construct.label + "\"")); - if (construct.isAdditionalOrderingPoint) { - newCode.add("\t\t" - + ASSIGN_TO_PTR(structName, "is_additional_point", "true")); - } else { - newCode.add("\t\t" - + ASSIGN_TO_PTR(structName, "is_additional_point", "false")); - } + newCode.add("\t\t" + STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno)); newCode.add("\t\t" + ASSIGN_TO_PTR(anno, "type", @@ -922,13 +951,7 @@ public class CodeVariables { + construct.label + "\"")); newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "interface_num", interfaceNum)); - if (construct.isAdditionalOrderingPoint) { - newCode.add("\t\t" - + ASSIGN_TO_PTR(structName, "is_additional_point", "true")); - } else { - newCode.add("\t\t" - + ASSIGN_TO_PTR(structName, "is_additional_point", "false")); - } + newCode.add("\t\t" + STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno)); newCode.add("\t\t" + ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_CP_DEFINE_CHECK)); @@ -1023,13 +1046,6 @@ public class CodeVariables { + construct.potentialCPLabel + "\"")); newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "interface_num", interfaceNum)); - if (construct.isAdditionalOrderingPoint) { - newCode.add("\t\t" - + ASSIGN_TO_PTR(structName, "is_additional_point", "true")); - } else { - newCode.add("\t\t" - + ASSIGN_TO_PTR(structName, "is_additional_point", "false")); - } newCode.add("\t\t" + STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno)); newCode.add("\t\t" + ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_CP_DEFINE));