benchmark/mcs-lock/note.txt

   1 #1: The bug that we can't expose in mcs-lock is basically because of the
   2 following:
   3
   4 the release/acquire are essential in building the hb relationship between the
   5 next field, such that it guarantees that the next lock() can see the update of
   6 gate by the previous unlock(). If no hb has been established, the lock() can
   7 never read the updated gate and will try forever until it gets the out-of-memory
   8 assertion bug. Thus our analysis cannot even have a valid execution to check!