From 3b645ad030ddb824d3cf6b80e321a466906a256f Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Wed, 7 Dec 2016 13:54:08 -0800 Subject: [PATCH] This is the PPoPP17 artifact version --- Makefile | 29 +- action.cc | 4 +- action.h | 5 - cdsspec-compiler/build.xml | 24 + cdsspec-compiler/clean.sh | 8 + cdsspec-compiler/generate.sh | 19 + cdsspec-compiler/grammer/util.jj | 458 +++++ cdsspec-compiler/lib/javacc.jar | Bin 0 -> 384637 bytes cdsspec-compiler/notes/definition.cc | 364 ++++ .../notes/generated_code_examples.txt | 256 +++ cdsspec-compiler/notes/impl.txt | 50 + .../notes/interesting_examples.txt | 1 + cdsspec-compiler/notes/nondeterm-spec.txt | 458 +++++ .../notes/register-example/Makefile | 12 + .../register-example/cdsspec-generated.h | 152 ++ .../notes/register-example/register.cc | 99 + .../register-example/register.cc.original | 65 + .../notes/register-example/register.h | 11 + cdsspec-compiler/notes/sequential_spec.txt | 137 ++ cdsspec-compiler/run-javacc.sh | 18 + .../uci/eecs/codeGenerator/CodeAdditions.java | 87 + .../uci/eecs/codeGenerator/CodeGenerator.java | 364 ++++ .../codeGenerator/CodeGeneratorUtils.java | 1280 +++++++++++++ .../uci/eecs/codeGenerator/Environment.java | 57 + .../src/edu/uci/eecs/specExtraction/Code.java | 197 ++ .../specExtraction/CommutativityRule.java | 22 + .../uci/eecs/specExtraction/Construct.java | 28 + .../eecs/specExtraction/DefineConstruct.java | 51 + .../eecs/specExtraction/EntryConstruct.java | 30 + .../eecs/specExtraction/FunctionHeader.java | 183 ++ .../eecs/specExtraction/GlobalConstruct.java | 367 ++++ .../specExtraction/InterfaceConstruct.java | 269 +++ .../uci/eecs/specExtraction/OPConstruct.java | 51 + .../edu/uci/eecs/specExtraction/OPType.java | 13 + .../eecs/specExtraction/QualifiedName.java | 47 + .../eecs/specExtraction/SpecExtractor.java | 735 ++++++++ .../uci/eecs/specExtraction/SpecNaming.java | 223 +++ .../uci/eecs/specExtraction/SpecUtils.java | 319 ++++ .../specExtraction/VariableDeclaration.java | 45 + .../WrongAnnotationException.java | 66 + common.h | 3 +- common.mk | 4 +- execution.cc | 34 +- execution.h | 5 +- impatomic.cc | 12 +- include/cdsannotate.h | 7 + include/impatomic.h | 25 +- include/model_memory.h | 25 + include/stdatomic.h | 32 + main.cc | 20 +- model.cc | 61 +- model.h | 24 +- mymemory.cc | 18 +- mymemory.h | 16 + nodestack.cc | 10 - nodestack.h | 1 - params.h | 2 +- plugins.cc | 4 +- scfence/scfence.cc | 2 +- spec-analysis/.gitignore | 12 + spec-analysis/Makefile | 7 + spec-analysis/cdsspec.h | 376 ++++ spec-analysis/executiongraph.cc | 1611 +++++++++++++++++ spec-analysis/executiongraph.h | 338 ++++ spec-analysis/include/specannotation-api.h | 38 + spec-analysis/methodcall.cc | 125 ++ spec-analysis/methodcall.h | 114 ++ spec-analysis/spec_common.h | 47 + spec-analysis/specanalysis.cc | 226 +++ spec-analysis/specanalysis.h | 77 + spec-analysis/specannotation.cc | 96 + spec-analysis/specannotation.h | 230 +++ test-cdsspec/Makefile | 19 + test-cdsspec/benchmarks.mk | 41 + test-cdsspec/chase-lev-deque-bugfix/Makefile | 24 + test-cdsspec/cleanse.sh | 12 + test-cdsspec/concurrent-hashmap/Makefile | 24 + test-cdsspec/include/unrelacy.h | 103 ++ test-cdsspec/linuxrwlocks/Makefile | 24 + test-cdsspec/mcs-lock/Makefile | 24 + test-cdsspec/mpmc-queue/Makefile | 24 + test-cdsspec/ms-queue/.gitignore | 8 + test-cdsspec/ms-queue/Makefile | 24 + test-cdsspec/performance.sh | 20 + test-cdsspec/read-copy-update/Makefile | 24 + test-cdsspec/run-all.sh | 21 + test-cdsspec/run.sh | 28 + test-cdsspec/seqlock/Makefile | 24 + test-cdsspec/spsc-bugfix/Makefile | 24 + test-cdsspec/ticket-lock/Makefile | 24 + test/Makefile | 3 +- test/iriw.cc | 66 - test/iriw_wildcard.cc | 66 - threads.cc | 4 +- traceanalysis.h | 15 - 95 files changed, 10508 insertions(+), 344 deletions(-) create mode 100644 cdsspec-compiler/build.xml create mode 100755 cdsspec-compiler/clean.sh create mode 100755 cdsspec-compiler/generate.sh create mode 100644 cdsspec-compiler/grammer/util.jj create mode 100644 cdsspec-compiler/lib/javacc.jar create mode 100644 cdsspec-compiler/notes/definition.cc create mode 100644 cdsspec-compiler/notes/generated_code_examples.txt create mode 100644 cdsspec-compiler/notes/impl.txt create mode 100644 cdsspec-compiler/notes/interesting_examples.txt create mode 100644 cdsspec-compiler/notes/nondeterm-spec.txt create mode 100644 cdsspec-compiler/notes/register-example/Makefile create mode 100644 cdsspec-compiler/notes/register-example/cdsspec-generated.h create mode 100644 cdsspec-compiler/notes/register-example/register.cc create mode 100644 cdsspec-compiler/notes/register-example/register.cc.original create mode 100644 cdsspec-compiler/notes/register-example/register.h create mode 100644 cdsspec-compiler/notes/sequential_spec.txt create mode 100755 cdsspec-compiler/run-javacc.sh create mode 100644 cdsspec-compiler/src/edu/uci/eecs/codeGenerator/CodeAdditions.java create mode 100644 cdsspec-compiler/src/edu/uci/eecs/codeGenerator/CodeGenerator.java create mode 100644 cdsspec-compiler/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java create mode 100644 cdsspec-compiler/src/edu/uci/eecs/codeGenerator/Environment.java create mode 100644 cdsspec-compiler/src/edu/uci/eecs/specExtraction/Code.java create mode 100644 cdsspec-compiler/src/edu/uci/eecs/specExtraction/CommutativityRule.java create mode 100644 cdsspec-compiler/src/edu/uci/eecs/specExtraction/Construct.java create mode 100644 cdsspec-compiler/src/edu/uci/eecs/specExtraction/DefineConstruct.java create mode 100644 cdsspec-compiler/src/edu/uci/eecs/specExtraction/EntryConstruct.java create mode 100644 cdsspec-compiler/src/edu/uci/eecs/specExtraction/FunctionHeader.java create mode 100644 cdsspec-compiler/src/edu/uci/eecs/specExtraction/GlobalConstruct.java create mode 100644 cdsspec-compiler/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java create mode 100644 cdsspec-compiler/src/edu/uci/eecs/specExtraction/OPConstruct.java create mode 100644 cdsspec-compiler/src/edu/uci/eecs/specExtraction/OPType.java create mode 100644 cdsspec-compiler/src/edu/uci/eecs/specExtraction/QualifiedName.java create mode 100644 cdsspec-compiler/src/edu/uci/eecs/specExtraction/SpecExtractor.java create mode 100644 cdsspec-compiler/src/edu/uci/eecs/specExtraction/SpecNaming.java create mode 100644 cdsspec-compiler/src/edu/uci/eecs/specExtraction/SpecUtils.java create mode 100644 cdsspec-compiler/src/edu/uci/eecs/specExtraction/VariableDeclaration.java create mode 100644 cdsspec-compiler/src/edu/uci/eecs/specExtraction/WrongAnnotationException.java create mode 100644 include/model_memory.h create mode 100644 spec-analysis/.gitignore create mode 100644 spec-analysis/Makefile create mode 100644 spec-analysis/cdsspec.h create mode 100644 spec-analysis/executiongraph.cc create mode 100644 spec-analysis/executiongraph.h create mode 100644 spec-analysis/include/specannotation-api.h create mode 100644 spec-analysis/methodcall.cc create mode 100644 spec-analysis/methodcall.h create mode 100644 spec-analysis/spec_common.h create mode 100644 spec-analysis/specanalysis.cc create mode 100644 spec-analysis/specanalysis.h create mode 100644 spec-analysis/specannotation.cc create mode 100644 spec-analysis/specannotation.h create mode 100644 test-cdsspec/Makefile create mode 100644 test-cdsspec/benchmarks.mk create mode 100644 test-cdsspec/chase-lev-deque-bugfix/Makefile create mode 100755 test-cdsspec/cleanse.sh create mode 100644 test-cdsspec/concurrent-hashmap/Makefile create mode 100644 test-cdsspec/include/unrelacy.h create mode 100644 test-cdsspec/linuxrwlocks/Makefile create mode 100644 test-cdsspec/mcs-lock/Makefile create mode 100644 test-cdsspec/mpmc-queue/Makefile create mode 100644 test-cdsspec/ms-queue/.gitignore create mode 100644 test-cdsspec/ms-queue/Makefile create mode 100755 test-cdsspec/performance.sh create mode 100644 test-cdsspec/read-copy-update/Makefile create mode 100755 test-cdsspec/run-all.sh create mode 100755 test-cdsspec/run.sh create mode 100644 test-cdsspec/seqlock/Makefile create mode 100644 test-cdsspec/spsc-bugfix/Makefile create mode 100644 test-cdsspec/ticket-lock/Makefile delete mode 100644 test/iriw.cc delete mode 100644 test/iriw_wildcard.cc 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(); + } +