7 #include "libinterface.h"
10 /*atomic_*/ int _data;
13 MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
15 MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
22 MCID _mold_seq; _mold_seq=MC2_nextOpLoad(MCID_NODEP); int old_seq = load_32(&_seq);
24 MCID _fn0; int c0 = (old_seq % 2 == 1);
25 _fn0 = MC2_function(1, sizeof (c0), c0, _mold_seq);
28 _br0 = MC2_branchUsesID(_fn0, 1, 2, true);
32 MCID _mres; _br0 = MC2_branchUsesID(_fn0, 0, 2, true);
33 _mres=MC2_nextOpLoad(MCID_NODEP); int res = load_32(&_data);
34 MCID _mseq; _mseq=MC2_nextOpLoad(MCID_NODEP); int seq = load_32(&_seq);
39 _fn1 = MC2_function(2, sizeof (c1), c1, _mold_seq, _mseq); MCID _br1;
41 _br1 = MC2_branchUsesID(_fn1, 1, 2, true);
43 MCID res_phi = MC2_loop_phi(_mres);
46 _br1 = MC2_branchUsesID(_fn1, 0, 2, true);
57 void seqlock_write(MCID _mnew_data, int new_data) {
60 MCID _mold_seq; _mold_seq=MC2_nextOpLoad(MCID_NODEP); int old_seq = load_32(&_seq);
61 MCID _fn2; int c2 = (old_seq % 2 == 1);
62 _fn2 = MC2_function(1, sizeof (c2), c2, _mold_seq);
65 _br2 = MC2_branchUsesID(_fn2, 1, 2, true);
69 MCID _fn3; _br2 = MC2_branchUsesID(_fn2, 0, 2, true);
70 int new_seq = old_seq + 1;
71 _fn3 = MC2_function(1, sizeof (new_seq), new_seq, _mold_seq);
72 MCID _rmw0 = MC2_nextRMW(MCID_NODEP, _mold_seq, _fn3);
73 int cas_value = rmw_32(CAS, &_seq, old_seq, new_seq);
74 MCID _fn4; int c3 = old_seq == cas_value;
75 _fn4 = MC2_function(2, sizeof (c3), c3, _mold_seq, _rmw0);
78 _br3 = MC2_branchUsesID(_fn4, 1, 2, true);
81 _br3 = MC2_branchUsesID(_fn4, 0, 2, true);
90 MC2_nextOpStore(MCID_NODEP, _mnew_data);
91 store_32(&_data, new_data);
93 MCID _rmw1 = MC2_nextRMW(MCID_NODEP, MCID_NODEP, MCID_NODEP);
94 rmw_32(ADD, &_seq, /*dummy */0, 1);
97 static void a(void *obj) {
98 seqlock_write(MCID_NODEP, 3);
101 static void b(void *obj) {
102 seqlock_write(MCID_NODEP, 2);
105 static void c(void *obj) {
106 int r1 = seqlock_read();
109 int user_main(int argc, char **argv) {
110 thrd_t t1; thrd_t t2; thrd_t t3;
113 thrd_create(&t1, (thrd_start_t)&a, NULL);
114 thrd_create(&t2, (thrd_start_t)&b, NULL);
115 thrd_create(&t3, (thrd_start_t)&c, NULL);