#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!