changes

diff --git a/barrier/result.txt b/barrier/result.txt
new file mode 100644 (file)
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 8f5a8af5879a0d5ac681081a6fa8251f108ad911..26dcd2df9c6cba778d25ade5c82fcab3f5a5c0a1 100644 (file)
--- 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 a62c7e3de5d75c25a74469ff6b89b3443a6e8925..27838a5dec5d2b4c34f5757018a87c9e59e4eb65 100644 (file)
--- 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 fcaca92f5af7cc94768fb139b1061bc7eb11209a..68ca03a569b9f0caeaafb5784106d2595aaf782e 100644 (file)
--- 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 (file)
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 (file)
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