model: bug fixes to new code
[model-checker.git] / test / linuxrwlocks.c
1 #include <stdio.h>
2
3 #include "libthreads.h"
4 #include "librace.h"
5 #include "stdatomic.h"
6
7
8 #define RW_LOCK_BIAS            0x00100000
9 #define WRITE_LOCK_CMP          RW_LOCK_BIAS
10
11 /** Example implementation of linux rw lock along with 2 thread test
12  *  driver... */
13
14
15 typedef union {
16         atomic_int lock;
17 } rwlock_t;
18
19 static inline int read_can_lock(rwlock_t *lock)
20 {
21         return atomic_load_explicit(&lock->lock, memory_order_relaxed) > 0;
22 }
23
24 static inline int write_can_lock(rwlock_t *lock)
25 {
26         return atomic_load_explicit(&lock->lock, memory_order_relaxed) == RW_LOCK_BIAS;
27 }
28
29 static inline void read_lock(rwlock_t *rw)
30 {
31         int currentvalue=atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
32         while (currentvalue<0) {
33                 atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
34                 do {
35                         currentvalue=atomic_load_explicit(&rw->lock, memory_order_relaxed);
36                 }       while(currentvalue<=0);
37                 currentvalue=atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
38         }
39 }
40
41 static inline void write_lock(rwlock_t *rw)
42 {
43         int currentvalue=atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
44         while (currentvalue!=0) {
45                 atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
46                 do {
47                         currentvalue=atomic_load_explicit(&rw->lock, memory_order_relaxed);
48                 }       while(currentvalue!=RW_LOCK_BIAS);
49                 currentvalue=atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
50         }
51 }
52
53 static inline int read_trylock(rwlock_t *rw)
54 {
55         int currentvalue=atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
56         if (currentvalue>=0)
57                 return 1;
58         
59         atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
60         return 0;
61 }
62
63 static inline int write_trylock(rwlock_t *rw)
64 {
65         int currentvalue=atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
66         if (currentvalue>=0)
67                 return 1;
68         
69         atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
70         return 0;
71 }
72
73 static inline void read_unlock(rwlock_t *rw)
74 {
75         atomic_fetch_add_explicit(&rw->lock, 1, memory_order_release);
76 }
77
78 static inline void write_unlock(rwlock_t *rw)
79 {
80         atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_release);
81 }
82
83 rwlock_t mylock;
84 int shareddata;
85
86 static void a(void *obj)
87 {
88         int i;
89         for(i=0;i<2;i++) {
90                 if ((i%2)==0) {
91                         read_lock(&mylock);
92                         load_32(&shareddata);
93                         read_unlock(&mylock);
94                 } else {
95                         write_lock(&mylock);
96                         store_32(&shareddata,(unsigned int)i);
97                         write_unlock(&mylock);
98                 }
99         }
100 }
101
102 void user_main()
103 {
104         thrd_t t1, t2;
105         atomic_init(&mylock.lock, RW_LOCK_BIAS);
106
107         thrd_create(&t1, (thrd_start_t)&a, NULL);
108         thrd_create(&t2, (thrd_start_t)&a, NULL);
109         
110         thrd_join(t1);
111         thrd_join(t2);
112 }