--- /dev/null
+#include <stdio.h>
+#include <threads.h>
+#include <stdatomic.h>
+
+#include <spec_lib.h>
+#include <stdlib.h>
+#include <cdsannotate.h>
+#include <specannotation.h>
+#include <model_memory.h>
+#include "common.h"
+
+#include "librace.h"
+
+
+atomic<bool> flag(false); // Shared variables
+/**
+@Structure_Define:
+@DeclareVar: bool locked;
+@InitVar: locked = false;
+@Happens_Before: Unlock -> Try_Lock(Trylock_Succ)
+*/
+
+/**
+@Method: Try_Lock
+@Commit_Point_Set:
+ Lock_Fail_Point | Lock_Succ_Point
+@HB_Condition:
+ Trylock_Succ :: __RET__
+@ID: DEFAULT
+@PreCondition:
+ (!locked && __RET__) || (locked && !__RET__)
+@SideEffect:
+ if (__RET__) locked = true;
+*/
+bool try_lock() {
+ bool succ = flag.compare_exchange_strong(false,/*@ \label{line:extendedlock_CAS} @*/
+ true, memory_order_acquire,
+ memory_order_relaxed);
+ /**
+ @Commit_Point_Label_Check: succ
+ @Label: Lock_Succ_Point
+ @End
+ */
+ /**
+ @Commit_Point_Label_Check: !succ
+ @Label: Lock_Fail_Point
+ @End
+ */
+ return succ;
+}
+
+/**
+@Method: Lock
+@Commit_Point_Set: Lock_Succ_Point
+@ID: DEFAULT
+@PreCondition: !locked
+@SideEffect: locked = true;
+*/
+void lock() {
+ do {
+ bool succ = try_lock();/*@ \label{line:lockacquirespec} @*/
+ } while (!succ);
+}
+
+/**
+@Method: Unlock
+@Commit_Point_Set: Unlock_Point
+@ID: DEFAULT
+@PreCondition: locked
+@SideEffect: locked = false;
+*/
+void unlock() {
+ flag.store(false, memory_order_release);/*@ \label{line:unlock_store} @*/
+ /**
+ @Commit_Point_Label_Check: true
+ @Label: Unlock_Point
+ */
+}
+
+static void b(void *obj)
+{
+ int i;
+ for(i = 0; i < 2; i++) {
+ if ((i % 2) == 0) {
+ if (read_trylock(&mylock) == 1) {
+ //printf("%d\n", shareddata);
+ read_unlock(&mylock);
+ }
+ } else {
+ if (write_trylock(&mylock) == 1) {
+ //shareddata = 47;
+ write_unlock(&mylock);
+ }
+ }
+ }
+}
+
+int user_main(int argc, char **argv)
+{
+ /**
+ @Begin
+ @Entry_point
+ @End
+ */
+ thrd_t t1, t2;
+ atomic_init(&mylock.lock, RW_LOCK_BIAS);
+
+ thrd_create(&t1, (thrd_start_t)&a, NULL);
+ thrd_create(&t2, (thrd_start_t)&b, NULL);
+
+ thrd_join(t1);
+ thrd_join(t2);
+
+ return 0;
+}