minor fix

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

diff --git a/benchmark/linuxrwlocks/linuxrwlocks.c b/benchmark/linuxrwlocks/linuxrwlocks.c
index 7fb604c52d72259e2ee55c073cdf08b5c61456d9..142e3766cf350e504a79079b3d80b8d14a9c8faf 100644 (file)
--- a/benchmark/linuxrwlocks/linuxrwlocks.c
+++ b/benchmark/linuxrwlocks/linuxrwlocks.c
@@ -7,6 +7,10 @@
 #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... */
 
@@ -39,15 +43,15 @@
 /**
        @Begin
        @Global_define:
-               bool __writer_lock_acquired = false;
-               int __reader_lock_cnt = 0;
-       
+               @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 -> Write_Lock
-               Read_Unlock -> Write_Trylock(HB_Write_Trylock_Succ)
-               
                Write_Unlock -> Write_Lock
                Write_Unlock -> Write_Trylock(HB_Write_Trylock_Succ)
 
@@ -56,13 +60,6 @@
        @End
 */
 
-/**
-       */
-
-typedef union {
-       atomic_int lock;
-} rwlock_t;
-
 static inline int read_can_lock(rwlock_t *lock)
 {
        return atomic_load_explicit(&lock->lock, memory_order_relaxed) > 0;
@@ -80,10 +77,9 @@ static inline int write_can_lock(rwlock_t *lock)
        @Commit_point_set:
                Read_Lock_Success_1 | Read_Lock_Success_2
        @Check:
-               !__writer_lock_acquired
+               !writer_lock_acquired
        @Action:
-               @Code:
-               __reader_lock_cnt++;
+               reader_lock_cnt++;
        @End
 */
 static inline void read_lock(rwlock_t *rw)
@@ -91,7 +87,7 @@ 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: __ATOMIC_RET__ > 0
+               @Commit_point_define_check: priorvalue > 0
                @Label:Read_Lock_Success_1
                @End
        */
@@ -103,7 +99,7 @@ static inline void read_lock(rwlock_t *rw)
                priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
                /**
                        @Begin
-                       @Commit_point_define_check: __ATOMIC_RET__ > 0
+                       @Commit_point_define_check: priorvalue > 0
                        @Label:Read_Lock_Success_2
                        @End
                */
@@ -117,10 +113,9 @@ static inline void read_lock(rwlock_t *rw)
        @Commit_point_set:
                Write_Lock_Success_1 | Write_Lock_Success_2
        @Check:
-               !__writer_lock_acquired && __reader_lock_cnt == 0
+               !writer_lock_acquired && reader_lock_cnt == 0
        @Action:
-               @Code:
-               __writer_lock_acquired = true;
+               writer_lock_acquired = true;
        @End
 */
 static inline void write_lock(rwlock_t *rw)
@@ -128,7 +123,7 @@ 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: __ATOMIC_RET__ == RW_LOCK_BIAS
+               @Commit_point_define_check: priorvalue == RW_LOCK_BIAS
                @Label: Write_Lock_Success_1
                @End
        */
@@ -140,7 +135,7 @@ static inline void write_lock(rwlock_t *rw)
                priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
                /**
                        @Begin
-                       @Commit_point_define_check: __ATOMIC_RET__ == RW_LOCK_BIAS
+                       @Commit_point_define_check: priorvalue == RW_LOCK_BIAS
                        @Label: Write_Lock_Success_2
                        @End
                */
@@ -151,17 +146,16 @@ 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
+               writer_lock_acquired == false
        @HB_condition:
                HB_Read_Trylock_Succ :: __RET__ == 1
        @Action:
-               @Code:
-               if (COND_SAT)
-                       __reader_lock_cnt++;
+               if (__COND_SAT__)
+                       reader_lock_cnt++;
        @Post_check:
-               COND_SAT ? __RET__ == 1 : __RET__ == 0
+               __COND_SAT__ ? __RET__ == 1 : __RET__ == 0
        @End
 */
 static inline int read_trylock(rwlock_t *rw)
@@ -169,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_define: true
+               @Label: Potential_Read_Trylock_Point
                @End
        */
-       if (priorvalue > 0)
+       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;
 }
@@ -184,17 +192,16 @@ 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
+               !writer_lock_acquired && reader_lock_cnt == 0
        @HB_condition:
                HB_Write_Trylock_Succ :: __RET__ == 1
        @Action:
-               @Code:
-               if (COND_SAT)
-                       __writer_lock_acquired = true;
+               if (__COND_SAT__)
+                       writer_lock_acquired = true;
        @Post_check:
-               COND_SAT ? __RET__ == 1 : __RET__ == 0
+               __COND_SAT__ ? __RET__ == 1 : __RET__ == 0
        @End
 */
 static inline int write_trylock(rwlock_t *rw)
@@ -202,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_define: true
+               @Label: Potential_Write_Trylock_Point
                @End
        */
-       if (priorvalue == RW_LOCK_BIAS)
+       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;
 }
@@ -218,9 +239,8 @@ static inline int write_trylock(rwlock_t *rw)
        @Interface: Read_Unlock
        @Commit_point_set: Read_Unlock_Point
        @Check:
-               __reader_lock_cnt > 0 && !__writer_lock_acquired
+               reader_lock_cnt > 0 && !writer_lock_acquired
        @Action: 
-               @Code:
                reader_lock_cnt--;
        @End
 */
@@ -242,11 +262,9 @@ static inline void read_unlock(rwlock_t *rw)
        @Check:
                reader_lock_cnt == 0 && writer_lock_acquired
        @Action: 
-               @Code:
-               __writer_lock_acquired = false;
+               writer_lock_acquired = false;
        @End
 */
-
 static inline void write_unlock(rwlock_t *rw)
 {
        atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_release);
@@ -279,6 +297,11 @@ static void a(void *obj)
 
 int user_main(int argc, char **argv)
 {
+       /**
+               @Begin
+               @Entry_point
+               @End
+       */
        thrd_t t1, t2;
        atomic_init(&mylock.lock, RW_LOCK_BIAS);