7 #include <cdsannotate.h>
8 #include <specannotation.h>
9 #include <model_memory.h>
13 #define RW_LOCK_BIAS 0x00100000
14 #define WRITE_LOCK_CMP RW_LOCK_BIAS
20 /** Example implementation of linux rw lock along with 2 thread test
25 1. At most 1 thread can acquire the write lock, and at the same time, no
26 other threads can acquire any lock (including read/write lock).
27 2. At most RW_LOCK_BIAS threads can successfully acquire the read lock.
28 3. A read_unlock release 1 read lock, and a write_unlock release the write
29 lock. They can not release a lock that they don't acquire.
31 4. Read_lock and write_lock can not be grabbed at the same time.
32 5. Happpens-before relationship should be checked and guaranteed, which
33 should be as the following:
34 a. read_unlock hb-> write_lock
35 b. write_unlock hb-> write_lock
36 c. write_unlock hb-> read_lock
40 Interesting point for locks:
41 a. If the users unlock() before any lock(), then the model checker will fail.
42 For this case, we can not say that the data structure is buggy, how can we
43 tell them from a real data structure bug???
44 b. We should specify that for a specific thread, successful locks and
45 unlocks should always come in pairs. We could make this check as an
46 auxiliary check since it is an extra rule for how the interfaces should called.
55 bool writer_lock_acquired;
58 writer_lock_acquired = false;
61 # Since commit_point_set has no ID attached, A -> B means that for any B,
62 # the previous A happens before B.
63 Write_Unlock -> Write_Lock
64 Write_Unlock -> Write_Trylock(HB_Write_Trylock_Succ)
66 Write_Unlock -> Read_Lock
67 Write_Unlock -> Read_Trylock(HB_Read_Trylock_Succ)
71 static inline int read_can_lock(rwlock_t *lock)
73 return atomic_load_explicit(&lock->lock, memory_order_relaxed) > 0;
76 static inline int write_can_lock(rwlock_t *lock)
78 return atomic_load_explicit(&lock->lock, memory_order_relaxed) == RW_LOCK_BIAS;
86 Read_Lock_Success_1 | Read_Lock_Success_2
93 static inline void read_lock(rwlock_t *rw)
95 int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
98 @Commit_point_define_check: priorvalue > 0
99 @Label:Read_Lock_Success_1
102 while (priorvalue <= 0) {
103 atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
104 while (atomic_load_explicit(&rw->lock, memory_order_relaxed) <= 0) {
107 priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
110 @Commit_point_define_check: priorvalue > 0
111 @Label:Read_Lock_Success_2
120 @Interface: Write_Lock
122 Write_Lock_Success_1 | Write_Lock_Success_2
124 !writer_lock_acquired && reader_lock_cnt == 0
126 writer_lock_acquired = true;
129 static inline void write_lock(rwlock_t *rw)
131 int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
134 @Commit_point_define_check: priorvalue == RW_LOCK_BIAS
135 @Label: Write_Lock_Success_1
138 while (priorvalue != RW_LOCK_BIAS) {
139 atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
140 while (atomic_load_explicit(&rw->lock, memory_order_relaxed) != RW_LOCK_BIAS) {
143 priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
146 @Commit_point_define_check: priorvalue == RW_LOCK_BIAS
147 @Label: Write_Lock_Success_2
155 @Interface: Read_Trylock
157 Read_Trylock_Succ_Point | Read_Trylock_Fail_Point
159 writer_lock_acquired == false
161 HB_Read_Trylock_Succ :: __RET__ == 1
166 __COND_SAT__ ? __RET__ == 1 : __RET__ == 0
169 static inline int read_trylock(rwlock_t *rw)
171 int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
174 @Potential_commit_point_define: true
175 @Label: Potential_Read_Trylock_Point
178 if (priorvalue > 0) {
181 @Commit_point_define: true
182 @Potential_commit_point_label: Potential_Read_Trylock_Point
183 @Label: Read_Trylock_Succ_Point
190 @Commit_point_define: true
191 @Potential_commit_point_label: Potential_Read_Trylock_Point
192 @Label: Read_Trylock_Fail_Point
195 atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
201 @Interface: Write_Trylock
203 Write_Trylock_Succ_Point | Write_Trylock_Fail_Point
205 !writer_lock_acquired && reader_lock_cnt == 0
207 HB_Write_Trylock_Succ :: __RET__ == 1
210 writer_lock_acquired = true;
212 __COND_SAT__ ? __RET__ == 1 : __RET__ == 0
215 static inline int write_trylock(rwlock_t *rw)
217 int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
220 @Potential_commit_point_define: true
221 @Label: Potential_Write_Trylock_Point
224 if (priorvalue == RW_LOCK_BIAS) {
227 @Commit_point_define: true
228 @Potential_commit_point_label: Potential_Write_Trylock_Point
229 @Label: Write_Trylock_Succ_Point
236 @Commit_point_define: true
237 @Potential_commit_point_label: Potential_Write_Trylock_Point
238 @Label: Write_Trylock_Fail_Point
241 atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
247 @Interface: Read_Unlock
248 @Commit_point_set: Read_Unlock_Point
250 reader_lock_cnt > 0 && !writer_lock_acquired
255 static inline void read_unlock(rwlock_t *rw)
257 atomic_fetch_add_explicit(&rw->lock, 1, memory_order_release);
260 @Commit_point_define_check: true
261 @Label: Read_Unlock_Point
268 @Interface: Write_Unlock
269 @Commit_point_set: Write_Unlock_Point
271 reader_lock_cnt == 0 && writer_lock_acquired
273 writer_lock_acquired = false;
276 static inline void write_unlock(rwlock_t *rw)
278 atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_release);
281 @Commit_point_define_check: true
282 @Label: Write_Unlock_Point
290 static void a(void *obj)
293 for(i = 0; i < 2; i++) {
296 //load_32(&shareddata);
297 printf("%d\n", shareddata);
298 read_unlock(&mylock);
301 //store_32(&shareddata,(unsigned int)i);
303 write_unlock(&mylock);
308 static void b(void *obj)
311 for(i = 0; i < 2; i++) {
313 if (read_trylock(&mylock) == 1) {
314 printf("%d\n", shareddata);
315 read_unlock(&mylock);
318 if (write_trylock(&mylock) == 1) {
320 write_unlock(&mylock);
326 int user_main(int argc, char **argv)
334 atomic_init(&mylock.lock, RW_LOCK_BIAS);
336 thrd_create(&t1, (thrd_start_t)&a, NULL);
337 thrd_create(&t2, (thrd_start_t)&b, NULL);