changes with lines of spec counted
[cdsspec-compiler.git] / benchmark / linuxrwlocks / linuxrwlocks.c
index 936a16a..b97c45b 100644 (file)
@@ -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)