From ce26a518f60749f4fa7bf0ee03f5c6929aed9533 Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Sun, 22 Mar 2015 00:55:17 -0700 Subject: [PATCH] ms-queue result --- ms-queue/Makefile | 2 +- ms-queue/note.txt | 6 ++++++ ms-queue/result1.txt | 43 ++++++++++--------------------------------- ms-queue/result2.txt | 26 +++++++++++++++++++++++++- 4 files changed, 42 insertions(+), 35 deletions(-) diff --git a/ms-queue/Makefile b/ms-queue/Makefile index 55a4edb..566aee0 100644 --- a/ms-queue/Makefile +++ b/ms-queue/Makefile @@ -23,4 +23,4 @@ $(NORMAL_TESTS): % : %.c $(BENCH).o $(CC) -o $@ $^ $(CFLAGS) $(LDFLAGS) clean: - rm -f *.o *.d $(TESTS) + rm -f *.o *.d $(TESTS) main diff --git a/ms-queue/note.txt b/ms-queue/note.txt index eb2b995..00a645c 100644 --- a/ms-queue/note.txt +++ b/ms-queue/note.txt @@ -4,3 +4,9 @@ result2.txt. We can't infer the wildcard(4) to be acquire because we can't reach "that case"!!! See http://stackoverflow.com/questions/3873689/lock-free-queue-algorithm-repeated-reads-for-consistency + + +result1.txt -> 0m14.826s +result2.txt -> 0m1.289s + +total -> 0m 16.115 diff --git a/ms-queue/result1.txt b/ms-queue/result1.txt index f1c01e6..95aa6bb 100644 --- a/ms-queue/result1.txt +++ b/ms-queue/result1.txt @@ -1,8 +1,16 @@ +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 + +real 0m15.210s +user 0m14.826s +sys 0m0.362s + Result 0: wildcard 1 -> memory_order_relaxed wildcard 2 -> memory_order_relaxed wildcard 3 -> memory_order_acquire -wildcard 4 -> memory_order_relaxed +wildcard 4 -> memory_order_acquire wildcard 5 -> memory_order_relaxed wildcard 6 -> memory_order_acq_rel wildcard 8 -> memory_order_relaxed @@ -14,6 +22,7 @@ wildcard 15 -> memory_order_acquire wildcard 16 -> memory_order_relaxed wildcard 17 -> memory_order_release wildcard 19 -> memory_order_relaxed + Result 1: wildcard 1 -> memory_order_relaxed wildcard 2 -> memory_order_relaxed @@ -30,35 +39,3 @@ wildcard 15 -> memory_order_acquire wildcard 16 -> memory_order_relaxed wildcard 17 -> memory_order_release wildcard 19 -> memory_order_relaxed -Result 2: -wildcard 1 -> memory_order_relaxed -wildcard 2 -> memory_order_relaxed -wildcard 3 -> memory_order_acquire -wildcard 4 -> memory_order_relaxed -wildcard 5 -> memory_order_relaxed -wildcard 6 -> memory_order_acq_rel -wildcard 8 -> memory_order_relaxed -wildcard 9 -> memory_order_acq_rel -wildcard 11 -> memory_order_release -wildcard 13 -> memory_order_relaxed -wildcard 14 -> memory_order_acquire -wildcard 15 -> memory_order_acquire -wildcard 16 -> memory_order_relaxed -wildcard 17 -> memory_order_release -wildcard 19 -> memory_order_relaxed -Result 3: -wildcard 1 -> memory_order_relaxed -wildcard 2 -> memory_order_relaxed -wildcard 3 -> memory_order_acquire -wildcard 4 -> memory_order_relaxed -wildcard 5 -> memory_order_relaxed -wildcard 6 -> memory_order_release -wildcard 8 -> memory_order_acquire -wildcard 9 -> memory_order_acq_rel -wildcard 11 -> memory_order_release -wildcard 13 -> memory_order_relaxed -wildcard 14 -> memory_order_acquire -wildcard 15 -> memory_order_acquire -wildcard 16 -> memory_order_relaxed -wildcard 17 -> memory_order_release -wildcard 19 -> memory_order_relaxed diff --git a/ms-queue/result2.txt b/ms-queue/result2.txt index eae4d2b..646ec97 100644 --- a/ms-queue/result2.txt +++ b/ms-queue/result2.txt @@ -1,10 +1,34 @@ +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 -Result 1: +real 0m1.339s +user 0m1.289s +sys 0m0.038s + +Result 0: wildcard 1 -> memory_order_relaxed wildcard 2 -> memory_order_relaxed wildcard 3 -> memory_order_acquire wildcard 4 -> memory_order_relaxed wildcard 5 -> memory_order_relaxed +wildcard 6 -> memory_order_release +wildcard 8 -> memory_order_acquire +wildcard 9 -> memory_order_release +wildcard 11 -> memory_order_release +wildcard 13 -> memory_order_acquire +wildcard 14 -> memory_order_acquire +wildcard 15 -> memory_order_acquire +wildcard 16 -> memory_order_relaxed +wildcard 17 -> memory_order_release +wildcard 19 -> memory_order_release + +Result 1: +wildcard 1 -> memory_order_relaxed +wildcard 2 -> memory_order_relaxed +wildcard 3 -> memory_order_acquire +wildcard 4 -> memory_order_acquire +wildcard 5 -> memory_order_relaxed wildcard 6 -> memory_order_acq_rel wildcard 8 -> memory_order_relaxed wildcard 9 -> memory_order_release -- 2.34.1