add notes to mcs-lock

diff --git a/benchmark/mcs-lock/mcs-lock.h b/benchmark/mcs-lock/mcs-lock.h
index d9165d124a5a517ce3d38570d7c3bac387e65df8..46c65305bd7ea98038dee2460a137012322728b6 100644 (file)
--- a/benchmark/mcs-lock/mcs-lock.h
+++ b/benchmark/mcs-lock/mcs-lock.h
@@ -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
+++ b/benchmark/mcs-lock/note.txt
@@ -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!