ms-queue result

diff --git a/ms-queue/Makefile b/ms-queue/Makefile
index 55a4edb65e06876a395593e05d42dcede8bd4190..566aee05af368c0ec31ab138ce2abcfcac68b4b7 100644 (file)
--- 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 eb2b99513de38b680b9f7bb42fb2f19cbb2a80a4..00a645cd1e83f7f5766dbffc6b3cd3e1fd8c7148 100644 (file)
--- 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 f1c01e6c19c72d18a03de11e8874746fc7d52986..95aa6bb0d2b397166dda921639b127de648b5e31 100644 (file)
--- 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 eae4d2bcfda29556f00f302af2493b8a10df3e8e..646ec9730862394e6ec7dc02728cae75fae1a2a9 100644 (file)
--- 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