injection result for ms-queue

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

diff --git a/benchmark/linuxrwlocks/linuxrwlocks.c b/benchmark/linuxrwlocks/linuxrwlocks.c
index 0f52b66b65f5887ed5e0ee6955d079eb3ac97b51..0a1a7b203f02f6477623c5ed8f64765ca341a10a 100644 (file)
--- a/benchmark/linuxrwlocks/linuxrwlocks.c
+++ b/benchmark/linuxrwlocks/linuxrwlocks.c
@@ -2,6 +2,13 @@
 #include <threads.h>
 #include <stdatomic.h>
 
+#include <spec_lib.h>
+#include <stdlib.h>
+#include <cdsannotate.h>
+#include <specannotation.h>
+#include <model_memory.h>
+#include "common.h"
+
 #include "librace.h"
 
 #define RW_LOCK_BIAS            0x00100000
@@ -42,6 +49,8 @@ typedef union {
 
 /**
        @Begin
+       @Options:
+               LANG = C;
        @Global_define:
                @DeclareVar:
                        bool writer_lock_acquired;
@@ -52,9 +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)
 
@@ -149,7 +160,7 @@ 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
        @HB_condition:
@@ -166,13 +177,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;
 }
@@ -181,30 +206,41 @@ static inline int read_trylock(rwlock_t *rw)
        @Begin
        @Interface: Write_Trylock
        @Commit_point_set:
-               Write_Trylock_Point
-       @Condition:
-               !writer_lock_acquired && reader_lock_cnt == 0
+               Write_Trylock_Succ_Point | Write_Trylock_Fail_Point
        @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
-               @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;
 }
@@ -260,16 +296,36 @@ static void a(void *obj)
        for(i = 0; i < 2; i++) {
                if ((i % 2) == 0) {
                        read_lock(&mylock);
-                       load_32(&shareddata);
+                       //load_32(&shareddata);
+                       printf("%d\n", shareddata);
                        read_unlock(&mylock);
                } else {
                        write_lock(&mylock);
-                       store_32(&shareddata,(unsigned int)i);
+                       //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);
+                       }
+               }
+       }
+}
+
 int user_main(int argc, char **argv)
 {
        /**
@@ -281,7 +337,7 @@ int user_main(int argc, char **argv)
        atomic_init(&mylock.lock, RW_LOCK_BIAS);
 
        thrd_create(&t1, (thrd_start_t)&a, NULL);
-       thrd_create(&t2, (thrd_start_t)&a, NULL);
+       thrd_create(&t2, (thrd_start_t)&b, NULL);
 
        thrd_join(t1);
        thrd_join(t2);