7 #include <cdsannotate.h>
8 #include <specannotation.h>
9 #include <model_memory.h>
14 #define RW_LOCK_BIAS 0x00100000
15 #define WRITE_LOCK_CMP RW_LOCK_BIAS
21 /** Example implementation of linux rw lock along with 2 thread test
26 1. At most 1 thread can acquire the write lock, and at the same time, no
27 other threads can acquire any lock (including read/write lock).
28 2. At most RW_LOCK_BIAS threads can successfully acquire the read lock.
29 3. A read_unlock release 1 read lock, and a write_unlock release the write
30 lock. They can not release a lock that they don't acquire.
32 4. Read_lock and write_lock can not be grabbed at the same time.
33 5. Happpens-before relationship should be checked and guaranteed, which
34 should be as the following:
35 a. read_unlock hb-> write_lock
36 b. write_unlock hb-> write_lock
37 c. write_unlock hb-> read_lock
41 Interesting point for locks:
42 a. If the users unlock() before any lock(), then the model checker will fail.
43 For this case, we can not say that the data structure is buggy, how can we
44 tell them from a real data structure bug???
45 b. We should specify that for a specific thread, successful locks and
46 unlocks should always come in pairs. We could make this check as an
47 auxiliary check since it is an extra rule for how the interfaces should called.
51 bool writer_lock_acquired;
53 @Initial: writer_lock_acquired = false;
55 @Commutativity: Read_Lock <-> Read_Lock: true
56 @Commutativity: Read_Lock <-> Read_Unlock: true
57 @Commutativity: Read_Lock <-> Read_Trylock: true
58 @Commutativity: Read_Lock <-> Write_Trylock: !_Method2.__RET__
60 @Commutativity: Read_Unlock <-> Read_Unlock: true
61 @Commutativity: Read_Unlock <-> Read_Trylock: true
62 @Commutativity: Read_Unlock <-> Write_Trylock: !_Method2.__RET__
64 @Commutativity: Read_Trylock <-> Read_Trylock: true
65 @Commutativity: Read_Trylock <-> Write_Trylock: !_Method1.__RET__ || !_Method2.__RET__
66 @Commutativity: Read_Trylock <-> Write_Lock: !_Method1.__RET__
67 @Commutativity: Read_Trylock <-> Write_Unlock: !_Method1.__RET__
69 @Commutativity: Write_Trylock <-> Write_Trylock: !_Method1.__RET__ || !_Method2.__RET__
70 @Commutativity: Write_Trylock <-> Write_Unlock: !_Method1.__RET__
71 @Commutativity: Write_Trylock <-> Write_Lock: !_Method1.__RET__
74 static inline int read_can_lock(rwlock_t *lock)
76 return atomic_load_explicit(&lock->lock, memory_order_relaxed) > 0;
79 static inline int write_can_lock(rwlock_t *lock)
81 return atomic_load_explicit(&lock->lock, memory_order_relaxed) == RW_LOCK_BIAS;
88 @Commit_point_set: Read_Lock_Success_1 | Read_Lock_Success_2
89 @Check: !writer_lock_acquired
90 @Action: reader_lock_cnt++;
93 static inline void read_lock(rwlock_t *rw)
96 /********** Admissibility **********/
97 int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
100 @Commit_point_define_check: priorvalue > 0
101 @Label:Read_Lock_Success_1
104 while (priorvalue <= 0) {
105 atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
106 while (atomic_load_explicit(&rw->lock, memory_order_relaxed) <= 0) {
109 /********** Admissibility **********/
110 priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
113 @Commit_point_define_check: priorvalue > 0
114 @Label:Read_Lock_Success_2
123 @Interface: Write_Lock
124 @Commit_point_set: Write_Lock_Success_1 | Write_Lock_Success_2
125 @Check: !writer_lock_acquired && reader_lock_cnt == 0
126 @Action: writer_lock_acquired = true;
129 static inline void write_lock(rwlock_t *rw)
131 /********** Admissibility **********/
132 int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
135 @Commit_point_define_check: priorvalue == RW_LOCK_BIAS
136 @Label: Write_Lock_Success_1
139 while (priorvalue != RW_LOCK_BIAS) {
140 atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
141 while (atomic_load_explicit(&rw->lock, memory_order_relaxed) != RW_LOCK_BIAS) {
144 /********** Admissibility **********/
145 priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
148 @Commit_point_define_check: priorvalue == RW_LOCK_BIAS
149 @Label: Write_Lock_Success_2
157 @Interface: Read_Trylock
158 @Commit_point_set: Read_Trylock_Succ_Point | Read_Trylock_Fail_Point
159 //@Condition: writer_lock_acquired == false
160 @HB_condition: HB_Read_Trylock_Succ :: __RET__ == 1
164 @Post_check: __RET__ == !writer_lock_acquired || !__RET__
167 static inline int read_trylock(rwlock_t *rw)
169 /********** Admissibility **********/
170 int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
173 @Potential_commit_point_define: true
174 @Label: Potential_Read_Trylock_Point
177 if (priorvalue > 0) {
180 @Commit_point_define: true
181 @Potential_commit_point_label: Potential_Read_Trylock_Point
182 @Label: Read_Trylock_Succ_Point
189 @Commit_point_define: true
190 @Potential_commit_point_label: Potential_Read_Trylock_Point
191 @Label: Read_Trylock_Fail_Point
194 atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
200 @Interface: Write_Trylock
201 @Commit_point_set: Write_Trylock_Succ_Point | Write_Trylock_Fail_Point
202 @HB_condition: HB_Write_Trylock_Succ :: __RET__ == 1
205 writer_lock_acquired = true;
208 static inline int write_trylock(rwlock_t *rw)
210 /********** Admissibility **********/
211 int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
212 //model_print("write_trylock: priorvalue: %d\n", priorvalue);
215 @Potential_commit_point_define: true
216 @Label: Potential_Write_Trylock_Point
219 if (priorvalue == RW_LOCK_BIAS) {
222 @Commit_point_define: true
223 @Potential_commit_point_label: Potential_Write_Trylock_Point
224 @Label: Write_Trylock_Succ_Point
231 @Commit_point_define: true
232 @Potential_commit_point_label: Potential_Write_Trylock_Point
233 @Label: Write_Trylock_Fail_Point
236 atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
242 @Interface: Read_Unlock
243 @Commit_point_set: Read_Unlock_Point
244 @Check: reader_lock_cnt > 0 && !writer_lock_acquired
245 @Action: reader_lock_cnt--;
248 static inline void read_unlock(rwlock_t *rw)
250 /********** Admissibility **********/
251 atomic_fetch_add_explicit(&rw->lock, 1, memory_order_release);
254 @Commit_point_define_check: true
255 @Label: Read_Unlock_Point
262 @Interface: Write_Unlock
263 @Commit_point_set: Write_Unlock_Point | Write_Unlock_Clear
264 @Check: reader_lock_cnt == 0 && writer_lock_acquired
265 @Action: writer_lock_acquired = false;
268 static inline void write_unlock(rwlock_t *rw)
270 /********** Admissibility **********/
271 atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_release);
274 @Commit_point_define_check: true
275 @Label: Write_Unlock_Point
281 @Commit_point_clear: true
282 @Label: Write_Unlock_Clear
290 static void a(void *obj)
293 //load_32(&shareddata);
294 //printf("%d\n", shareddata);
295 read_unlock(&mylock);
298 //store_32(&shareddata,(unsigned int)i);
300 write_unlock(&mylock);
303 static void b(void *obj)
305 if (read_trylock(&mylock) == 1) {
306 //printf("%d\n", shareddata);
307 read_unlock(&mylock);
310 if (write_trylock(&mylock) == 1) {
312 write_unlock(&mylock);
316 int user_main(int argc, char **argv)
324 atomic_init(&mylock.lock, RW_LOCK_BIAS);
326 thrd_create(&t1, (thrd_start_t)&a, NULL);
327 thrd_create(&t2, (thrd_start_t)&b, NULL);