ticket-lock/lock.c

   1 #include <stdatomic.h>
   2
   3 #include "librace.h"
   4 #include "lock.h"
   5
   6 /**
   7         This ticket lock implementation is derived from the original Mellor-Crummey
   8         & Scott paper <Algorithms for Scalable Synchronization on
   9                 SharedMemory Multiprocessors> in 1991.
  10         It assumes that the ticket and turn counter are large enough to accommodate
  11         the maximum number of simultaneous requests for the lock.
  12 */
  13
  14 /** @DeclareState: bool lock; */
  15
  16
  17 void initTicketLock(TicketLock *l) {
  18         atomic_init(&l->ticket, 0);
  19         atomic_init(&l->turn, 0);
  20 }
  21
  22 /** @PreCondition: return STATE(lock) == false;
  23 @Transition: STATE(lock) = true; */
  24 void lock(struct TicketLock *l) {
  25         // First grab a ticket
  26         unsigned ticket = atomic_fetch_add_explicit(&l->ticket, 1,
  27                 memory_order_relaxed);
  28         // Spinning for my turn
  29         while (true) {
  30         // XXX-injection-#1: Weaken the parameter "memory_order_acquire" to
  31         // "memory_order_relaxed", run "make" to recompile, and then run:
  32         // "./run.sh ./ticket-lock/testcase1 -m2 -Y -u3 -tSPEC"
  33                 /**********    Detected Correctness (testcase1 with -Y)    **********/
  34                 unsigned turn = atomic_load_explicit(&l->turn, memory_order_acquire);
  35                 /** @OPDefine: turn == ticket */
  36                 if (turn == ticket) { // Now it's my turn
  37                         return;
  38                 } else {
  39                         thrd_yield(); // Added for CDSChecker
  40                 }
  41         }
  42 }
  43
  44 /** @PreCondition: return STATE(lock) == true;
  45 @Transition: STATE(lock) = false; */
  46 void unlock(struct TicketLock *l) {
  47         unsigned turn = atomic_load_explicit(&l->turn, memory_order_relaxed);
  48     // XXX-injection-#2: Weaken the parameter "memory_order_release" to
  49     // "memory_order_relaxed", run "make" to recompile, and then run:
  50     // "./run.sh ./ticket-lock/testcase1 -m2 -Y -u3 -tSPEC"
  51         /**********    Detected Correctness (testcase1 with -Y)    **********/
  52         atomic_store_explicit(&l->turn, turn + 1, memory_order_release);
  53         /** @OPDefine: true */
  54 }