edits

diff --git a/Makefile b/Makefile
index e124a0472fb7500b796a7eca6cfbdf74b91ec964..4c96e107d2a0fcdf3e7c00d2c30220f64d4d658d 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -1,6 +1,7 @@
 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
+       concurrent-hashmap seqlock spsc-example spsc-queue-scfence \
+       treiber-stack
 
 .PHONY: $(DIRS)
 

diff --git a/barrier/result.txt b/barrier/result.txt
index 5eab816eb81cc954d85ff720e0a482858794b489..bdfe6dd4051ee10a4cd865a5d3fc81dd9dd22d29 100644 (file)
--- a/barrier/result.txt
+++ b/barrier/result.txt
@@ -1,5 +1,5 @@
 peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv/benchmarks$ time
-./run.sh barrier/testcase -m2 -y -u3 -tSCFENCE -o weaken &> /scratch/a
+./run.sh barrier/testcase -m2 -y -u3 -tSCFENCE &> /scratch/a
 
 real   0m0.060s
 user   0m0.031s

diff --git a/chase-lev-deque-bugfix/result1.txt b/chase-lev-deque-bugfix/result1.txt
index be8390fdc9abfbe26d7d9dfcf8aaab46f864b1a3..74c5f2bf03ebc79f325a58d7bde0ebb25316ed7c 100644 (file)
--- a/chase-lev-deque-bugfix/result1.txt
+++ b/chase-lev-deque-bugfix/result1.txt
@@ -1,6 +1,5 @@
-peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv/benchmarks$ time
-./run.sh chase-lev-deque-bugfix/testcase1_wildcard -m2 -y -u3 -tSCFENCE -o
-weaken &> /scratch/a
+peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv/benchmarks$
+time ./run.sh benchmarks/chase-lev-deque-bugfix/testcase1_wildcard -m2 -y -u3 -tSCFENCE &> /scratch/a
 
 real   0m0.032s
 user   0m0.013s

diff --git a/chase-lev-deque-bugfix/result2.txt b/chase-lev-deque-bugfix/result2.txt
index f6af1b9f6d0fb8d3e8147491337f7f062125e61e..9ce70ff857663462e0a22d032b3940906d4816b6 100644 (file)
--- a/chase-lev-deque-bugfix/result2.txt
+++ b/chase-lev-deque-bugfix/result2.txt
@@ -1,6 +1,5 @@
-peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv/benchmarks$ time
-./run.sh chase-lev-deque-bugfix/testcase2_wildcard -m2 -y -u3 -tSCFENCE -o
-fchase-lev-deque-bugfix/result1.txt -o weaken &> /scratch/a
+peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv/benchmarks$ 
+time ./run.sh benchmarks/chase-lev-deque-bugfix/testcase2_wildcard -m2 -y -u3 -tSCFENCE -o file-benchmarks/chase-lev-deque-bugfix/result1.txt &> /scratch/a
 
 real   0m0.061s
 user   0m0.028s

diff --git a/chase-lev-deque-bugfix/result3.txt b/chase-lev-deque-bugfix/result3.txt
index d19d5fddc97552093f5067663fa2385ede6e405f..3565d6d770da94dccd09c5e8bc415ebc5dc5bbd2 100644 (file)
--- a/chase-lev-deque-bugfix/result3.txt
+++ b/chase-lev-deque-bugfix/result3.txt
@@ -1,6 +1,5 @@
-peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv/benchmarks$ time
-./run.sh chase-lev-deque-bugfix/testcase3_wildcard -m2 -y -u3 -tSCFENCE -o
-fchase-lev-deque-bugfix/result2.txt -o weaken &> /scratch/a
+peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv/benchmarks$ 
+time ./run.sh benchmarks/chase-lev-deque-bugfix/testcase3_wildcard -m2 -y -u3 -tSCFENCE -o file-benchmarks/chase-lev-deque-bugfix/result2.txt &> /scratch/a
 
 real   0m6.858s
 user   0m6.264s

diff --git a/chase-lev-deque-bugfix/result4.txt b/chase-lev-deque-bugfix/result4.txt
index 463d1335b658be8ac8a11193dcbef050a0ae5aad..b9dfa84b5aa0c851aa251b67194f912befad1788 100644 (file)
--- a/chase-lev-deque-bugfix/result4.txt
+++ b/chase-lev-deque-bugfix/result4.txt
@@ -1,6 +1,5 @@
-peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv/benchmarks$ time
-./run.sh chase-lev-deque-bugfix/testcase4_wildcard -m2 -y -u3 -tSCFENCE -o
-fchase-lev-deque-bugfix/result3.txt -o weaken &> /scratch/a
+peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv/benchmarks$ 
+time ./run.sh benchmarks/chase-lev-deque-bugfix/testcase4_wildcard -m2 -y -u3 -tSCFENCE -o file-benchmarks/chase-lev-deque-bugfix/result3.txt &> /scratch/a
 
 real   0m0.918s
 user   0m0.824s

diff --git a/chase-lev-deque-bugfix/result5.txt b/chase-lev-deque-bugfix/result5.txt
index 5d8c42b70cc9e5bb119e4fee5dbd9b49facfa26b..748bc387786d58846f932b9300f5b0bab45db755 100644 (file)
--- a/chase-lev-deque-bugfix/result5.txt
+++ b/chase-lev-deque-bugfix/result5.txt
@@ -1,6 +1,5 @@
-peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv/benchmarks$ time
-./run.sh chase-lev-deque-bugfix/testcase5_wildcard -m2 -y -u3 -tSCFENCE -o
-fchase-lev-deque-bugfix/result4.txt -o weaken &> /scratch/a
+peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv/benchmarks$ 
+time ./run.sh benchmarks/chase-lev-deque-bugfix/testcase5_wildcard -m2 -y -u3 -tSCFENCE -o file-benchmarks/chase-lev-deque-bugfix/result4.txt &> /scratch/a
 
 real   0m0.088s
 user   0m0.054s

diff --git a/chase-lev-deque-bugfix/result6.txt b/chase-lev-deque-bugfix/result6.txt
index 4218d43d2b02b80e1ecef160e2f6e1ece3d3cf84..0b9a887880782892df1f08b194456504128b8bab 100644 (file)
--- a/chase-lev-deque-bugfix/result6.txt
+++ b/chase-lev-deque-bugfix/result6.txt
@@ -1,6 +1,5 @@
-peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv/benchmarks$ time
-./run.sh chase-lev-deque-bugfix/testcase6_wildcard -m2 -y -u3 -tSCFENCE -o
-fchase-lev-deque-bugfix/result5.txt -o weaken &> /scratch/a
+peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv/benchmarks$ 
+time ./run.sh benchmarks/chase-lev-deque-bugfix/testcase6_wildcard -m2 -y -u3 -tSCFENCE -o file-benchmarks/chase-lev-deque-bugfix/result5.txt &> /scratch/a
 
 real   10m3.700s
 user   9m19.887s

diff --git a/concurrent-hashmap/result1.txt b/concurrent-hashmap/result1.txt
index a47e66db703da8e365f0936d7260f2cd3f8956c1..1b50551a51936070df766710b8a15d0c5d3079e5 100644 (file)
--- a/concurrent-hashmap/result1.txt
+++ b/concurrent-hashmap/result1.txt
@@ -1,6 +1,5 @@
-peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv$ time ./run.sh
-benchmarks/concurrent-hashmap/testcase1_wildcard -m2 -y -u3 -tSCFENCE -o weaken
-&> /scratch/a
+peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv$
+time ./run.sh benchmarks/concurrent-hashmap/testcase1_wildcard -m2 -y -u3 -tSCFENCE &> /scratch/a
 
 real   0m0.031s
 user   0m0.015s

diff --git a/concurrent-hashmap/result2.txt b/concurrent-hashmap/result2.txt
index 176baf34dd0bebcf186301c0f7ea075993a98441..c22d5b5f9d21f29d789b25261ba1585e5f62dcd5 100644 (file)
--- a/concurrent-hashmap/result2.txt
+++ b/concurrent-hashmap/result2.txt
@@ -1,6 +1,5 @@
-peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv$ time ./run.sh
-benchmarks/concurrent-hashmap/testcase2_wildcard -m2 -y -u3 -tSCFENCE -o weaken
--o fbenchmarks/concurrent-hashmap/result1.txt -o annotation  &> /scratch/a
+peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv$ 
+time ./run.sh benchmarks/concurrent-hashmap/testcase2_wildcard -m2 -y -u3 -tSCFENCE -o file-benchmarks/concurrent-hashmap/result1.txt -o anno &> /scratch/a
 
 real   0m0.027s
 user   0m0.000s

diff --git a/dekker-fences/result1.txt b/dekker-fences/result1.txt
index 20c6aca95a8639d3dbb687442d1347a292628845..908202a9f6ac0cbeae526235dbc72f490d670bdf 100644 (file)
--- a/dekker-fences/result1.txt
+++ b/dekker-fences/result1.txt
@@ -1,6 +1,5 @@
-peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv$ time ./run.sh
-benchmarks/dekker-fences/dekker-fences-wildcard1 -m2 -y -u3 -tSCFENCE -o weaken
-&> /scratch/a
+peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv$
+time ./run.sh benchmarks/dekker-fences/dekker-fences-wildcard1 -m2 -y -u3 -tSCFENCE &> /scratch/a
 
 real   1m27.052s
 user   1m20.790s

diff --git a/dekker-fences/result2.txt b/dekker-fences/result2.txt
index 9d3d5f12ce89f5f004c206fcee1276ffeae65626..ce9f031fbe66e72298650bb0a5f1678171c00dcc 100644 (file)
--- a/dekker-fences/result2.txt
+++ b/dekker-fences/result2.txt
@@ -1,6 +1,5 @@
-peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv$ time ./run.sh
-benchmarks/dekker-fences/dekker-fences-wildcard2 -m2 -y -u3 -tSCFENCE -o weaken
--o fbenchmarks/dekker-fences/result1.txt -x10000 &> /scratch/a
+peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv$
+time ./run.sh benchmarks/dekker-fences/dekker-fences-wildcard2 -m2 -y -u3 -tSCFENCE -o file-benchmarks/dekker-fences/result1.txt -x10000 &> /scratch/a
 
 real   5m43.236s
 user   5m19.538s

diff --git a/linuxrwlocks/result1.txt b/linuxrwlocks/result1.txt
index 27838a5dec5d2b4c34f5757018a87c9e59e4eb65..e992b3d173bf0a0d7459d12b59416e24ff44305a 100644 (file)
--- a/linuxrwlocks/result1.txt
+++ b/linuxrwlocks/result1.txt
@@ -1,5 +1,5 @@
-peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv$ time ./run.sh
-benchmarks/linuxrwlocks/testcase1 -m2 -y -u3 -tSCFENCE -o weaken &> /scratch/a
+peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv$
+time ./run.sh benchmarks/linuxrwlocks/testcase1 -m2 -y -u3 -tSCFENCE &> /scratch/a
 
 real   1m58.120s
 user   1m56.110s

diff --git a/linuxrwlocks/result2.txt b/linuxrwlocks/result2.txt
index 68ca03a569b9f0caeaafb5784106d2595aaf782e..4b143b5524d58795b40464668514070dc62992a1 100644 (file)
--- a/linuxrwlocks/result2.txt
+++ b/linuxrwlocks/result2.txt
@@ -1,6 +1,5 @@
-peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv$ time ./run.sh
-benchmarks/linuxrwlocks/testcase2 -m2 -y -u3 -tSCFENCE -o weaken -o
-fbenchmarks/linuxrwlocks/result1.txt &> /scratch/a
+peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv$
+time ./run.sh benchmarks/linuxrwlocks/testcase2 -m2 -y -u3 -tSCFENCE -o file-benchmarks/linuxrwlocks/result1.txt &> /scratch/a
 
 real   0m0.291s
 user   0m0.207s

diff --git a/mcs-lock/result.txt b/mcs-lock/result.txt
index 2c0ce45f0b3444dde68504c060c68b20823611c0..192ae7451ff381f314b895cc06547fdbc56264fa 100644 (file)
--- a/mcs-lock/result.txt
+++ b/mcs-lock/result.txt
@@ -1,6 +1,5 @@
-peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv$ time ./run.sh
-benchmarks/mcs-lock/testcase1 -m2 -y -u3 -b100 -tSCFENCE -o weaken -o m &>
-/scratch/a
+peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv$
+time ./run.sh benchmarks/mcs-lock/testcase1 -m2 -y -u3 -b100 -tSCFENCE -o implicit-mo &> /scratch/a
 
 real   0m12.838s
 user   0m11.925s

diff --git a/mpmc-queue/result1.txt b/mpmc-queue/result1.txt
index 07a40136e6756a894ca01b9b7379706de24272e0..ad6a8544a38526cc3509b6b1976434c14eddc836 100644 (file)
--- a/mpmc-queue/result1.txt
+++ b/mpmc-queue/result1.txt
@@ -1,6 +1,5 @@
-peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv$ time ./run.sh
-benchmarks/mpmc-queue/testcase1 -m2 -Y -u3 -tSCFENCE -o weaken -o
-fbenchmarks/mpmc-queue/result1.txt   &> /scratch/a
+peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv$
+time ./run.sh benchmarks/mpmc-queue/testcase1 -m2 -Y -u3 -tSCFENCE &> /scratch/a
 
 real   0m0.162s
 user   0m0.143s
@@ -15,3 +14,22 @@ wildcard 5 -> memory_order_relaxed
 wildcard 6 -> memory_order_relaxed
 wildcard 7 -> memory_order_acquire
 wildcard 8 -> memory_order_release
+
+--------------------------------------------------------------------------------
+
+peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv$
+time ./run.sh benchmarks/mpmc-queue/testcase1 -m2 -y -u3 -tSCFENCE &> /scratch/a
+
+Result 0:
+wildcard 1 -> memory_order_seq_cst
+wildcard 2 -> memory_order_release
+wildcard 3 -> memory_order_acquire
+wildcard 4 -> memory_order_seq_cst
+wildcard 5 -> memory_order_relaxed
+wildcard 6 -> memory_order_seq_cst
+wildcard 7 -> memory_order_seq_cst
+wildcard 8 -> memory_order_release
+
+real   0m0.403s
+user   0m0.348s
+sys    0m0.047s

diff --git a/ms-queue/result1.txt b/ms-queue/result1.txt
index 95aa6bb0d2b397166dda921639b127de648b5e31..219d8c392621681bd6b8fb29819b8282931ba260 100644 (file)
--- a/ms-queue/result1.txt
+++ b/ms-queue/result1.txt
@@ -1,6 +1,5 @@
-peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv$ time ./run.sh
-benchmarks/ms-queue/testcase1_wildcard -m2 -y -u3 -tSCFENCE -o weaken &>
-/scratch/a
+peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv$ 
+time ./run.sh benchmarks/ms-queue/testcase1_wildcard -m2 -y -u3 -tSCFENCE &> /scratch/a
 
 real   0m15.210s
 user   0m14.826s

diff --git a/ms-queue/result2.txt b/ms-queue/result2.txt
index 646ec9730862394e6ec7dc02728cae75fae1a2a9..d5fd6c8f4a43eea3e077a07ea1703b9d18c0c347 100644 (file)
--- a/ms-queue/result2.txt
+++ b/ms-queue/result2.txt
@@ -1,6 +1,5 @@
-peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv$ time ./run.sh
-benchmarks/ms-queue/testcase2_wildcard -m2 -y -u3 -tSCFENCE -o weaken -o
-fbenchmarks/ms-queue/result1.txt &> /scratch/a
+peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv$ 
+time ./run.sh benchmarks/ms-queue/testcase2_wildcard -m2 -y -u3 -tSCFENCE -o file-benchmarks/ms-queue/result1.txt &> /scratch/a
 
 real   0m1.339s
 user   0m1.289s

diff --git a/ms-queue/result3.txt b/ms-queue/result3.txt
index e26b8d5346116347df5a3479a4c60b228b694358..ca22779d7a92a638051d328b33b0b7b860c22b7c 100644 (file)
--- a/ms-queue/result3.txt
+++ b/ms-queue/result3.txt
@@ -1,6 +1,5 @@
-peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv$ time ./run.sh
-benchmarks/ms-queue/testcase3_wildcard -m2 -y -u3 -tSCFENCE -o
-fbenchmarks/ms-queue/result2.txt -o weaken  &> /scratch/a
+peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv$ 
+time ./run.sh benchmarks/ms-queue/testcase3_wildcard -m2 -y -u3 -tSCFENCE -o file-benchmarks/ms-queue/result2.txt &> /scratch/a
 
 real   0m1.040s
 user   0m0.930s

diff --git a/seqlock/result.txt b/seqlock/result.txt
index 2631c4a368c41ad71e6e6bf879f7539fda2f0092..6e2a8b0524ac1079f1f064447edf41fb6c5ed9bc 100644 (file)
--- a/seqlock/result.txt
+++ b/seqlock/result.txt
@@ -1,5 +1,5 @@
-peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv$ time ./run.sh
-benchmarks/seqlock/testcase1 -m2 -y -u3 -tSCFENCE -o weaken &> /scratch/a
+peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv$
+time ./run.sh benchmarks/seqlock/testcase1 -m2 -y -u3 -tSCFENCE &> /scratch/a
 
 real   0m0.390s
 user   0m0.363s

diff --git a/spsc-queue-scfence/result.txt b/spsc-queue-scfence/result.txt
index 19ab37db5493871209489f03fc379188c3021253..1ab35ac1870101ea7ca1b6a50ed821623f78d978 100644 (file)
--- a/spsc-queue-scfence/result.txt
+++ b/spsc-queue-scfence/result.txt
@@ -1,6 +1,5 @@
-peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv/benchmarks$ time
-./run.sh spsc-queue-scfence/spsc-queue -m2 -y -u3 -tSCFENCE -o weaken  &>
-/scratch/a
+peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv/benchmarks$
+time ./run.sh benchmarks/spsc-queue-scfence/spsc-queue -m2 -y -u3 -tSCFENCE &> /scratch/a
 
 real   0m0.050s
 user   0m0.004s

diff --git a/treiber-stack/result.txt b/treiber-stack/result.txt
index e12937604b60e984919227a49b03040d778f85db..5201081ed93d623e9c33a65d62a27daeca5d43ba 100644 (file)
--- a/treiber-stack/result.txt
+++ b/treiber-stack/result.txt
@@ -1,6 +1,5 @@
-peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv/benchmarks$ time
-./run.sh  treiber-stack/testcase1_wildcard -m2 -y -u3 -tSCFENCE -o weaken &>
-/scratch/a
+peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv/benchmarks$ 
+time ./run.sh  benchmarks/treiber-stack/testcase1_wildcard -m2 -y -u3 -tSCFENCE &> /scratch/a
 
 real   0m0.031s
 user   0m0.018s