add notes to mcs-lock
authorPeizhao Ou <peizhaoo@uci.edu>
Fri, 16 Jan 2015 18:51:17 +0000 (10:51 -0800)
committerPeizhao Ou <peizhaoo@uci.edu>
Fri, 16 Jan 2015 18:51:17 +0000 (10:51 -0800)
benchmark/mcs-lock/mcs-lock.h
benchmark/mcs-lock/note.txt [new file with mode: 0644]

index d9165d1..46c6530 100644 (file)
@@ -81,6 +81,7 @@ public:
                me->next.store(NULL, std::mo_relaxed );
                me->gate.store(1, std::mo_relaxed );
 
+               /** Run this in the -Y mode to expose the HB bug */
                // publish my node as the new tail :
                mcs_node * pred = m_tail.exchange(me, std::mo_acq_rel);
                /**
diff --git a/benchmark/mcs-lock/note.txt b/benchmark/mcs-lock/note.txt
new file mode 100644 (file)
index 0000000..93a5387
--- /dev/null
@@ -0,0 +1,8 @@
+#1: The bug that we can't expose in mcs-lock is basically because of the
+following:
+
+the release/acquire are essential in building the hb relationship between the
+next field, such that it guarantees that the next lock() can see the update of
+gate by the previous unlock(). If no hb has been established, the lock() can
+never read the updated gate and will try forever until it gets the out-of-memory
+assertion bug. Thus our analysis cannot even have a valid execution to check!