From d0adbc3c9d1f23d285f35b6a1a883bc8ddb7d51e Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Sun, 22 Mar 2015 00:28:37 -0700 Subject: [PATCH] results for mcs-lock --- mcs-lock/note.txt | 2 ++ mcs-lock/result.txt | 29 +++++++++++++++++++++++++++++ 2 files changed, 31 insertions(+) create mode 100644 mcs-lock/result.txt diff --git a/mcs-lock/note.txt b/mcs-lock/note.txt index aeef26e..8fe59f0 100644 --- a/mcs-lock/note.txt +++ b/mcs-lock/note.txt @@ -23,3 +23,5 @@ peizhaoo@dw-2:~/model-checker$ ./run.sh mcs-lock/testcase1 -m2 -b100 -y -tSCFENC The '-b100' is to terminate the execution in case of infinite loops because of improper synchronization at the beginning period. The 'm' option for SCFENCE analysis is to turn on the implyMO mode. + +It took to finish!! diff --git a/mcs-lock/result.txt b/mcs-lock/result.txt new file mode 100644 index 0000000..2c0ce45 --- /dev/null +++ b/mcs-lock/result.txt @@ -0,0 +1,29 @@ +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 + +real 0m12.838s +user 0m11.925s +sys 0m0.834s + +Result 0: +wildcard 1 -> memory_order_relaxed +wildcard 2 -> memory_order_relaxed +wildcard 3 -> memory_order_acq_rel +wildcard 4 -> memory_order_release +wildcard 5 -> memory_order_acquire +wildcard 6 -> memory_order_acquire +wildcard 7 -> memory_order_acq_rel +wildcard 8 -> memory_order_relaxed +wildcard 9 -> memory_order_release + +Result 1: +wildcard 1 -> memory_order_relaxed +wildcard 2 -> memory_order_relaxed +wildcard 3 -> memory_order_acq_rel +wildcard 4 -> memory_order_release +wildcard 5 -> memory_order_acquire +wildcard 6 -> memory_order_acquire +wildcard 7 -> memory_order_release +wildcard 8 -> memory_order_acquire +wildcard 9 -> memory_order_release -- 2.34.1