edits
[cdsspec-compiler.git] / generate.sh
index f91e55b38acd52922b2ac03dfaa6f181c30b1549..38ec8b2a41e5e2f7e89678aa5877560158a5dbc8 100755 (executable)
@@ -1,9 +1,19 @@
 #!/bin/bash
 
-BENCH=(register ms-queue linuxrwlocks mcs-lock chase-lev-deque-bugfix treiber-stack)
+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 
+Class=edu/uci/eecs/codeGenerator/CodeGenerator
 
-java -cp $ClassPath $Class ${BENCH[*]}
+# 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[*]}