mcs-lock/note.txt

   1 When lock() publishes the 'me' to the previous lock-holder
   2         // prev->next.store(me, std::mo_release);
   3 , it must synchronize with the unlock()'s
   4         // me->next.load(std::mo_acquire);
   5 because otherwise when it's the lock()'s turn to lock, it is allowed to always
   6 read 1 in
   7         // me->gate.load(std::mo_acquire)
   8 such that it will end up with an infinite loop.
   9
  10 To make this happen, we establish synchronization between the initialization of
  11 the gate and the later update of gate. From the inference analysis, we actually
  12 got two results, where wildcard(7) and wildcard(8) only need one acquire. That's
  13 actually the place to synchronize the update of gate. We can achieve it at the
  14 Tail or at the next field.
  15
  16 To generate those results, we actually need to pass a specific option to the
  17 scfence analysis, as follows.
  18
  19 *******************************************************
  20 peizhaoo@dw-2:~/model-checker$ ./run.sh mcs-lock/testcase1 -m2 -b100 -y -tSCFENCE -o m
  21 *******************************************************
  22
  23 The '-b100' is to terminate the execution in case of infinite loops because of
  24 improper synchronization at the beginning period. The 'm' option for SCFENCE
  25 analysis is to turn on the implyMO mode.