From 17e2549eb9e16b6fd93b4f46bf501d94c0d79ebf Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Mon, 30 Mar 2015 11:35:00 -0700 Subject: [PATCH] changes --- barrier/result.txt | 13 +++++++++++++ linuxrwlocks/note.txt | 5 +++++ linuxrwlocks/result1.txt | 23 ++++++++++++++++++++++- linuxrwlocks/result2.txt | 8 ++++++++ seqlock/result.txt | 24 ++++++++++++++++++++++++ treiber-stack/result.txt | 14 ++++++++++++++ 6 files changed, 86 insertions(+), 1 deletion(-) create mode 100644 barrier/result.txt create mode 100644 seqlock/result.txt create mode 100644 treiber-stack/result.txt diff --git a/barrier/result.txt b/barrier/result.txt new file mode 100644 index 0000000..5eab816 --- /dev/null +++ b/barrier/result.txt @@ -0,0 +1,13 @@ +peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv/benchmarks$ time +./run.sh barrier/testcase -m2 -y -u3 -tSCFENCE -o weaken &> /scratch/a + +real 0m0.060s +user 0m0.031s +sys 0m0.018s + +Result 0: +wildcard 1 -> memory_order_relaxed +wildcard 2 -> memory_order_acq_rel +wildcard 3 -> memory_order_relaxed +wildcard 4 -> memory_order_release +wildcard 5 -> memory_order_acquire diff --git a/linuxrwlocks/note.txt b/linuxrwlocks/note.txt index 8f5a8af..26dcd2d 100644 --- a/linuxrwlocks/note.txt +++ b/linuxrwlocks/note.txt @@ -6,3 +6,8 @@ cases (plus corner cases) and then run each of them one after another. We ran testcase1 and then got inference result1.txt, then we ran testcase2 based on result1.txt, and we got result2.txt, which is the correct inference. + +result1.txt -> 1m56.110s +result2.txt -> 0m0.207s + +total -> 1m56.317s diff --git a/linuxrwlocks/result1.txt b/linuxrwlocks/result1.txt index a62c7e3..27838a5 100644 --- a/linuxrwlocks/result1.txt +++ b/linuxrwlocks/result1.txt @@ -1,3 +1,10 @@ +peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv$ time ./run.sh +benchmarks/linuxrwlocks/testcase1 -m2 -y -u3 -tSCFENCE -o weaken &> /scratch/a + +real 1m58.120s +user 1m56.110s +sys 0m1.909s + Result 0: wildcard 3 -> memory_order_acquire wildcard 4 -> memory_order_relaxed @@ -7,7 +14,21 @@ wildcard 7 -> memory_order_acquire wildcard 8 -> memory_order_relaxed wildcard 9 -> memory_order_relaxed wildcard 10 -> memory_order_acquire -wildcard 13 -> memory_order_relaxed +wildcard 13 -> memory_order_acquire +wildcard 14 -> memory_order_relaxed +wildcard 15 -> memory_order_release +wildcard 16 -> memory_order_release + +Result 1: +wildcard 3 -> memory_order_acquire +wildcard 4 -> memory_order_relaxed +wildcard 5 -> memory_order_relaxed +wildcard 6 -> memory_order_acquire +wildcard 7 -> memory_order_acquire +wildcard 8 -> memory_order_relaxed +wildcard 9 -> memory_order_acquire +wildcard 10 -> memory_order_acquire +wildcard 13 -> memory_order_acquire wildcard 14 -> memory_order_relaxed wildcard 15 -> memory_order_release wildcard 16 -> memory_order_release diff --git a/linuxrwlocks/result2.txt b/linuxrwlocks/result2.txt index fcaca92..68ca03a 100644 --- a/linuxrwlocks/result2.txt +++ b/linuxrwlocks/result2.txt @@ -1,3 +1,11 @@ +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 + +real 0m0.291s +user 0m0.207s +sys 0m0.006s + Result 0: wildcard 1 -> memory_order_relaxed wildcard 2 -> memory_order_relaxed diff --git a/seqlock/result.txt b/seqlock/result.txt new file mode 100644 index 0000000..2631c4a --- /dev/null +++ b/seqlock/result.txt @@ -0,0 +1,24 @@ +peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv$ time ./run.sh +benchmarks/seqlock/testcase1 -m2 -y -u3 -tSCFENCE -o weaken &> /scratch/a + +real 0m0.390s +user 0m0.363s +sys 0m0.018s + +Result 0: +wildcard 1 -> memory_order_acquire +wildcard 2 -> memory_order_acquire +wildcard 3 -> memory_order_relaxed +wildcard 4 -> memory_order_acquire +wildcard 5 -> memory_order_relaxed +wildcard 7 -> memory_order_release +wildcard 8 -> memory_order_release + +Result 1: +wildcard 1 -> memory_order_acquire +wildcard 2 -> memory_order_acquire +wildcard 3 -> memory_order_relaxed +wildcard 4 -> memory_order_relaxed +wildcard 5 -> memory_order_acquire +wildcard 7 -> memory_order_release +wildcard 8 -> memory_order_release diff --git a/treiber-stack/result.txt b/treiber-stack/result.txt new file mode 100644 index 0000000..e129376 --- /dev/null +++ b/treiber-stack/result.txt @@ -0,0 +1,14 @@ +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 + +real 0m0.031s +user 0m0.018s +sys 0m0.002s + +Result 0: +wildcard 1 -> memory_order_relaxed +wildcard 2 -> memory_order_relaxed +wildcard 3 -> memory_order_release +wildcard 5 -> memory_order_acquire +wildcard 6 -> memory_order_relaxed -- 2.34.1