7 #include <cdsannotate.h>
8 #include <specannotation.h>
9 #include <model_memory.h>
15 atomic<bool> flag(false); // Shared variables
18 @DeclareVar: bool locked;
19 @InitVar: locked = false;
20 @Happens_Before: Unlock -> Try_Lock(Trylock_Succ)
26 Lock_Fail_Point | Lock_Succ_Point
28 Trylock_Succ :: __RET__
31 (!locked && __RET__) || (locked && !__RET__)
33 if (__RET__) locked = true;
36 bool succ = flag.compare_exchange_strong(false,/*@ \label{line:extendedlock_CAS} @*/
37 true, memory_order_acquire,
38 memory_order_relaxed);
40 @Commit_Point_Label_Check: succ
41 @Label: Lock_Succ_Point
45 @Commit_Point_Label_Check: !succ
46 @Label: Lock_Fail_Point
54 @Commit_Point_Set: Lock_Succ_Point
56 @PreCondition: !locked
57 @SideEffect: locked = true;
61 bool succ = try_lock();/*@ \label{line:lockacquirespec} @*/
67 @Commit_Point_Set: Unlock_Point
70 @SideEffect: locked = false;
73 flag.store(false, memory_order_release);/*@ \label{line:unlock_store} @*/
75 @Commit_Point_Label_Check: true
80 static void b(void *obj)
83 for(i = 0; i < 2; i++) {
85 if (read_trylock(&mylock) == 1) {
86 //printf("%d\n", shareddata);
90 if (write_trylock(&mylock) == 1) {
92 write_unlock(&mylock);
98 int user_main(int argc, char **argv)
106 atomic_init(&mylock.lock, RW_LOCK_BIAS);
108 thrd_create(&t1, (thrd_start_t)&a, NULL);
109 thrd_create(&t2, (thrd_start_t)&b, NULL);