fixed command line

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

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