Refactor

* Add A* search
* Add squash reads
* Add held variables
* Refactor file structure
* Implement Closure
* Implement IncludeSet
* Revamp Closure using vector clock algorithm
* Add parallel execution
* Clean up makefile
* Remove extra traces, logs, scripts

Author: bryanljx

README.md

@@ -6,29 +6,49 @@
 
 ## Building and Running 
 
+### Building
 To build: 
 ```sh
 make all
 ```
 
+### Command Line flags
+The executable `verify_sc` takes in the following flags:
+
+- `-v`, `--verbose`
+  - Prints more verbose output to stdout
+- `-w`, `--witness`
+  - Enables generation of witness for data races predicted 
+- `-o <OUTPUT_DIR>`, `--outputDir <OUTPUT_DIR>`
+  - <OUTPUT_DIR> for generated witness 
+  - Requires `-w` or `--witness` flag for witnesses to be generated
+- `-p <NUM_THREADS>`, `--parallel <NUM_THREADS>`
+  - Execute <NUM_THREADS> in parallel
+  
+All flags are optional.
+
+### Running
 To run: 
+
 ```sh
-make run INPUT=<INPUT_FILE> 
+./bin/verify_sc <INPUT_TRACE> -v -w -o <WITNESS_DIR> -p <NUM_THREADS>
 ```
 
-To run with debug info enabled:
-
+For convenience, some additional makefile targets are provided:
 ```sh
-make debug INPUT=<INPUT_FILE>
+make run INPUT=<INPUT_FILE> NUM_THREADS=<NUM_THREADS>
 ```
 
-## Trace Generation
+This combines building and running together. Witness generation, however, is disabled for speed. Modify the makefile as needed.
 
-The chosen format for an event is an `uint64_t` as follows:
-  - 4 bits event identifier
-  - 8 bits thread identifier 
-  - 20 bits variable
-  
-This project reads and parses traces from a binary file where each event is represented using the above format. 
 
-For convenience, scripts are provided to convert human-readable as well as STD format to the binary format expected. Use one of `make gen_from_std_trace` to convert to human-readable format and `make gen_traces` to convert from human-readable format to the required binary file. 
+## Trace Format
+~enumerate_race_detection~ support the following events: 
+- Read/Write
+- Acquire/Release
+- Begin/End
+- Fork/Join
+
+Each event are represented using 64 bits: 4 bits event identifier, 8 bits thread identifier, 20 bits variable dentifer, 32 bits variable value. 
+
+Input traces are assumed to be binary files where each line consists of a 64 bit representing an event.

logs/csv/input9.csv

@@ -1,92 +1,39 @@
 CXX = g++
-CXXFLAGS = -std=c++17
+CXXFLAGS = -std=c++20
 
 DEBUGFLAGS = -DDEBUG
 
 BIN_DIR=bin
 SRC_DIR=src
 
 TRACE_DIR=trace
-STD_TRACE_DIR=$(TRACE_DIR)/STD_Format
-TEST_TRACE_DIR=$(TRACE_DIR)/test
-HUMANREADABLE_TRACE_DIR=$(TRACE_DIR)/human_readable_trace
-FORMATTED_TRACE_DIR=$(TRACE_DIR)/binary_trace
+WITNESS_DIR=witness
 
 TARGET = $(BIN_DIR)/verify_sc
-TRACE_GENERATOR = $(BIN_DIR)/trace_generator
 
-SRC = $(SRC_DIR)/main.cpp
-DEPS = $(wildcard $(SRC_DIR)/common/*.cpp) $(wildcard $(SRC_DIR)/consistency_checker/.cpp) $(SRC_DIR)/parsing/parser.cpp
+SRC = $(wildcard $(SRC_DIR)/*.cpp)
+DEPS = $(wildcard $(SRC_DIR)/*.hpp)
 
-TRACE_GENERATOR_SRC = $(SRC_DIR)/trace_generator.cpp
-TRACE_GENERATOR_DEPS = $(SRC_DIR/common/event.cpp) $(SRC_DIR/parsing/trace_conversion.cpp)
-
-STD_CONVERTER=scripts/convert.py
-TEST_CONVERTER=scripts/convert_test.py
-
-readable_traces = $(shell ls $(HUMANREADABLE_TRACE_DIR)/*.txt)
-INPUT = trace/binary_trace/input1.txt
-SIZE = 100
-
-CSV_GENERATOR = scripts/benchmark_to_csv.py
-LOG_DIR = logs/output
-CSV_DIR = logs/csv
-
-PREP_CSV_GENERATOR = scripts/prep_csv.py
-PREP_CSV_DIR = logs/combined
+INPUT = input.txt
+NUM_THREADS = 8
 
 all: $(TARGET)
 
 run: clean $(TARGET)
 	@echo "Running with input file: $(INPUT)"
 	@echo ""
-	@./$(TARGET) $(INPUT) -s $(SIZE) -v
+	@./$(TARGET) $(INPUT) -v -o $(WITNESS_DIR) -p $(NUM_THREADS)
 
 debug: clean $(SRC) $(DEPS)
 	mkdir -p $(BIN_DIR)
 	$(CXX) $(CXXFLAGS) $(DEBUGFLAGS) -o $(TARGET) $(SRC)
-	./$(TARGET) $(INPUT) -s $(SIZE) -v
-
-benchmark: clean $(SRC) $(DEPS)
-	mkdir -p $(BIN_DIR)
-	$(CXX) $(CXXFLAGS) $(DEBUGFLAGS) -o $(TARGET) $(SRC)
-	command time -v ./$(TARGET) $(INPUT) -s $(SIZE) -v
+	./$(TARGET) $(INPUT) -v -o $(WITNESS_DIR) -p $(NUM_THREADS)
 
 $(TARGET): $(SRC) $(DEPS)
 	mkdir -p $(BIN_DIR)
 	$(CXX) $(CXXFLAGS) -o $(TARGET) $(SRC)
 
-$(TRACE_GENERATOR): $(TRACE_GENERATOR_SRC) $(TRACE_GENERATOR_DEPS)
-	mkdir -p $(BIN_DIR)
-	$(CXX) $(CXXFLAGS) -o $(TRACE_GENERATOR) $(TRACE_GENERATOR_SRC)
-
-gen_from_std_trace:
-	mkdir -p $(HUMANREADABLE_TRACE_DIR)
-	python3 $(STD_CONVERTER) $(STD_TRACE_DIR) $(HUMANREADABLE_TRACE_DIR)
-
-gen_single_trace: $(TRACE_GENERATOR)
-	mkdir -p $(FORMATTED_TRACE_DIR)
-	$(TRACE_GENERATOR) $(args) $(FORMATTED_TRACE_DIR)
-
-gen_from_test_trace:
-	mkdir -p $(HUMANREADABLE_TRACE_DIR)
-	python3 $(TEST_CONVERTER) $(TEST_TRACE_DIR) $(HUMANREADABLE_TRACE_DIR)
-
-gen_traces: $(TRACE_GENERATOR)
-	mkdir -p $(FORMATTED_TRACE_DIR)
-	@for file in $(readable_traces); do \
-		echo "Generating trace for $$file..."; \
-		$(TRACE_GENERATOR) $$file $(FORMATTED_TRACE_DIR);\
-	done
-
-.PHONY = gen_csv prep_csv
-gen_csv:
-	python3 $(CSV_GENERATOR) $(LOG_DIR) $(CSV_DIR)
-
-prep_csv:
-	rm $(PREP_CSV_DIR)/*
-	python3 $(PREP_CSV_GENERATOR) $(CSV_DIR) $(PREP_CSV_DIR)
-
 # Clean target to remove the compiled files
 clean:
-	rm -f $(TARGET) $(TRACE_GENERATOR) $(TARGET_STRICT)
+	rm -f $(TARGET)
+	rm -rf $(WTINESS_DIR)