edits

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

diff --git a/benchmark/linuxrwlocks/linuxrwlocks.c b/benchmark/linuxrwlocks/linuxrwlocks.c
index 936a16a1e827df7f3ff0494bb8157daf0e5a028d..1f7059f828004926926c0b0682b52cf909804c9d 100644 (file)
--- a/benchmark/linuxrwlocks/linuxrwlocks.c
+++ b/benchmark/linuxrwlocks/linuxrwlocks.c
@@ -61,16 +61,34 @@ 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 -> Read_Lock
                Read_Unlock -> Write_Lock
                Read_Unlock -> Write_Trylock(HB_Write_Trylock_Succ)
-               Read_Unlock -> Read_Trylock(HB_Read_Trylock_Succ)
+               #Read_Unlock -> Read_Trylock(HB_Read_Trylock_Succ)
 
                Write_Unlock -> Write_Lock
                Write_Unlock -> Write_Trylock(HB_Write_Trylock_Succ)
 
                Write_Unlock -> Read_Lock
                Write_Unlock -> Read_Trylock(HB_Read_Trylock_Succ)
+       
+       @Commutativity: Read_Lock <-> Read_Lock: true
+       @Commutativity: Read_Lock <-> Read_Unlock: true
+       @Commutativity: Read_Lock <-> Read_Trylock: true
+       @Commutativity: Read_Lock <-> Write_Trylock: !_Method2.__RET__
+       
+       @Commutativity: Read_Unlock <-> Read_Unlock: true
+       @Commutativity: Read_Unlock <-> Read_Trylock: true
+       @Commutativity: Read_Unlock <-> Write_Trylock: !_Method2.__RET__
+
+       @Commutativity: Read_Trylock <-> Read_Trylock: true
+       @Commutativity: Read_Trylock <-> Write_Trylock: !_Method1.__RET__ || !_Method2.__RET__
+       @Commutativity: Read_Trylock <-> Write_Lock: !_Method1.__RET__
+       @Commutativity: Read_Trylock <-> Write_Unlock: !_Method1.__RET__
+
+       @Commutativity: Write_Trylock <-> Write_Trylock: !_Method1.__RET__ || !_Method2.__RET__
+       @Commutativity: Write_Trylock <-> Write_Unlock: !_Method1.__RET__
+       @Commutativity: Write_Trylock <-> Write_Lock: !_Method1.__RET__
        @End
 */
 
@@ -88,16 +106,15 @@ static inline int write_can_lock(rwlock_t *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)
 {
+       
+       /**********  Admissibility  **********/
        int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
        /**
                @Begin
@@ -110,6 +127,7 @@ static inline void read_lock(rwlock_t *rw)
                while (atomic_load_explicit(&rw->lock, memory_order_relaxed) <= 0) {
                        thrd_yield();
                }
+               /**********  Admissibility  **********/
                priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
                /**
                        @Begin
@@ -124,16 +142,14 @@ static inline void read_lock(rwlock_t *rw)
 /**
        @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)
 {
+       /**********  Admissibility  **********/
        int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
        /**
                @Begin
@@ -146,6 +162,7 @@ static inline void write_lock(rwlock_t *rw)
                while (atomic_load_explicit(&rw->lock, memory_order_relaxed) != RW_LOCK_BIAS) {
                        thrd_yield();
                }
+               /**********  Admissibility  **********/
                priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
                /**
                        @Begin
@@ -159,21 +176,18 @@ static inline void write_lock(rwlock_t *rw)
 /**
        @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__)
+               if (__RET__)
                        reader_lock_cnt++;
-       @Post_check:
-               __COND_SAT__ ? __RET__ == 1 : __RET__ == 0
+       @Post_check: __RET__ == !writer_lock_acquired || !__RET__
        @End
 */
 static inline int read_trylock(rwlock_t *rw)
 {
+       /**********  Admissibility  **********/
        int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
        /**
                @Begin
@@ -205,10 +219,8 @@ static inline int read_trylock(rwlock_t *rw)
 /**
        @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;
@@ -216,6 +228,7 @@ static inline int read_trylock(rwlock_t *rw)
 */
 static inline int write_trylock(rwlock_t *rw)
 {
+       /**********  Admissibility  **********/
        int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
        //model_print("write_trylock: priorvalue: %d\n", priorvalue);
        /**
@@ -249,14 +262,13 @@ static inline int write_trylock(rwlock_t *rw)
        @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)
 {
+       /**********  Admissibility  **********/
        atomic_fetch_add_explicit(&rw->lock, 1, memory_order_release);
        /**
                @Begin
@@ -270,14 +282,13 @@ static inline void read_unlock(rwlock_t *rw)
        @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)
 {
+       /**********  Admissibility  **********/
        atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_release);
        /**
                @Begin
@@ -299,37 +310,27 @@ int shareddata;
 
 static void a(void *obj)
 {
-       int i;
-       for(i = 0; i < 2; i++) {
-               if ((i % 2) == 0) {
-                       read_lock(&mylock);
-                       //load_32(&shareddata);
-                       //printf("%d\n", shareddata);
-                       read_unlock(&mylock);
-               } else {
-                       write_lock(&mylock);
-                       //store_32(&shareddata,(unsigned int)i);
-                       shareddata = 47;
-                       write_unlock(&mylock);
-               }
-       }
+       read_lock(&mylock);
+       //load_32(&shareddata);
+       //printf("%d\n", shareddata);
+       read_unlock(&mylock);
+       
+       write_lock(&mylock);
+       //store_32(&shareddata,(unsigned int)i);
+       shareddata = 47;
+       write_unlock(&mylock);
 }
 
 static void b(void *obj)
 {
-       int i;
-       for(i = 0; i < 2; i++) {
-               if ((i % 2) == 0) {
-                       if (read_trylock(&mylock) == 1) {
-                               //printf("%d\n", shareddata);
-                               read_unlock(&mylock);
-                       }
-               } else {
-                       if (write_trylock(&mylock) == 1) {
-                               //shareddata = 47;
-                               write_unlock(&mylock);
-                       }
-               }
+       if (read_trylock(&mylock) == 1) {
+               //printf("%d\n", shareddata);
+               read_unlock(&mylock);
+       }
+       
+       if (write_trylock(&mylock) == 1) {
+               //shareddata = 47;
+               write_unlock(&mylock);
        }
 }