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                 /**********    Detected Correctness (testcase1 with -Y)    **********/
  31                 unsigned turn = atomic_load_explicit(&l->turn, memory_order_acquire);
  32                 /** @OPDefine: turn == ticket */
  33                 if (turn == ticket) { // Now it's my turn
  34                         return;
  35                 } else {
  36                         thrd_yield(); // Added for CDSChecker
  37                 }
  38         }
  39 }
  40
  41 /** @PreCondition: return STATE(lock) == true;
  42 @Transition: STATE(lock) = false; */
  43 void unlock(struct TicketLock *l) {
  44         unsigned turn = atomic_load_explicit(&l->turn, memory_order_relaxed);
  45         /**********    Detected Correctness (testcase1 with -Y)    **********/
  46         atomic_store_explicit(&l->turn, turn + 1, memory_order_release);
  47         /** @OPDefine: true */
  48 }