The CDSSpec checker's benchmarks
[model-checker-benchmarks.git] / 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 }