changes with lines of spec counted

[cdsspec-compiler.git] / benchmark / linuxrwlocks / linuxrwlocks.c

diff --git a/benchmark/linuxrwlocks/linuxrwlocks.c b/benchmark/linuxrwlocks/linuxrwlocks.c
index 936a16a1e827df7f3ff0494bb8157daf0e5a028d..b97c45b4b71835f6f74503788487761de78c8b66 100644 (file)
--- 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
 /**
        @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)
        @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
 /**
        @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)
        @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
 /**
        @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++;
        @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)
        @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
 /**
        @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;
        @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
        @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)
        @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
        @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)
        @End
 */
 static inline void write_unlock(rwlock_t *rw)