From: Peizhao Ou <peizhaoo@uci.edu>
Date: Tue, 17 Nov 2015 22:14:34 +0000 (-0800)
Subject: edits
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=23fa78968c89a4c4b943c18c86619177f9e3570d;p=cdsspec-compiler.git

edits
---

diff --git a/benchmark/linuxrwlocks/Makefile b/benchmark/linuxrwlocks/Makefile
index 90dafcf..c62b36a 100644
--- a/benchmark/linuxrwlocks/Makefile
+++ b/benchmark/linuxrwlocks/Makefile
@@ -1,10 +1,10 @@
 include ../benchmarks.mk
 
-TESTNAME = linuxrwlocks
+TESTNAME = linuxrwlocks testcase1 testcase2
 
 all: $(TESTNAME)
 
-$(TESTNAME): $(TESTNAME).c
+$(TESTNAME): % : %.c
 	$(CC) -o $@ $< $(CFLAGS) $(LDFLAGS)
 
 clean:
diff --git a/benchmark/linuxrwlocks/linuxrwlocks.c b/benchmark/linuxrwlocks/linuxrwlocks.c
index b97c45b..1f7059f 100644
--- a/benchmark/linuxrwlocks/linuxrwlocks.c
+++ b/benchmark/linuxrwlocks/linuxrwlocks.c
@@ -61,16 +61,34 @@ typedef union {
 	@Happens_before:
 		# Since commit_point_set has no ID attached, A -> B means that for any B,
 		# the previous A happens before B.
-		Read_Unlock -> Read_Lock
+		#Read_Unlock -> Read_Lock
 		Read_Unlock -> Write_Lock
 		Read_Unlock -> Write_Trylock(HB_Write_Trylock_Succ)
-		Read_Unlock -> Read_Trylock(HB_Read_Trylock_Succ)
+		#Read_Unlock -> Read_Trylock(HB_Read_Trylock_Succ)
 
 		Write_Unlock -> Write_Lock
 		Write_Unlock -> Write_Trylock(HB_Write_Trylock_Succ)
 
 		Write_Unlock -> Read_Lock
 		Write_Unlock -> Read_Trylock(HB_Read_Trylock_Succ)
+	
+	@Commutativity: Read_Lock <-> Read_Lock: true
+	@Commutativity: Read_Lock <-> Read_Unlock: true
+	@Commutativity: Read_Lock <-> Read_Trylock: true
+	@Commutativity: Read_Lock <-> Write_Trylock: !_Method2.__RET__
+	
+	@Commutativity: Read_Unlock <-> Read_Unlock: true
+	@Commutativity: Read_Unlock <-> Read_Trylock: true
+	@Commutativity: Read_Unlock <-> Write_Trylock: !_Method2.__RET__
+
+	@Commutativity: Read_Trylock <-> Read_Trylock: true
+	@Commutativity: Read_Trylock <-> Write_Trylock: !_Method1.__RET__ || !_Method2.__RET__
+	@Commutativity: Read_Trylock <-> Write_Lock: !_Method1.__RET__
+	@Commutativity: Read_Trylock <-> Write_Unlock: !_Method1.__RET__
+
+	@Commutativity: Write_Trylock <-> Write_Trylock: !_Method1.__RET__ || !_Method2.__RET__
+	@Commutativity: Write_Trylock <-> Write_Unlock: !_Method1.__RET__
+	@Commutativity: Write_Trylock <-> Write_Lock: !_Method1.__RET__
 	@End
 */
 
@@ -95,6 +113,8 @@ static inline int write_can_lock(rwlock_t *lock)
 */
 static inline void read_lock(rwlock_t *rw)
 {
+	
+	/**********  Admissibility  **********/
 	int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
 	/**
 		@Begin
@@ -107,6 +127,7 @@ static inline void read_lock(rwlock_t *rw)
 		while (atomic_load_explicit(&rw->lock, memory_order_relaxed) <= 0) {
 			thrd_yield();
 		}
+		/**********  Admissibility  **********/
 		priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
 		/**
 			@Begin
@@ -128,6 +149,7 @@ static inline void read_lock(rwlock_t *rw)
 */
 static inline void write_lock(rwlock_t *rw)
 {
+	/**********  Admissibility  **********/
 	int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
 	/**
 		@Begin
@@ -140,6 +162,7 @@ static inline void write_lock(rwlock_t *rw)
 		while (atomic_load_explicit(&rw->lock, memory_order_relaxed) != RW_LOCK_BIAS) {
 			thrd_yield();
 		}
+		/**********  Admissibility  **********/
 		priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
 		/**
 			@Begin
@@ -157,13 +180,14 @@ static inline void write_lock(rwlock_t *rw)
 	//@Condition: writer_lock_acquired == false
 	@HB_condition: HB_Read_Trylock_Succ :: __RET__ == 1
 	@Action:
-		if (__COND_SAT__)
+		if (__RET__)
 			reader_lock_cnt++;
-	@Post_check: __COND_SAT__ ? __RET__ == 1 : __RET__ == 0
+	@Post_check: __RET__ == !writer_lock_acquired || !__RET__
 	@End
 */
 static inline int read_trylock(rwlock_t *rw)
 {
+	/**********  Admissibility  **********/
 	int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
 	/**
 		@Begin
@@ -204,6 +228,7 @@ static inline int read_trylock(rwlock_t *rw)
 */
 static inline int write_trylock(rwlock_t *rw)
 {
+	/**********  Admissibility  **********/
 	int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
 	//model_print("write_trylock: priorvalue: %d\n", priorvalue);
 	/**
@@ -243,6 +268,7 @@ static inline int write_trylock(rwlock_t *rw)
 */
 static inline void read_unlock(rwlock_t *rw)
 {
+	/**********  Admissibility  **********/
 	atomic_fetch_add_explicit(&rw->lock, 1, memory_order_release);
 	/**
 		@Begin
@@ -262,6 +288,7 @@ static inline void read_unlock(rwlock_t *rw)
 */
 static inline void write_unlock(rwlock_t *rw)
 {
+	/**********  Admissibility  **********/
 	atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_release);
 	/**
 		@Begin
@@ -283,37 +310,27 @@ int shareddata;
 
 static void a(void *obj)
 {
-	int i;
-	for(i = 0; i < 2; i++) {
-		if ((i % 2) == 0) {
-			read_lock(&mylock);
-			//load_32(&shareddata);
-			//printf("%d\n", shareddata);
-			read_unlock(&mylock);
-		} else {
-			write_lock(&mylock);
-			//store_32(&shareddata,(unsigned int)i);
-			shareddata = 47;
-			write_unlock(&mylock);
-		}
-	}
+	read_lock(&mylock);
+	//load_32(&shareddata);
+	//printf("%d\n", shareddata);
+	read_unlock(&mylock);
+	
+	write_lock(&mylock);
+	//store_32(&shareddata,(unsigned int)i);
+	shareddata = 47;
+	write_unlock(&mylock);
 }
 
 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);
-			}
-		}
+	if (read_trylock(&mylock) == 1) {
+		//printf("%d\n", shareddata);
+		read_unlock(&mylock);
+	}
+	
+	if (write_trylock(&mylock) == 1) {
+		//shareddata = 47;
+		write_unlock(&mylock);
 	}
 }
 
diff --git a/benchmark/linuxrwlocks/testcase1.c b/benchmark/linuxrwlocks/testcase1.c
new file mode 100644
index 0000000..9faad2a
--- /dev/null
+++ b/benchmark/linuxrwlocks/testcase1.c
@@ -0,0 +1,338 @@
+#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"
+
+#define RW_LOCK_BIAS            0x00100000
+#define WRITE_LOCK_CMP          RW_LOCK_BIAS
+
+typedef union {
+	atomic_int lock;
+} rwlock_t;
+
+/** Example implementation of linux rw lock along with 2 thread test
+ *  driver... */
+
+/**
+	Properties to check:
+	1. At most 1 thread can acquire the write lock, and at the same time, no
+		other threads can acquire any lock (including read/write lock).
+	2. At most RW_LOCK_BIAS threads can successfully acquire the read lock.
+	3. A read_unlock release 1 read lock, and a write_unlock release the write
+	lock. They can not release a lock that they don't acquire.
+	###
+	4. Read_lock and write_lock can not be grabbed at the same time.
+	5. Happpens-before relationship should be checked and guaranteed, which
+	should be as the following:
+		a. read_unlock hb-> write_lock
+		b. write_unlock hb-> write_lock
+		c. write_unlock hb-> read_lock
+*/
+
+/**
+	Interesting point for locks:
+	a. If the users unlock() before any lock(), then the model checker will fail.
+	For this case, we can not say that the data structure is buggy, how can we
+	tell them from a real data structure bug???
+	b. We should specify that for a specific thread, successful locks and
+	unlocks should always come in pairs. We could make this check as an
+	auxiliary check since it is an extra rule for how the interfaces should called.
+*/
+
+/**
+	@Begin
+	@Options:
+		LANG = C;
+	@Global_define:
+		@DeclareVar:
+			bool writer_lock_acquired;
+			int reader_lock_cnt;
+		@InitVar:
+			writer_lock_acquired = false;
+			reader_lock_cnt = 0;
+	@Happens_before:
+		# Since commit_point_set has no ID attached, A -> B means that for any B,
+		# the previous A happens before B.
+		#Read_Unlock -> Read_Lock
+		Read_Unlock -> Write_Lock
+		Read_Unlock -> Write_Trylock(HB_Write_Trylock_Succ)
+		#Read_Unlock -> Read_Trylock(HB_Read_Trylock_Succ)
+
+		Write_Unlock -> Write_Lock
+		Write_Unlock -> Write_Trylock(HB_Write_Trylock_Succ)
+
+		Write_Unlock -> Read_Lock
+		Write_Unlock -> Read_Trylock(HB_Read_Trylock_Succ)
+	
+	@Commutativity: Read_Lock <-> Read_Lock: true
+	@Commutativity: Read_Lock <-> Read_Unlock: true
+	@Commutativity: Read_Lock <-> Read_Trylock: true
+	@Commutativity: Read_Lock <-> Write_Trylock: !_Method2.__RET__
+	
+	@Commutativity: Read_Unlock <-> Read_Unlock: true
+	@Commutativity: Read_Unlock <-> Read_Trylock: true
+	@Commutativity: Read_Unlock <-> Write_Trylock: !_Method2.__RET__
+
+	@Commutativity: Read_Trylock <-> Read_Trylock: true
+	@Commutativity: Read_Trylock <-> Write_Trylock: !_Method1.__RET__ || !_Method2.__RET__
+	@Commutativity: Read_Trylock <-> Write_Lock: !_Method1.__RET__
+	@Commutativity: Read_Trylock <-> Write_Unlock: !_Method1.__RET__
+
+	@Commutativity: Write_Trylock <-> Write_Trylock: !_Method1.__RET__ || !_Method2.__RET__
+	@Commutativity: Write_Trylock <-> Write_Unlock: !_Method1.__RET__
+	@Commutativity: Write_Trylock <-> Write_Lock: !_Method1.__RET__
+	@End
+*/
+
+static inline int read_can_lock(rwlock_t *lock)
+{
+	return atomic_load_explicit(&lock->lock, memory_order_relaxed) > 0;
+}
+
+static inline int write_can_lock(rwlock_t *lock)
+{
+	return atomic_load_explicit(&lock->lock, memory_order_relaxed) == RW_LOCK_BIAS;
+}
+
+
+/**
+	@Begin
+	@Interface: Read_Lock
+	@Commit_point_set: Read_Lock_Success_1 | Read_Lock_Success_2
+	@Check: !writer_lock_acquired
+	@Action: reader_lock_cnt++;
+	@End
+*/
+static inline void read_lock(rwlock_t *rw)
+{
+	int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
+	/**
+		@Begin
+		@Commit_point_define_check: priorvalue > 0
+		@Label:Read_Lock_Success_1
+		@End
+	*/
+	while (priorvalue <= 0) {
+		atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
+		while (atomic_load_explicit(&rw->lock, memory_order_relaxed) <= 0) {
+			thrd_yield();
+		}
+		priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
+		/**
+			@Begin
+			@Commit_point_define_check: priorvalue > 0
+			@Label:Read_Lock_Success_2
+			@End
+		*/
+	}
+}
+
+
+/**
+	@Begin
+	@Interface: Write_Lock
+	@Commit_point_set: Write_Lock_Success_1 | Write_Lock_Success_2
+	@Check: !writer_lock_acquired && reader_lock_cnt == 0
+	@Action: writer_lock_acquired = true;
+	@End
+*/
+static inline void write_lock(rwlock_t *rw)
+{
+	int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
+	/**
+		@Begin
+		@Commit_point_define_check: priorvalue == RW_LOCK_BIAS
+		@Label: Write_Lock_Success_1
+		@End
+	*/
+	while (priorvalue != RW_LOCK_BIAS) {
+		atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
+		while (atomic_load_explicit(&rw->lock, memory_order_relaxed) != RW_LOCK_BIAS) {
+			thrd_yield();
+		}
+		priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
+		/**
+			@Begin
+			@Commit_point_define_check: priorvalue == RW_LOCK_BIAS
+			@Label: Write_Lock_Success_2
+			@End
+		*/
+	}
+}
+
+/**
+	@Begin
+	@Interface: Read_Trylock
+	@Commit_point_set: Read_Trylock_Succ_Point | Read_Trylock_Fail_Point
+	//@Condition: writer_lock_acquired == false
+	@HB_condition: HB_Read_Trylock_Succ :: __RET__ == 1
+	@Action:
+		if (__RET__)
+			reader_lock_cnt++;
+	@Post_check: __RET__ == !writer_lock_acquired || !__RET__
+	@End
+*/
+static inline int read_trylock(rwlock_t *rw)
+{
+	int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
+	/**
+		@Begin
+		@Potential_commit_point_define: true
+		@Label: Potential_Read_Trylock_Point
+		@End
+	*/
+	if (priorvalue > 0) {
+		/**
+			@Begin
+			@Commit_point_define: true
+			@Potential_commit_point_label: Potential_Read_Trylock_Point
+			@Label:  Read_Trylock_Succ_Point
+			@End
+		*/
+		return 1;
+	}
+	/**
+		@Begin
+		@Commit_point_define: true
+		@Potential_commit_point_label: Potential_Read_Trylock_Point
+		@Label:  Read_Trylock_Fail_Point
+		@End
+	*/
+	atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
+	return 0;
+}
+
+/**
+	@Begin
+	@Interface: Write_Trylock
+	@Commit_point_set: Write_Trylock_Succ_Point | Write_Trylock_Fail_Point
+	@HB_condition: HB_Write_Trylock_Succ :: __RET__ == 1
+	@Action:
+		if (__RET__ == 1)
+			writer_lock_acquired = true;
+	@End
+*/
+static inline int write_trylock(rwlock_t *rw)
+{
+	int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
+	//model_print("write_trylock: priorvalue: %d\n", priorvalue);
+	/**
+		@Begin
+		@Potential_commit_point_define: true
+		@Label: Potential_Write_Trylock_Point
+		@End
+	*/
+	if (priorvalue == RW_LOCK_BIAS) {
+		/**
+			@Begin
+			@Commit_point_define: true
+			@Potential_commit_point_label: Potential_Write_Trylock_Point
+			@Label: Write_Trylock_Succ_Point
+			@End
+		*/
+		return 1;
+	}
+	/**
+		@Begin
+		@Commit_point_define: true
+		@Potential_commit_point_label: Potential_Write_Trylock_Point
+		@Label: Write_Trylock_Fail_Point
+		@End
+	*/
+	atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
+	return 0;
+}
+
+/**
+	@Begin
+	@Interface: Read_Unlock
+	@Commit_point_set: Read_Unlock_Point
+	@Check: reader_lock_cnt > 0 && !writer_lock_acquired
+	@Action: reader_lock_cnt--;
+	@End
+*/
+static inline void read_unlock(rwlock_t *rw)
+{
+	/**********  Admissibility  **********/
+	atomic_fetch_add_explicit(&rw->lock, 1, memory_order_release);
+	/**
+		@Begin
+		@Commit_point_define_check: true
+		@Label: Read_Unlock_Point
+		@End
+	*/
+}
+
+/**
+	@Begin
+	@Interface: Write_Unlock
+	@Commit_point_set: Write_Unlock_Point | Write_Unlock_Clear
+	@Check: reader_lock_cnt == 0 && writer_lock_acquired
+	@Action: writer_lock_acquired = false;
+	@End
+*/
+static inline void write_unlock(rwlock_t *rw)
+{
+	/**********  Admissibility  **********/
+	atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_release);
+	/**
+		@Begin
+		@Commit_point_define_check: true
+		@Label: Write_Unlock_Point
+		@End
+	*/
+
+	/**
+		//@Begin
+		@Commit_point_clear: true
+		@Label: Write_Unlock_Clear
+		@End
+	*/
+}
+
+rwlock_t mylock;
+int shareddata;
+
+static void a(void *obj)
+{
+	write_lock(&mylock);
+	//store_32(&shareddata,(unsigned int)i);
+	shareddata = 47;
+	write_unlock(&mylock);
+}
+
+static void b(void *obj)
+{
+	if (read_trylock(&mylock)) {
+		//load_32(&shareddata);
+		//printf("%d\n", shareddata);
+		read_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;
+}
diff --git a/benchmark/linuxrwlocks/testcase2.c b/benchmark/linuxrwlocks/testcase2.c
new file mode 100644
index 0000000..f5f0820
--- /dev/null
+++ b/benchmark/linuxrwlocks/testcase2.c
@@ -0,0 +1,343 @@
+#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"
+
+#define RW_LOCK_BIAS            0x00100000
+#define WRITE_LOCK_CMP          RW_LOCK_BIAS
+
+typedef union {
+	atomic_int lock;
+} rwlock_t;
+
+/** Example implementation of linux rw lock along with 2 thread test
+ *  driver... */
+
+/**
+	Properties to check:
+	1. At most 1 thread can acquire the write lock, and at the same time, no
+		other threads can acquire any lock (including read/write lock).
+	2. At most RW_LOCK_BIAS threads can successfully acquire the read lock.
+	3. A read_unlock release 1 read lock, and a write_unlock release the write
+	lock. They can not release a lock that they don't acquire.
+	###
+	4. Read_lock and write_lock can not be grabbed at the same time.
+	5. Happpens-before relationship should be checked and guaranteed, which
+	should be as the following:
+		a. read_unlock hb-> write_lock
+		b. write_unlock hb-> write_lock
+		c. write_unlock hb-> read_lock
+*/
+
+/**
+	Interesting point for locks:
+	a. If the users unlock() before any lock(), then the model checker will fail.
+	For this case, we can not say that the data structure is buggy, how can we
+	tell them from a real data structure bug???
+	b. We should specify that for a specific thread, successful locks and
+	unlocks should always come in pairs. We could make this check as an
+	auxiliary check since it is an extra rule for how the interfaces should called.
+*/
+
+/**
+	@Begin
+	@Options:
+		LANG = C;
+	@Global_define:
+		@DeclareVar:
+			bool writer_lock_acquired;
+			int reader_lock_cnt;
+		@InitVar:
+			writer_lock_acquired = false;
+			reader_lock_cnt = 0;
+	@Happens_before:
+		# Since commit_point_set has no ID attached, A -> B means that for any B,
+		# the previous A happens before B.
+		#Read_Unlock -> Read_Lock
+		Read_Unlock -> Write_Lock
+		Read_Unlock -> Write_Trylock(HB_Write_Trylock_Succ)
+		#Read_Unlock -> Read_Trylock(HB_Read_Trylock_Succ)
+
+		Write_Unlock -> Write_Lock
+		Write_Unlock -> Write_Trylock(HB_Write_Trylock_Succ)
+
+		Write_Unlock -> Read_Lock
+		Write_Unlock -> Read_Trylock(HB_Read_Trylock_Succ)
+	
+	@Commutativity: Read_Lock <-> Read_Lock: true
+	@Commutativity: Read_Lock <-> Read_Unlock: true
+	@Commutativity: Read_Lock <-> Read_Trylock: true
+	@Commutativity: Read_Lock <-> Write_Trylock: !_Method2.__RET__
+	
+	@Commutativity: Read_Unlock <-> Read_Unlock: true
+	@Commutativity: Read_Unlock <-> Read_Trylock: true
+	@Commutativity: Read_Unlock <-> Write_Trylock: !_Method2.__RET__
+
+	@Commutativity: Read_Trylock <-> Read_Trylock: true
+	@Commutativity: Read_Trylock <-> Write_Trylock: !_Method1.__RET__ || !_Method2.__RET__
+	@Commutativity: Read_Trylock <-> Write_Lock: !_Method1.__RET__
+	@Commutativity: Read_Trylock <-> Write_Unlock: !_Method1.__RET__
+
+	@Commutativity: Write_Trylock <-> Write_Trylock: !_Method1.__RET__ || !_Method2.__RET__
+	@Commutativity: Write_Trylock <-> Write_Unlock: !_Method1.__RET__
+	@Commutativity: Write_Trylock <-> Write_Lock: !_Method1.__RET__
+	@End
+*/
+
+static inline int read_can_lock(rwlock_t *lock)
+{
+	return atomic_load_explicit(&lock->lock, memory_order_relaxed) > 0;
+}
+
+static inline int write_can_lock(rwlock_t *lock)
+{
+	return atomic_load_explicit(&lock->lock, memory_order_relaxed) == RW_LOCK_BIAS;
+}
+
+
+/**
+	@Begin
+	@Interface: Read_Lock
+	@Commit_point_set: Read_Lock_Success_1 | Read_Lock_Success_2
+	@Check: !writer_lock_acquired
+	@Action: reader_lock_cnt++;
+	@End
+*/
+static inline void read_lock(rwlock_t *rw)
+{
+	int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
+	/**
+		@Begin
+		@Commit_point_define_check: priorvalue > 0
+		@Label:Read_Lock_Success_1
+		@End
+	*/
+	while (priorvalue <= 0) {
+		atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
+		while (atomic_load_explicit(&rw->lock, memory_order_relaxed) <= 0) {
+			thrd_yield();
+		}
+		priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
+		/**
+			@Begin
+			@Commit_point_define_check: priorvalue > 0
+			@Label:Read_Lock_Success_2
+			@End
+		*/
+	}
+}
+
+
+/**
+	@Begin
+	@Interface: Write_Lock
+	@Commit_point_set: Write_Lock_Success_1 | Write_Lock_Success_2
+	@Check: !writer_lock_acquired && reader_lock_cnt == 0
+	@Action: writer_lock_acquired = true;
+	@End
+*/
+static inline void write_lock(rwlock_t *rw)
+{
+	int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
+	/**
+		@Begin
+		@Commit_point_define_check: priorvalue == RW_LOCK_BIAS
+		@Label: Write_Lock_Success_1
+		@End
+	*/
+	while (priorvalue != RW_LOCK_BIAS) {
+		atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
+		while (atomic_load_explicit(&rw->lock, memory_order_relaxed) != RW_LOCK_BIAS) {
+			thrd_yield();
+		}
+		priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
+		/**
+			@Begin
+			@Commit_point_define_check: priorvalue == RW_LOCK_BIAS
+			@Label: Write_Lock_Success_2
+			@End
+		*/
+	}
+}
+
+/**
+	@Begin
+	@Interface: Read_Trylock
+	@Commit_point_set: Read_Trylock_Succ_Point | Read_Trylock_Fail_Point
+	//@Condition: writer_lock_acquired == false
+	@HB_condition: HB_Read_Trylock_Succ :: __RET__ == 1
+	@Action:
+		if (__RET__)
+			reader_lock_cnt++;
+	@Post_check: __RET__ == !writer_lock_acquired || !__RET__
+	@End
+*/
+static inline int read_trylock(rwlock_t *rw)
+{
+	int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
+	/**
+		@Begin
+		@Potential_commit_point_define: true
+		@Label: Potential_Read_Trylock_Point
+		@End
+	*/
+	if (priorvalue > 0) {
+		/**
+			@Begin
+			@Commit_point_define: true
+			@Potential_commit_point_label: Potential_Read_Trylock_Point
+			@Label:  Read_Trylock_Succ_Point
+			@End
+		*/
+		return 1;
+	}
+	/**
+		@Begin
+		@Commit_point_define: true
+		@Potential_commit_point_label: Potential_Read_Trylock_Point
+		@Label:  Read_Trylock_Fail_Point
+		@End
+	*/
+	atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
+	return 0;
+}
+
+/**
+	@Begin
+	@Interface: Write_Trylock
+	@Commit_point_set: Write_Trylock_Succ_Point | Write_Trylock_Fail_Point
+	@HB_condition: HB_Write_Trylock_Succ :: __RET__ == 1
+	@Action:
+		if (__RET__ == 1)
+			writer_lock_acquired = true;
+	@End
+*/
+static inline int write_trylock(rwlock_t *rw)
+{
+	int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
+	//model_print("write_trylock: priorvalue: %d\n", priorvalue);
+	/**
+		@Begin
+		@Potential_commit_point_define: true
+		@Label: Potential_Write_Trylock_Point
+		@End
+	*/
+	if (priorvalue == RW_LOCK_BIAS) {
+		/**
+			@Begin
+			@Commit_point_define: true
+			@Potential_commit_point_label: Potential_Write_Trylock_Point
+			@Label: Write_Trylock_Succ_Point
+			@End
+		*/
+		return 1;
+	}
+	/**
+		@Begin
+		@Commit_point_define: true
+		@Potential_commit_point_label: Potential_Write_Trylock_Point
+		@Label: Write_Trylock_Fail_Point
+		@End
+	*/
+	atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
+	return 0;
+}
+
+/**
+	@Begin
+	@Interface: Read_Unlock
+	@Commit_point_set: Read_Unlock_Point
+	@Check: reader_lock_cnt > 0 && !writer_lock_acquired
+	@Action: reader_lock_cnt--;
+	@End
+*/
+static inline void read_unlock(rwlock_t *rw)
+{
+	/**********  Admissibility  **********/
+	atomic_fetch_add_explicit(&rw->lock, 1, memory_order_release);
+	/**
+		@Begin
+		@Commit_point_define_check: true
+		@Label: Read_Unlock_Point
+		@End
+	*/
+}
+
+/**
+	@Begin
+	@Interface: Write_Unlock
+	@Commit_point_set: Write_Unlock_Point | Write_Unlock_Clear
+	@Check: reader_lock_cnt == 0 && writer_lock_acquired
+	@Action: writer_lock_acquired = false;
+	@End
+*/
+static inline void write_unlock(rwlock_t *rw)
+{
+	/**********  Admissibility  **********/
+	atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_release);
+	/**
+		@Begin
+		@Commit_point_define_check: true
+		@Label: Write_Unlock_Point
+		@End
+	*/
+
+	/**
+		//@Begin
+		@Commit_point_clear: true
+		@Label: Write_Unlock_Clear
+		@End
+	*/
+}
+
+rwlock_t mylock;
+int shareddata;
+
+static void a(void *obj)
+{
+	write_lock(&mylock);
+	//store_32(&shareddata,(unsigned int)i);
+	shareddata = 47;
+	write_unlock(&mylock);
+}
+
+static void b(void *obj)
+{
+	if (write_trylock(&mylock)) {
+		//store_32(&shareddata,(unsigned int)i);
+		shareddata = 47;
+		write_unlock(&mylock);
+	}
+
+	read_lock(&mylock);
+	//load_32(&shareddata);
+	//printf("%d\n", shareddata);
+	read_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;
+}
diff --git a/output/Makefile b/output/Makefile
index c697477..c232475 100644
--- a/output/Makefile
+++ b/output/Makefile
@@ -3,7 +3,7 @@
 	concurrent-hashmap seqlock spsc-example spsc-queue-scfence \
 	treiber-stack
 
-DIRS := ms-queue concurrent-hashmap
+DIRS := ms-queue concurrent-hashmap linuxrwlocks 
 
 .PHONY: $(DIRS)
 
diff --git a/output/linuxrwlocks/Makefile b/output/linuxrwlocks/Makefile
new file mode 100644
index 0000000..c62b36a
--- /dev/null
+++ b/output/linuxrwlocks/Makefile
@@ -0,0 +1,11 @@
+include ../benchmarks.mk
+
+TESTNAME = linuxrwlocks testcase1 testcase2
+
+all: $(TESTNAME)
+
+$(TESTNAME): % : %.c
+	$(CC) -o $@ $< $(CFLAGS) $(LDFLAGS)
+
+clean:
+	rm -f $(TESTNAME) *.o
diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
index 95637ee..4e74668 100644
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
@@ -288,8 +288,15 @@ public class CodeGenerator {
 	public static void main(String[] argvs) {
 		String homeDir = Environment.HOME_DIRECTORY;
 
-//		File[] srcLinuxRWLocks = { new File(homeDir
-//				+ "/benchmark/linuxrwlocks/linuxrwlocks.c") };
+		File[] srcLinuxRWLock1 = {
+				new File(homeDir
+				+ "/benchmark/linuxrwlocks/linuxrwlocks.c") };
+		File[] srcLinuxRWLock2 = {
+				new File(homeDir
+				+ "/benchmark/linuxrwlocks/testcase1.c") };
+		File[] srcLinuxRWLock3 = {
+				new File(homeDir
+				+ "/benchmark/linuxrwlocks/testcase2.c") };
 //
 		File[] srcHashtable = {
 				new File(homeDir
@@ -308,8 +315,8 @@ public class CodeGenerator {
 //		File[] srcRCU = { new File(homeDir
 //				+ "/benchmark/read-copy-update/rcu.cc") };
 //		
-//		File[] srcTrylock = { new File(homeDir
-//				+ "/benchmark/trylock/trylock.c") };
+		File[] srcTrylock = { new File(homeDir
+				+ "/benchmark/trylock/trylock.c") };
 
 //		File[] srcDeque = {
 //				new File(homeDir + "/benchmark/chase-lev-deque-bugfix/deque.c"),
@@ -333,7 +340,7 @@ public class CodeGenerator {
 //		File[][] sources = { srcLinuxRWLocks,  srcMSQueue, srcRCU,
 //				srcDeque, srcMCSLock, srcSPSCQueue, srcMPMCQueue, srcHashtable };
 
-		 File[][] sources = {srcMSQueue, srcHashtable};
+		 File[][] sources = {srcLinuxRWLock1, srcLinuxRWLock2, srcLinuxRWLock3};
 		// Compile all the benchmarks
 		for (int i = 0; i < sources.length; i++) {
 			CodeGenerator gen = new CodeGenerator(sources[i]);
diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
index 4d19458..469006b 100644
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
@@ -662,8 +662,11 @@ public class CodeVariables {
 
 		for (int i = 0; i < rules.size(); i++) {
 			CommutativityRule rule = rules.get(i);
-			String interfaceNumBefore = Integer
-					.toString(semantics.interface2Num.get(rule.method1));
+			Integer method = semantics.interface2Num.get(rule.method1);
+			if (method == null) {
+				System.out.println("Wrong method label in commutativity rule: " + rule.method1);
+			}
+			String interfaceNumBefore = Integer.toString(method);
 			String interfaceNumAfter = Integer.toString(semantics.interface2Num
 					.get(rule.method2));
 			String conditionFuncName = "CommutativityCondition" + i;