From ebcac5d8b3ac3864cd920623b79f9e3e5f20dada Mon Sep 17 00:00:00 2001
From: Peizhao Ou <peizhaoo@uci.edu>
Date: Fri, 29 Aug 2014 17:16:16 -0700
Subject: [PATCH] add trylock

---
 benchmark/trylock/.gitignore |   1 +
 benchmark/trylock/Makefile   |  11 ++++
 benchmark/trylock/trylock.c  | 115 +++++++++++++++++++++++++++++++++++
 3 files changed, 127 insertions(+)
 create mode 100644 benchmark/trylock/.gitignore
 create mode 100644 benchmark/trylock/Makefile
 create mode 100644 benchmark/trylock/trylock.c

diff --git a/benchmark/trylock/.gitignore b/benchmark/trylock/.gitignore
new file mode 100644
index 0000000..2fdb632
--- /dev/null
+++ b/benchmark/trylock/.gitignore
@@ -0,0 +1 @@
+/linuxrwlocks
diff --git a/benchmark/trylock/Makefile b/benchmark/trylock/Makefile
new file mode 100644
index 0000000..8868ce3
--- /dev/null
+++ b/benchmark/trylock/Makefile
@@ -0,0 +1,11 @@
+include ../benchmarks.mk
+
+TESTNAME = trylock
+
+all: $(TESTNAME)
+
+$(TESTNAME): $(TESTNAME).c
+	$(CC) -o $@ $< $(CFLAGS) $(LDFLAGS)
+
+clean:
+	rm -f $(TESTNAME) *.o
diff --git a/benchmark/trylock/trylock.c b/benchmark/trylock/trylock.c
new file mode 100644
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;
+}
-- 
2.34.1