X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker-benchmarks.git;a=blobdiff_plain;f=concurrent-hashmap%2Fnote.txt;fp=concurrent-hashmap%2Fnote.txt;h=0056dcdc89fe1d2f1b9ef8907fd46957fc2d26dd;hp=0000000000000000000000000000000000000000;hb=3cb559e8fea6c3839ed20d6a10a636d728cf8695;hpb=c046bae812a0dd4d54be2236487c112d36641538

diff --git a/concurrent-hashmap/note.txt b/concurrent-hashmap/note.txt
new file mode 100644
index 0000000..0056dcd
--- /dev/null
+++ b/concurrent-hashmap/note.txt
@@ -0,0 +1,10 @@
+#Non-SC:
+The following case can be non-SC.
+
+Thrd1						Thrd2
+put(k1, v1); // a			put(k2, v2); // c
+get(k2); // b				get(k1); // d
+
+When b and d both read the old head of the list (and they later grab the lock,
+making it the interface SC), it's non-SC because neither reads the updated
+value.