From: Peizhao Ou Date: Wed, 5 Aug 2015 22:21:04 +0000 (-0700) Subject: edits X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=897165f73e9501261756fc8d3ead29013f4b022f;p=model-checker-benchmarks.git edits --- diff --git a/Makefile b/Makefile index e124a04..4c96e10 100644 --- 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 5eab816..bdfe6dd 100644 --- 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 be8390f..74c5f2b 100644 --- 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 f6af1b9..9ce70ff 100644 --- 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 d19d5fd..3565d6d 100644 --- 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 463d133..b9dfa84 100644 --- 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 5d8c42b..748bc38 100644 --- 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 4218d43..0b9a887 100644 --- 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 a47e66d..1b50551 100644 --- 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 176baf3..c22d5b5 100644 --- 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 20c6aca..908202a 100644 --- 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 9d3d5f1..ce9f031 100644 --- 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 27838a5..e992b3d 100644 --- 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 68ca03a..4b143b5 100644 --- 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 2c0ce45..192ae74 100644 --- 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 07a4013..ad6a854 100644 --- 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 95aa6bb..219d8c3 100644 --- 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 646ec97..d5fd6c8 100644 --- 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 e26b8d5..ca22779 100644 --- 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 2631c4a..6e2a8b0 100644 --- 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 19ab37d..1ab35ac 100644 --- 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 e129376..5201081 100644 --- 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