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.
56 bool writer_lock_acquired;
59 writer_lock_acquired = false;
62 # Since commit_point_set has no ID attached, A -> B means that for any B,
63 # the previous A happens before B.
64 Read_Unlock -> Read_Lock
65 Read_Unlock -> Write_Lock
66 Read_Unlock -> Write_Trylock(HB_Write_Trylock_Succ)
67 Read_Unlock -> Read_Trylock(HB_Read_Trylock_Succ)
69 Write_Unlock -> Write_Lock
70 Write_Unlock -> Write_Trylock(HB_Write_Trylock_Succ)
72 Write_Unlock -> Read_Lock
73 Write_Unlock -> Read_Trylock(HB_Read_Trylock_Succ)
77 static inline int read_can_lock(rwlock_t *lock)
79 return atomic_load_explicit(&lock->lock, memory_order_relaxed) > 0;
82 static inline int write_can_lock(rwlock_t *lock)
84 return atomic_load_explicit(&lock->lock, memory_order_relaxed) == RW_LOCK_BIAS;
92 Read_Lock_Success_1 | Read_Lock_Success_2
99 static inline void read_lock(rwlock_t *rw)
101 int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
104 @Commit_point_define_check: priorvalue > 0
105 @Label:Read_Lock_Success_1
108 while (priorvalue <= 0) {
109 atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
110 while (atomic_load_explicit(&rw->lock, memory_order_relaxed) <= 0) {
113 priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
116 @Commit_point_define_check: priorvalue > 0
117 @Label:Read_Lock_Success_2
126 @Interface: Write_Lock
128 Write_Lock_Success_1 | Write_Lock_Success_2
130 !writer_lock_acquired && reader_lock_cnt == 0
132 writer_lock_acquired = true;
135 static inline void write_lock(rwlock_t *rw)
137 int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
140 @Commit_point_define_check: priorvalue == RW_LOCK_BIAS
141 @Label: Write_Lock_Success_1
144 while (priorvalue != RW_LOCK_BIAS) {
145 atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
146 while (atomic_load_explicit(&rw->lock, memory_order_relaxed) != RW_LOCK_BIAS) {
149 priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
152 @Commit_point_define_check: priorvalue == RW_LOCK_BIAS
153 @Label: Write_Lock_Success_2
161 @Interface: Read_Trylock
163 Read_Trylock_Succ_Point | Read_Trylock_Fail_Point
165 writer_lock_acquired == false
167 HB_Read_Trylock_Succ :: __RET__ == 1
172 __COND_SAT__ ? __RET__ == 1 : __RET__ == 0
175 static inline int read_trylock(rwlock_t *rw)
177 int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
180 @Potential_commit_point_define: true
181 @Label: Potential_Read_Trylock_Point
184 if (priorvalue > 0) {
187 @Commit_point_define: true
188 @Potential_commit_point_label: Potential_Read_Trylock_Point
189 @Label: Read_Trylock_Succ_Point
196 @Commit_point_define: true
197 @Potential_commit_point_label: Potential_Read_Trylock_Point
198 @Label: Read_Trylock_Fail_Point
201 atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
207 @Interface: Write_Trylock
209 Write_Trylock_Succ_Point | Write_Trylock_Fail_Point
211 HB_Write_Trylock_Succ :: __RET__ == 1
214 writer_lock_acquired = true;
217 static inline int write_trylock(rwlock_t *rw)
219 int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
220 //model_print("write_trylock: priorvalue: %d\n", priorvalue);
223 @Potential_commit_point_define: true
224 @Label: Potential_Write_Trylock_Point
227 if (priorvalue == RW_LOCK_BIAS) {
230 @Commit_point_define: true
231 @Potential_commit_point_label: Potential_Write_Trylock_Point
232 @Label: Write_Trylock_Succ_Point
239 @Commit_point_define: true
240 @Potential_commit_point_label: Potential_Write_Trylock_Point
241 @Label: Write_Trylock_Fail_Point
244 atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
250 @Interface: Read_Unlock
251 @Commit_point_set: Read_Unlock_Point
253 reader_lock_cnt > 0 && !writer_lock_acquired
258 static inline void read_unlock(rwlock_t *rw)
260 atomic_fetch_add_explicit(&rw->lock, 1, memory_order_release);
263 @Commit_point_define_check: true
264 @Label: Read_Unlock_Point
271 @Interface: Write_Unlock
272 @Commit_point_set: Write_Unlock_Point
274 reader_lock_cnt == 0 && writer_lock_acquired
276 writer_lock_acquired = false;
279 static inline void write_unlock(rwlock_t *rw)
281 atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_release);
284 @Commit_point_define_check: true
285 @Label: Write_Unlock_Point
293 static void a(void *obj)
296 for(i = 0; i < 2; i++) {
299 //load_32(&shareddata);
300 printf("%d\n", shareddata);
301 read_unlock(&mylock);
304 //store_32(&shareddata,(unsigned int)i);
306 write_unlock(&mylock);
311 static void b(void *obj)
314 for(i = 0; i < 2; i++) {
316 if (read_trylock(&mylock) == 1) {
317 printf("%d\n", shareddata);
318 read_unlock(&mylock);
321 if (write_trylock(&mylock) == 1) {
323 write_unlock(&mylock);
329 int user_main(int argc, char **argv)
337 atomic_init(&mylock.lock, RW_LOCK_BIAS);
339 thrd_create(&t1, (thrd_start_t)&a, NULL);
340 thrd_create(&t2, (thrd_start_t)&b, NULL);