The CDSSpec checker's benchmarks
[model-checker-benchmarks.git] / linuxrwlocks / testcase3.c
1 #include <stdio.h>
2 #include <threads.h>
3 #include <stdatomic.h>
4
5 #include "librace.h"
6 #include "linuxrwlocks.h"
7
8 rwlock_t mylock;
9 int shareddata;
10
11 atomic_int x, y;
12
13 static void a(void *obj)
14 {
15         write_lock(&mylock);
16         atomic_store_explicit(&x, 17, memory_order_relaxed);
17         write_unlock(&mylock);
18         
19         if (!read_can_lock(&mylock))
20                 return;
21         if (read_trylock(&mylock)) {
22                 atomic_load_explicit(&x, memory_order_relaxed);
23                 read_unlock(&mylock);
24         }
25 }
26
27 static void b(void *obj)
28 {
29
30         if (write_trylock(&mylock)) {
31                 atomic_store_explicit(&x, 16, memory_order_relaxed);
32                 write_unlock(&mylock);
33         }
34         
35         read_lock(&mylock);
36         atomic_load_explicit(&x, memory_order_relaxed);
37         read_unlock(&mylock);
38 }
39
40 int user_main(int argc, char **argv)
41 {
42         thrd_t t1, t2;
43         /** @Entry */
44         atomic_init(&mylock.lock, RW_LOCK_BIAS);
45         atomic_init(&x, 0);
46         atomic_init(&y, 0);
47
48         thrd_create(&t1, (thrd_start_t)&a, NULL);
49         thrd_create(&t2, (thrd_start_t)&b, NULL);
50
51         thrd_join(t1);
52         thrd_join(t2);
53
54         return 0;
55 }