add trylock

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

diff --git a/benchmark/linuxrwlocks/linuxrwlocks.c b/benchmark/linuxrwlocks/linuxrwlocks.c
index 6341c4c1fcf336474ea9008b5e84b3e083b0968f..936a16a1e827df7f3ff0494bb8157daf0e5a028d 100644 (file)
--- a/benchmark/linuxrwlocks/linuxrwlocks.c
+++ b/benchmark/linuxrwlocks/linuxrwlocks.c
@@ -61,6 +61,11 @@ 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.
+               Read_Unlock -> Read_Lock
+               Read_Unlock -> Write_Lock
+               Read_Unlock -> Write_Trylock(HB_Write_Trylock_Succ)
+               Read_Unlock -> Read_Trylock(HB_Read_Trylock_Succ)
+
                Write_Unlock -> Write_Lock
                Write_Unlock -> Write_Trylock(HB_Write_Trylock_Succ)
 
@@ -202,20 +207,17 @@ static inline int read_trylock(rwlock_t *rw)
        @Interface: Write_Trylock
        @Commit_point_set:
                Write_Trylock_Succ_Point | Write_Trylock_Fail_Point
-       @Condition:
-               !writer_lock_acquired && reader_lock_cnt == 0
        @HB_condition:
                HB_Write_Trylock_Succ :: __RET__ == 1
        @Action:
-               if (__COND_SAT__)
+               if (__RET__ == 1)
                        writer_lock_acquired = true;
-       @Post_check:
-               __COND_SAT__ ? __RET__ == 1 : __RET__ == 0
        @End
 */
 static inline int write_trylock(rwlock_t *rw)
 {
        int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
+       //model_print("write_trylock: priorvalue: %d\n", priorvalue);
        /**
                @Begin
                @Potential_commit_point_define: true
@@ -267,7 +269,7 @@ static inline void read_unlock(rwlock_t *rw)
 /**
        @Begin
        @Interface: Write_Unlock
-       @Commit_point_set: Write_Unlock_Point
+       @Commit_point_set: Write_Unlock_Point | Write_Unlock_Clear
        @Check:
                reader_lock_cnt == 0 && writer_lock_acquired
        @Action: 
@@ -283,6 +285,13 @@ static inline void write_unlock(rwlock_t *rw)
                @Label: Write_Unlock_Point
                @End
        */
+
+       /**
+               //@Begin
+               @Commit_point_clear: true
+               @Label: Write_Unlock_Clear
+               @End
+       */
 }
 
 rwlock_t mylock;
@@ -295,7 +304,7 @@ static void a(void *obj)
                if ((i % 2) == 0) {
                        read_lock(&mylock);
                        //load_32(&shareddata);
-                       printf("%d\n", shareddata);
+                       //printf("%d\n", shareddata);
                        read_unlock(&mylock);
                } else {
                        write_lock(&mylock);
@@ -312,12 +321,12 @@ static void b(void *obj)
        for(i = 0; i < 2; i++) {
                if ((i % 2) == 0) {
                        if (read_trylock(&mylock) == 1) {
-                               printf("%d\n", shareddata);
+                               //printf("%d\n", shareddata);
                                read_unlock(&mylock);
                        }
                } else {
                        if (write_trylock(&mylock) == 1) {
-                               shareddata = 47;
+                               //shareddata = 47;
                                write_unlock(&mylock);
                        }
                }