minor fix

diff --git a/benchmark/linuxrwlocks/linuxrwlocks.c b/benchmark/linuxrwlocks/linuxrwlocks.c
index 0f52b66b65f5887ed5e0ee6955d079eb3ac97b51..f3d0896c817b1eefb514bd312cd27b462e240c9b 100644 (file)
--- a/benchmark/linuxrwlocks/linuxrwlocks.c
+++ b/benchmark/linuxrwlocks/linuxrwlocks.c
@@ -52,9 +52,6 @@ typedef union {
        @Happens_before:
                # Since commit_point_set has no ID attached, A -> B means that for any B,
                # the previous A happens before B.
        @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)
 
                Write_Unlock -> Write_Lock
                Write_Unlock -> Write_Trylock(HB_Write_Trylock_Succ)
 


@@ -149,7 +146,7 @@ static inline void write_lock(rwlock_t *rw)
        @Begin
        @Interface: Read_Trylock
        @Commit_point_set:
        @Begin
        @Interface: Read_Trylock
        @Commit_point_set:

-               Read_Trylock_Point
+               Read_Trylock_Succ_Point | Read_Trylock_Fail_Point

        @Condition:
                writer_lock_acquired == false
        @HB_condition:
        @Condition:
                writer_lock_acquired == false
        @HB_condition:


@@ -166,13 +163,27 @@ static inline int read_trylock(rwlock_t *rw)
        int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
        /**
                @Begin
        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: true
+               @Label: Potential_Read_Trylock_Point

                @End
        */
                @End
        */

-       if (priorvalue > 0)
+       if (priorvalue > 0) {
+               /**
+                       @Begin
+                       @Commit_point_define: true
+                       @Label:  Read_Trylock_Succ_Point
+                       @Potential_commit_point_label: Potential_Read_Trylock_Point
+                       @End
+               */

                return 1;
                return 1;

-
+       }
+       /**
+               @Begin
+               @Commit_point_define: true
+               @Label:  Read_Trylock_Fail_Point
+               @Potential_commit_point_label: Potential_Read_Trylock_Point
+               @End
+       */

        atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
        return 0;
 }
        atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
        return 0;
 }


@@ -181,7 +192,7 @@ static inline int read_trylock(rwlock_t *rw)
        @Begin
        @Interface: Write_Trylock
        @Commit_point_set:
        @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
        @HB_condition:
        @Condition:
                !writer_lock_acquired && reader_lock_cnt == 0
        @HB_condition:


@@ -198,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
        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: true
+               @Label: Potential_Write_Trylock_Point

                @End
        */
                @End
        */

-       if (priorvalue == RW_LOCK_BIAS)
+       if (priorvalue == RW_LOCK_BIAS) {
+               /**
+                       @Begin
+                       @Commit_point_define: true
+                       @Label: Write_Trylock_Succ_Point
+                       @Potential_commit_point_label: Potential_Write_Trylock_Point
+                       @End
+               */

                return 1;
                return 1;

-
+       }
+       /**
+               @Begin
+               @Commit_point_define: true
+               @Label: Write_Trylock_Fail_Point
+               @Potential_commit_point_label: Potential_Write_Trylock_Point
+               @End
+       */

        atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
        return 0;
 }
        atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
        return 0;
 }