650d0f8c742f4b5103fcb36da63cbb8564b1aa13
[satcheck.git] / clang / test / linuxrwlocks.c
1 #include <stdio.h>
2 #include <threads.h>
3 #include <stdatomic.h>
4
5 #include "libinterface.h"
6
7 #define RW_LOCK_BIAS            0x00100000
8 #define WRITE_LOCK_CMP          RW_LOCK_BIAS
9
10 /** Example implementation of linux rw lock along with 2 thread test
11  *  driver... */
12
13 typedef union {
14         int lock;
15 } rwlock_t;
16
17 static inline void read_lock(MCID _mrw, rwlock_t *rw)
18 {
19         MCID _rmw0 = MC2_nextRMW(MCID_NODEP, MCID_NODEP, MCID_NODEP);
20         int priorvalue=rmw_32(ADD, &rw->lock, /* dummy */ 0, ((unsigned int)-1));
21
22         MC2_enterLoop();
23         while (true) {
24                 MCID _br0;
25
26                 int _cond0 = priorvalue <= 0;
27                 MCID _cond0_m = MC2_function(1, sizeof(_cond0), _cond0, _rmw0);
28                 if (_cond0) {_br0 = MC2_branchUsesID(_cond0_m, 1, 2, true);
29                 
30                         MC2_merge(_br0);
31                 } else {
32                         _br0 = MC2_branchUsesID(_cond0_m, 0, 2, true);
33                         break;
34                 }
35
36                 MCID _rmw1 = MC2_nextRMW(MCID_NODEP, MCID_NODEP, MCID_NODEP);
37                 rmw_32(ADD, &rw->lock, /* dummy */ 0, 1);
38
39                 MC2_enterLoop();
40                 while (true) {
41                         MCID _mstatus; _mstatus=MC2_nextOpLoadOffset(_mrw, MC2_OFFSET(rwlock_t *, lock)); int status = load_32(&rw->lock);
42                         MCID _br1;
43
44                         int _cond1 = status > 0;
45                         MCID _cond1_m = MC2_function(1, sizeof(_cond1), _cond1, _mstatus);
46                         if (_cond1) {_br1 = MC2_branchUsesID(_cond1_m, 1, 2, true);
47                         
48                                 MC2_merge(_br1);
49                         } else {
50                                 _br1 = MC2_branchUsesID(_cond1_m, 0, 2, true);
51                                 break;
52                         }
53                         MC2_yield();
54                 }
55 MC2_exitLoop();
56
57
58                 MCID _rmw2 = MC2_nextRMW(MCID_NODEP, MCID_NODEP, MCID_NODEP);
59                 priorvalue=rmw_32(ADD, &rw->lock, /* dummy */ 0, ((unsigned int)-1));
60                 MC2_loopIterate();
61         }
62 MC2_exitLoop();
63
64 }
65
66 static inline void write_lock(MCID _mrw, rwlock_t *rw)
67 {
68         MCID _rmw3 = MC2_nextRMW(MCID_NODEP, MCID_NODEP, MCID_NODEP);
69         int priorvalue=rmw_32(ADD, &rw->lock, /* dummy */ 0, ((unsigned int)-(RW_LOCK_BIAS)));
70         MC2_enterLoop();
71         while(true) {
72
73                 MCID _br2;
74
75                 int _cond2 = priorvalue != 1048576;
76                 MCID _cond2_m = MC2_function(1, sizeof(_cond2), _cond2, _rmw3);
77                 if (_cond2) {_br2 = MC2_branchUsesID(_cond2_m, 1, 2, true);
78                 
79                         MC2_merge(_br2);
80                 } else {
81                         _br2 = MC2_branchUsesID(_cond2_m, 0, 2, true);
82                         break;
83                 }
84
85                 MCID _rmw4 = MC2_nextRMW(MCID_NODEP, MCID_NODEP, MCID_NODEP);
86                 rmw_32(ADD, &rw->lock, /* dummy */ 0, RW_LOCK_BIAS);
87                 
88                 MC2_enterLoop();
89                 while (true) {
90                         MCID _mstatus; _mstatus=MC2_nextOpLoadOffset(_mrw, MC2_OFFSET(rwlock_t *, lock)); int status = load_32(&rw->lock);
91                         MCID _br3;
92
93                         int _cond3 = status != 1048576;
94                         MCID _cond3_m = MC2_function(1, sizeof(_cond3), _cond3, _mstatus);
95                         if (_cond3) {_br3 = MC2_branchUsesID(_cond3_m, 1, 2, true);
96                         
97                                 MC2_merge(_br3);
98                         } else {
99                                 _br3 = MC2_branchUsesID(_cond3_m, 0, 2, true);
100                                 break;
101                         }
102                         MC2_yield();
103                 }
104 MC2_exitLoop();
105
106
107                 MCID _rmw5 = MC2_nextRMW(MCID_NODEP, MCID_NODEP, MCID_NODEP);
108                 priorvalue=rmw_32(ADD, &rw->lock, /* dummy */ 0, ((unsigned int)-(RW_LOCK_BIAS)));
109         }
110 MC2_exitLoop();
111
112 }
113
114 static inline bool write_trylock(MCID _mrw, rwlock_t *rw, MCID * retval)
115 {
116         MCID _rmw6 = MC2_nextRMW(MCID_NODEP, MCID_NODEP, MCID_NODEP);
117         int priorvalue=rmw_32(ADD, &rw->lock, /* dummy */ 0, ((unsigned int)-(RW_LOCK_BIAS)));
118
119         MCID _fn0; int flag = priorvalue != RW_LOCK_BIAS;
120         _fn0 = MC2_function(1, sizeof (flag), flag, _rmw6);
121         MCID _br4;
122         if (flag) {_br4 = MC2_branchUsesID(_fn0, 1, 2, true);
123         
124                 MC2_merge(_br4);
125         } else {
126                 _br4 = MC2_branchUsesID(_fn0, 0, 2, true);
127                 MCID _rmw7 = MC2_nextRMW(MCID_NODEP, MCID_NODEP, MCID_NODEP);
128                 rmw_32(ADD, &rw->lock, /* dummy */ 0, RW_LOCK_BIAS);
129                 MC2_merge(_br4);
130         }
131
132         *retval = _fn0;
133         return flag;
134 }
135
136 static inline void read_unlock(MCID _mrw, rwlock_t *rw)
137 {
138         MCID _rmw8 = MC2_nextRMW(MCID_NODEP, MCID_NODEP, MCID_NODEP);
139         rmw_32(ADD, &rw->lock, /* dummy */ 0, 1);
140 }
141
142 static inline void write_unlock(MCID _mrw, rwlock_t *rw)
143 {
144         MCID _rmw9 = MC2_nextRMW(MCID_NODEP, MCID_NODEP, MCID_NODEP);
145         rmw_32(ADD, &rw->lock, /* dummy */ 0, RW_LOCK_BIAS);
146 }
147
148 MCID _mmylock; rwlock_t mylock;
149 int shareddata;
150
151 static void foo() {
152         MCID _rv0;
153         int flag=write_trylock(MCID_NODEP, &mylock, &_rv0);
154         MCID _br5;
155         if (flag) {
156                 _br5 = MC2_branchUsesID(_rv0, 1, 2, true);
157                 write_unlock(MCID_NODEP, &mylock);
158                 MC2_merge(_br5);
159         } else { _br5 = MC2_branchUsesID(_rv0, 0, 2, true); MC2_merge(_br5);
160          }
161 }
162
163 static void a(void *obj)
164 {
165         int i;
166         MC2_enterLoop();
167         for(i=0;i<13;i++)
168                 foo();
169 MC2_exitLoop();
170
171 }
172
173 int user_main(int argc, char **argv)
174 {
175         thrd_t t1, t2;
176         //, t3, t4;
177         MC2_nextOpStoreOffset(_mmylock, MC2_OFFSET(rwlock_t, lock), MCID_NODEP);
178         store_32(&mylock.lock, RW_LOCK_BIAS);
179
180         thrd_create(&t1, (thrd_start_t)&a, NULL);
181         thrd_create(&t2, (thrd_start_t)&a, NULL);
182         //      thrd_create(&t3, (thrd_start_t)&a, NULL);
183         //      thrd_create(&t4, (thrd_start_t)&a, NULL);
184
185         thrd_join(t1);
186         thrd_join(t2);
187         //      thrd_join(t3);
188         //      thrd_join(t4);
189
190         return 0;
191 }