From: Peizhao Ou Date: Wed, 7 Dec 2016 21:54:08 +0000 (-0800) Subject: This is the PPoPP17 artifact version X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=3b645ad030ddb824d3cf6b80e321a466906a256f;p=model-checker.git This is the PPoPP17 artifact version --- diff --git a/Makefile b/Makefile index eb84076..56d0dab 100644 --- a/Makefile +++ b/Makefile @@ -1,6 +1,6 @@ include common.mk -SCFENCE_DIR := scfence +SPEC_DIR := spec-analysis OBJECTS := libthreads.o schedule.o model.o threads.o librace.o action.o \ nodestack.o clockvector.o main.o snapshot-interface.o cyclegraph.o \ @@ -8,7 +8,9 @@ OBJECTS := libthreads.o schedule.o model.o threads.o librace.o action.o \ snapshot.o malloc.o mymemory.o common.o mutex.o promise.o conditionvariable.o \ context.o scanalysis.o execution.o plugins.o libannotate.o -CPPFLAGS += -Iinclude -I. -I$(SCFENCE_DIR) +include $(SPEC_DIR)/Makefile + +CPPFLAGS += -Iinclude -I. -I$(SPEC_DIR) LDFLAGS := -ldl -lrt -rdynamic SHARED := -shared @@ -34,28 +36,27 @@ docs: *.c *.cc *.h README.html README.html: README.md $(MARKDOWN) $< > $@ +$(LIB_SO): $(OBJECTS) + $(CXX) $(SHARED) -o $(LIB_SO) $+ $(LDFLAGS) malloc.o: malloc.c - $(CC) -fPIC -c malloc.c -DMSPACES -DONLY_MSPACES -DHAVE_MMAP=0 $(CPPFLAGS) -Wno-unused-variable - -%.o : %.cc - $(CXX) -MMD -MF .$@.d -fPIC -c $< $(CPPFLAGS) - -include $(SCFENCE_DIR)/Makefile + $(CC) -fPIC -c malloc.c -DMSPACES -DONLY_MSPACES -DHAVE_MMAP=0 $(CPPLAGS) -Wno-unused-variable --include $(wildcard $(SCFENCE_DIR)/.*.d) - -$(LIB_SO): $(OBJECTS) - $(CXX) $(SHARED) -o $(LIB_SO) $+ $(LDFLAGS) +%.o: %.cc + $(CXX) -MMD -MF $(dir $@).$(notdir $@).d -fPIC -c $< -o $@ $(CPPFLAGS) %.pdf: %.dot dot -Tpdf $< -o $@ --include $(OBJECTS:%=.%.d) +# Replace all the basename with +ALL_DEPS := $(shell echo $(OBJECTS) | sed -E 's/([^ ]*\/)?([^\/ ]*)/\1\.\2.d/g') +-include $(ALL_DEPS) +#-include $(OBJECTS:%=.%.d) + PHONY += clean clean: - rm -f *.o *.so .*.d *.pdf *.dot $(SCFENCE_DIR)/.*.d $(SCFENCE_DIR)/*.o + rm -f *.o *.so $(ALL_DEPS) *.pdf *.dot $(OBJECTS) $(MAKE) -C $(TESTS_DIR) clean PHONY += mrclean diff --git a/action.cc b/action.cc index d4c6253..2e9dece 100644 --- a/action.cc +++ b/action.cc @@ -9,7 +9,6 @@ #include "common.h" #include "threads-model.h" #include "nodestack.h" -#include "wildcard.h" #define ACTION_INITIAL_CLOCK 0 @@ -35,7 +34,6 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value, Thread *thread) : type(type), order(order), - original_order(order), location(loc), value(value), reads_from(NULL), @@ -555,7 +553,7 @@ const char * ModelAction::get_type_str() const case ATOMIC_WAIT: return "wait"; case ATOMIC_NOTIFY_ONE: return "notify one"; case ATOMIC_NOTIFY_ALL: return "notify all"; - case ATOMIC_ANNOTATION: return "annotation"; + case ATOMIC_ANNOTATION: return "atomic annotation"; default: return "unknown type"; }; } diff --git a/action.h b/action.h index c8ad85b..ad3b828 100644 --- a/action.h +++ b/action.h @@ -96,8 +96,6 @@ public: thread_id_t get_tid() const { return tid; } action_type get_type() const { return type; } memory_order get_mo() const { return order; } - memory_order get_original_mo() const { return original_order; } - void set_mo(memory_order order) { this->order = order; } void * get_location() const { return location; } modelclock_t get_seq_number() const { return seq_number; } uint64_t get_value() const { return value; } @@ -196,9 +194,6 @@ private: /** @brief The memory order for this operation. */ memory_order order; - /** @brief The original memory order parameter for this operation. */ - memory_order original_order; - /** @brief A pointer to the memory location for this action. */ void *location; diff --git a/cdsspec-compiler/build.xml b/cdsspec-compiler/build.xml new file mode 100644 index 0000000..065bcad --- /dev/null +++ b/cdsspec-compiler/build.xml @@ -0,0 +1,24 @@ + + + + + + + + + + + + + + + + + + + + + diff --git a/cdsspec-compiler/clean.sh b/cdsspec-compiler/clean.sh new file mode 100755 index 0000000..22c313e --- /dev/null +++ b/cdsspec-compiler/clean.sh @@ -0,0 +1,8 @@ +#!/bin/bash + +AutoGenDir=$(pwd)/src/edu/uci/eecs/utilParser +echo "Deleting the old generated java files." +rm -rf $AutoGenDir + +echo "Deleting the class files." +rm -rf ./classes diff --git a/cdsspec-compiler/generate.sh b/cdsspec-compiler/generate.sh new file mode 100755 index 0000000..38ec8b2 --- /dev/null +++ b/cdsspec-compiler/generate.sh @@ -0,0 +1,19 @@ +#!/bin/bash + +BENCH=(ms-queue linuxrwlocks mcs-lock \ + chase-lev-deque-bugfix spsc-bugfix mpmc-queue ticket-lock \ + concurrent-hashmap seqlock read-copy-update) + +ClassPath=$(dirname ${BASH_SOURCE[0]})/classes + +Class=edu/uci/eecs/codeGenerator/CodeGenerator + +# Use your own directory. +# We recommend the original benchmarks and generated instrumented benchmarks to +# be within the model checker's directory. +BenchDir=../benchmarks +GenerateDir=../test-cdsspec + +mkdir -p $GenerateDir + +java -cp $ClassPath $Class $BenchDir $GenerateDir ${BENCH[*]} diff --git a/cdsspec-compiler/grammer/util.jj b/cdsspec-compiler/grammer/util.jj new file mode 100644 index 0000000..5b5446b --- /dev/null +++ b/cdsspec-compiler/grammer/util.jj @@ -0,0 +1,458 @@ +/* util.jj Grammer definition for utility functions */ + +options { + STATIC = false; + JAVA_UNICODE_ESCAPE = true; +} + +PARSER_BEGIN(UtilParser) +package edu.uci.eecs.utilParser; +import edu.uci.eecs.specExtraction.FunctionHeader; +import edu.uci.eecs.specExtraction.QualifiedName; +import edu.uci.eecs.specExtraction.VariableDeclaration; +//import edu.uci.eecs.specExtraction.WrongAnnotationException; + +import java.io.FileInputStream; +import java.io.FileNotFoundException; +import java.io.InputStream; +import java.io.ByteArrayInputStream; +import java.io.File; +import java.util.ArrayList; + + +public class UtilParser { + public static void main(String[] argvs) + throws ParseException, TokenMgrError { + try { + File f = new File("./grammer/spec1.txt"); + FileInputStream fis = new FileInputStream(f); + UtilParser parser = new UtilParser(fis); + + //parser.Test(); + System.out.println("Parsing finished!"); + } catch (FileNotFoundException e) { + e.printStackTrace(); + } + } + + public static ArrayList getTemplateArg(String line) + throws ParseException { + InputStream input = new ByteArrayInputStream(line.getBytes()); + UtilParser parser = new UtilParser(input); + return parser.TemplateParamList(); + } + + public static FunctionHeader parseFuncHeader(String line) + throws ParseException { + InputStream input = new ByteArrayInputStream(line.getBytes()); + UtilParser parser = new UtilParser(input); + return parser.FuncDecl(); + } + + public static VariableDeclaration parseDeclaration(String line) + throws ParseException { + InputStream input = new ByteArrayInputStream(line.getBytes()); + UtilParser parser = new UtilParser(input); + return parser.Declaration(); + } + + public static String stringArray2String(ArrayList content) { + StringBuilder sb = new StringBuilder(); + if (content.size() == 1) + return content.get(0); + for (int i = 0; i < content.size(); i++) { + sb.append(content.get(i) + "\n"); + } + return sb.toString(); + } +} +PARSER_END(UtilParser) + +SKIP : +{ + " " +| + "\n" +| + "\r" +| + "\r\n" +| + "\t" +} + +TOKEN : +{ +/* Specification & C/C++ shared tokens */ +// Reserved keywords + +| + +| + +| + +| + +| + +| + +| + +| + <#DIGIT: ["0"-"9"]> +| + <#LETTER: ["a"-"z", "A"-"Z"]> +| + | "_") ( | | "_")*> +| + +| + +| + +| + +| + +| + +| + +| + "> +| + +| +/* C/C++ only token*/ + +| + +| + +| + +| + +| + +| + +| + +| + +| + +| + +| + +| + +| + +| + +| + "> +| + ="> +| + +| + +| + +| + +| + +| + +| + +| + >"> +| + >>"> +| + +| + +| + +| + +| + < INTEGER_LITERAL: + (["l","L"])? + | (["l","L"])? + | (["l","L"])?> +| + < #DECIMAL_LITERAL: ["1"-"9"] (["0"-"9"])* > +| + < #HEX_LITERAL: "0" ["x","X"] (["0"-"9","a"-"f","A"-"F"])+ > +| + < #OCTAL_LITERAL: "0" (["0"-"7"])* > +| + < FLOATING_POINT_LITERAL: + + | > +| + < #DECIMAL_FLOATING_POINT_LITERAL: + (["0"-"9"])+ "." (["0"-"9"])* ()? (["f","F","d","D"])? + | "." (["0"-"9"])+ ()? (["f","F","d","D"])? + | (["0"-"9"])+ (["f","F","d","D"])? + | (["0"-"9"])+ ()? ["f","F","d","D"]> +| + < #DECIMAL_EXPONENT: ["e","E"] (["+","-"])? (["0"-"9"])+ > +| + < #HEXADECIMAL_FLOATING_POINT_LITERAL: + "0" ["x", "X"] (["0"-"9","a"-"f","A"-"F"])+ (".")? (["f","F","d","D"])? + | "0" ["x", "X"] (["0"-"9","a"-"f","A"-"F"])* "." (["0"-"9","a"-"f","A"-"F"])+ (["f","F","d","D"])?> +| + < #HEXADECIMAL_EXPONENT: ["p","P"] (["+","-"])? (["0"-"9"])+ > +| + < #SPACE: (" " | "\t")+> +| + < #TO_END_OF_LINE: (~["\n"])+> +| + /* Macro token */ + )? "include" ( | "<" ( | )+ ">")> +| + )? > +} + +String Type() : +{ + String type; + String str; + QualifiedName name; +} +{ + { type = ""; } + ( + { type = "const"; } + )? + ( + ((str = .image | str = .image | str = .image) { + type = type.equals("") ? type + str : type + " " + str; + })? + ( + name = ParseQualifiedName() { + if (!type.equals("")) + type = type + " " + name.fullName; + else + type = name.fullName; + }) + ) + ((str = .image { + if (!type.equals("")) + type = type + " " + str; + else + type = str; + }) | + (str = .image { + if (!type.equals("")) + type = type + " " + str; + else + type = str; + }) | + (str = .image { + if (!type.equals("")) + type = type + " " + str; + else + type = str; + }) + )* + { + return type; + } +} + +void Test() : +{ + String str; + FunctionHeader func; +} +{ + /* + str = Type() + { + System.out.println(str); + } + */ + func = FuncDecl() + { + System.out.println(func); + } + +} + +String ParameterizedName() : +{ + String res = ""; + String str; +} +{ + (str = .image {res = str;}) + ( str = Type() { res = res + "<" + str; } + ( str = Type() { res = res + ", " + str; })* + { res = res + ">"; } + )? + { + return res; + } +} + +FunctionHeader FuncDecl() : +{ + String ret; + QualifiedName funcName; + ArrayList args; +} +{ + ( | )* + ret = Type() + funcName = ParseQualifiedName() + args = FormalParamList() + { + FunctionHeader res = new FunctionHeader(ret, funcName, args); + //System.out.println(res); + return res; + } +} + +QualifiedName ParseQualifiedName() : +{ + String qualifiedName, str; +} +{ + { qualifiedName = ""; } + (str = ParameterizedName() { qualifiedName = qualifiedName + str; } ) + ( (str = ParameterizedName() { qualifiedName = qualifiedName + + "::" + str; } ))* + { + QualifiedName res = new QualifiedName(qualifiedName); + //System.out.println(res); + return res; + } +} + +ArrayList TemplateParamList() : +{ + ArrayList params; + String type; + String name; +} +{ + { + params = new ArrayList(); + } +