X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=blobdiff_plain;f=benchmark%2Flinuxrwlocks%2Flinuxrwlocks.c;h=b97c45b4b71835f6f74503788487761de78c8b66;hp=936a16a1e827df7f3ff0494bb8157daf0e5a028d;hb=7f2fd73fe54a04e0f795e7b8f6e28b3a7708df03;hpb=2d5eeaa6ee1e3f22dff90b00780fdfce5e70b13c

diff --git a/benchmark/linuxrwlocks/linuxrwlocks.c b/benchmark/linuxrwlocks/linuxrwlocks.c
index 936a16a..b97c45b 100644
--- a/benchmark/linuxrwlocks/linuxrwlocks.c
+++ b/benchmark/linuxrwlocks/linuxrwlocks.c
@@ -88,12 +88,9 @@ static inline int write_can_lock(rwlock_t *lock)
 /**
 	@Begin
 	@Interface: Read_Lock
-	@Commit_point_set:
-		Read_Lock_Success_1 | Read_Lock_Success_2
-	@Check:
-		!writer_lock_acquired
-	@Action:
-		reader_lock_cnt++;
+	@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)
@@ -124,12 +121,9 @@ static inline void read_lock(rwlock_t *rw)
 /**
 	@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;
+	@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)
@@ -159,17 +153,13 @@ static inline void write_lock(rwlock_t *rw)
 /**
 	@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
+	@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 (__COND_SAT__)
 			reader_lock_cnt++;
-	@Post_check:
-		__COND_SAT__ ? __RET__ == 1 : __RET__ == 0
+	@Post_check: __COND_SAT__ ? __RET__ == 1 : __RET__ == 0
 	@End
 */
 static inline int read_trylock(rwlock_t *rw)
@@ -205,10 +195,8 @@ static inline int read_trylock(rwlock_t *rw)
 /**
 	@Begin
 	@Interface: Write_Trylock
-	@Commit_point_set:
-		Write_Trylock_Succ_Point | Write_Trylock_Fail_Point
-	@HB_condition:
-		HB_Write_Trylock_Succ :: __RET__ == 1
+	@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;
@@ -249,10 +237,8 @@ static inline int write_trylock(rwlock_t *rw)
 	@Begin
 	@Interface: Read_Unlock
 	@Commit_point_set: Read_Unlock_Point
-	@Check:
-		reader_lock_cnt > 0 && !writer_lock_acquired
-	@Action: 
-		reader_lock_cnt--;
+	@Check: reader_lock_cnt > 0 && !writer_lock_acquired
+	@Action: reader_lock_cnt--;
 	@End
 */
 static inline void read_unlock(rwlock_t *rw)
@@ -270,10 +256,8 @@ static inline void read_unlock(rwlock_t *rw)
 	@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;
+	@Check: reader_lock_cnt == 0 && writer_lock_acquired
+	@Action: writer_lock_acquired = false;
 	@End
 */
 static inline void write_unlock(rwlock_t *rw)