From: Peizhao Ou <peizhaoo@uci.edu>
Date: Tue, 14 Jan 2014 05:47:39 +0000 (-0800)
Subject: minor fix
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=ae05116999cae16e0f45f3b57f16b93b0e2fa1bd;ds=sidebyside

minor fix
---

diff --git a/benchmark/linuxrwlocks/linuxrwlocks.c b/benchmark/linuxrwlocks/linuxrwlocks.c
index 0f52b66..f3d0896 100644
--- a/benchmark/linuxrwlocks/linuxrwlocks.c
+++ b/benchmark/linuxrwlocks/linuxrwlocks.c
@@ -52,9 +52,6 @@ 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 -> Write_Lock
-		Read_Unlock -> Write_Trylock(HB_Write_Trylock_Succ)
-		
 		Write_Unlock -> Write_Lock
 		Write_Unlock -> Write_Trylock(HB_Write_Trylock_Succ)
 
@@ -149,7 +146,7 @@ static inline void write_lock(rwlock_t *rw)
 	@Begin
 	@Interface: Read_Trylock
 	@Commit_point_set:
-		Read_Trylock_Point
+		Read_Trylock_Succ_Point | Read_Trylock_Fail_Point
 	@Condition:
 		writer_lock_acquired == false
 	@HB_condition:
@@ -166,13 +163,27 @@ static inline int read_trylock(rwlock_t *rw)
 	int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
 	/**
 		@Begin
-		@Commit_point_define_check: true
-		@Label:Read_Trylock_Point
+		@Potential_commit_point: true
+		@Label: Potential_Read_Trylock_Point
 		@End
 	*/
-	if (priorvalue > 0)
+	if (priorvalue > 0) {
+		/**
+			@Begin
+			@Commit_point_define: true
+			@Label:  Read_Trylock_Succ_Point
+			@Potential_commit_point_label: Potential_Read_Trylock_Point
+			@End
+		*/
 		return 1;
-
+	}
+	/**
+		@Begin
+		@Commit_point_define: true
+		@Label:  Read_Trylock_Fail_Point
+		@Potential_commit_point_label: Potential_Read_Trylock_Point
+		@End
+	*/
 	atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
 	return 0;
 }
@@ -181,7 +192,7 @@ static inline int read_trylock(rwlock_t *rw)
 	@Begin
 	@Interface: Write_Trylock
 	@Commit_point_set:
-		Write_Trylock_Point
+		Write_Trylock_Succ_Point | Write_Trylock_Fail_Point
 	@Condition:
 		!writer_lock_acquired && reader_lock_cnt == 0
 	@HB_condition:
@@ -198,13 +209,27 @@ static inline int write_trylock(rwlock_t *rw)
 	int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
 	/**
 		@Begin
-		@Commit_point_define_check: true
-		@Label: Write_Trylock_Point
+		@Potential_commit_point: true
+		@Label: Potential_Write_Trylock_Point
 		@End
 	*/
-	if (priorvalue == RW_LOCK_BIAS)
+	if (priorvalue == RW_LOCK_BIAS) {
+		/**
+			@Begin
+			@Commit_point_define: true
+			@Label: Write_Trylock_Succ_Point
+			@Potential_commit_point_label: Potential_Write_Trylock_Point
+			@End
+		*/
 		return 1;
-
+	}
+	/**
+		@Begin
+		@Commit_point_define: true
+		@Label: Write_Trylock_Fail_Point
+		@Potential_commit_point_label: Potential_Write_Trylock_Point
+		@End
+	*/
 	atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
 	return 0;
 }