From: Peizhao Ou <peizhaoo@uci.edu>
Date: Fri, 6 Feb 2015 08:27:36 +0000 (-0800)
Subject: add notes
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=36d769fab2d50a8fd20f4007e4626a79c2dabd2e;p=model-checker-benchmarks.git

add notes
---

diff --git a/concurrent-hashmap/note.txt b/concurrent-hashmap/note.txt
new file mode 100644
index 0000000..6b0898d
--- /dev/null
+++ b/concurrent-hashmap/note.txt
@@ -0,0 +1,14 @@
+#Non-SC case:
+If we have two threads, 1 thread has a put(K1, V1), another thread has another
+put(K2, V2) followed by a get(K3), where K1 and K3 have the same hash and k1 and
+k2 are hashed in the same slot, as follows.
+
+Thrd1						Thrd2
+put(k1, v1); // a			put(k2, v2); // b
+							get(k3); // c
+Suppose we have a synchronized before b with the segment lock, so by SC a is
+before b. Since b is sequenced before c, a should be SC before c. However, in c,
+the first time it does not grab the lock, and c could read an old entry (the
+head of the linked list, meaning that it gets a shorter list), and that can be
+an SC violation. The solution is that we use annotations to tell the SC analysis
+when we will ignore the specific actions (FIXME!!)