add trylock

[cdsspec-compiler.git] / benchmark / trylock / trylock.c

diff --git a/benchmark/trylock/trylock.c b/benchmark/trylock/trylock.c
new file mode 100644 (file)
index 0000000..80728f8
--- /dev/null
+++ b/benchmark/trylock/trylock.c
@@ -0,0 +1,115 @@
+#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;
+}