fix header in the middle of code bug

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

diff --git a/benchmark/linuxrwlocks/linuxrwlocks.c b/benchmark/linuxrwlocks/linuxrwlocks.c
index 9dd2bf897b893073648badb9b0e2681e84aaff8a..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... */
 
@@ -45,13 +49,9 @@
                @InitVar:
                        writer_lock_acquired = false;
                        reader_lock_cnt = 0;
-               @DefineFunc:
        @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)
 
@@ -60,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;
@@ -84,10 +77,9 @@ static inline int write_can_lock(rwlock_t *lock)
        @Commit_point_set:
                Read_Lock_Success_1 | Read_Lock_Success_2
        @Check:
-               !__sequential.writer_lock_acquired
+               !writer_lock_acquired
        @Action:
-               @Code:
-               __sequential.reader_lock_cnt++;
+               reader_lock_cnt++;
        @End
 */
 static inline void read_lock(rwlock_t *rw)
@@ -95,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
        */
@@ -107,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
                */
@@ -121,10 +113,9 @@ static inline void read_lock(rwlock_t *rw)
        @Commit_point_set:
                Write_Lock_Success_1 | Write_Lock_Success_2
        @Check:
-               !__sequential.writer_lock_acquired && __sequential.reader_lock_cnt == 0
+               !writer_lock_acquired && reader_lock_cnt == 0
        @Action:
-               @Code:
-               __sequential.writer_lock_acquired = true;
+               writer_lock_acquired = true;
        @End
 */
 static inline void write_lock(rwlock_t *rw)
@@ -132,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
        */
@@ -144,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
                */
@@ -155,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:
-               __sequential.writer_lock_acquired == false
+               writer_lock_acquired == false
        @HB_condition:
                HB_Read_Trylock_Succ :: __RET__ == 1
        @Action:
-               @Code:
-               if (__COND_SAY__)
-                       __sequential.reader_lock_cnt++;
+               if (__COND_SAT__)
+                       reader_lock_cnt++;
        @Post_check:
-               __COND_SAY__ ? __RET__ == 1 : __RET__ == 0
+               __COND_SAT__ ? __RET__ == 1 : __RET__ == 0
        @End
 */
 static inline int read_trylock(rwlock_t *rw)
@@ -173,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;
 }
@@ -188,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:
-               !__sequential.writer_lock_acquired && __sequential.reader_lock_cnt == 0
+               !writer_lock_acquired && reader_lock_cnt == 0
        @HB_condition:
                HB_Write_Trylock_Succ :: __RET__ == 1
        @Action:
-               @Code:
-               if (__COND_SAY__)
-                       __sequential.writer_lock_acquired = true;
+               if (__COND_SAT__)
+                       writer_lock_acquired = true;
        @Post_check:
-               __COND_SAY__ ? __RET__ == 1 : __RET__ == 0
+               __COND_SAT__ ? __RET__ == 1 : __RET__ == 0
        @End
 */
 static inline int write_trylock(rwlock_t *rw)
@@ -206,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;
 }
@@ -222,9 +239,8 @@ static inline int write_trylock(rwlock_t *rw)
        @Interface: Read_Unlock
        @Commit_point_set: Read_Unlock_Point
        @Check:
-               __sequential.reader_lock_cnt > 0 && !__sequential.writer_lock_acquired
+               reader_lock_cnt > 0 && !writer_lock_acquired
        @Action: 
-               @Code:
                reader_lock_cnt--;
        @End
 */
@@ -246,11 +262,9 @@ static inline void read_unlock(rwlock_t *rw)
        @Check:
                reader_lock_cnt == 0 && writer_lock_acquired
        @Action: 
-               @Code:
-               __sequential.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);
@@ -283,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);