5 #include "libinterface.h"
11 MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
13 MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
20 MCID _mold_seq; _mold_seq=MC2_nextOpLoad(MCID_NODEP); int old_seq = load_32(&_seq);
22 MCID _fn0; int c0 = (old_seq % 2 == 1);
23 _fn0 = MC2_function(1, sizeof (c0), c0, _mold_seq);
26 _br0 = MC2_branchUsesID(_fn0, 1, 2, true);
30 MCID _mres; _br0 = MC2_branchUsesID(_fn0, 0, 2, true);
31 _mres=MC2_nextOpLoad(MCID_NODEP); int res = load_32(&_data);
32 MCID _mseq; _mseq=MC2_nextOpLoad(MCID_NODEP); int seq = load_32(&_seq);
37 _fn1 = MC2_function(2, sizeof (c1), c1, _mold_seq, _mseq); MCID _br1;
39 _br1 = MC2_branchUsesID(_fn1, 1, 2, true);
41 MCID res_phi = MC2_loop_phi(_mres);
44 _br1 = MC2_branchUsesID(_fn1, 0, 2, true);
55 void seqlock_write(MCID _mnew_data, int new_data) {
58 MCID _mold_seq; _mold_seq=MC2_nextOpLoad(MCID_NODEP); int old_seq = load_32(&_seq);
59 MCID _fn2; int c2 = (old_seq % 2 == 1);
60 _fn2 = MC2_function(1, sizeof (c2), c2, _mold_seq);
63 _br2 = MC2_branchUsesID(_fn2, 1, 2, true);
67 MCID _fn3; _br2 = MC2_branchUsesID(_fn2, 0, 2, true);
68 int new_seq = old_seq + 1;
69 _fn3 = MC2_function(1, sizeof (new_seq), new_seq, _mold_seq);
70 MCID _rmw0 = MC2_nextRMW(MCID_NODEP, _mold_seq, _fn3);
71 int cas_value = rmw_32(CAS, &_seq, old_seq, new_seq);
72 MCID _fn4; int c3 = old_seq == cas_value;
73 _fn4 = MC2_function(2, sizeof (c3), c3, _mold_seq, _rmw0);
76 _br3 = MC2_branchUsesID(_fn4, 1, 2, true);
79 _br3 = MC2_branchUsesID(_fn4, 0, 2, true);
88 MC2_nextOpStore(MCID_NODEP, _mnew_data);
89 store_32(&_data, new_data);
91 MCID _rmw1 = MC2_nextRMW(MCID_NODEP, MCID_NODEP, MCID_NODEP);
92 rmw_32(ADD, &_seq, /*dummy */0, 1);
95 static void a(void *obj) {
96 seqlock_write(MCID_NODEP, 3);
99 static void b(void *obj) {
100 seqlock_write(MCID_NODEP, 2);
103 static void c(void *obj) {
104 int r1 = seqlock_read();
107 int user_main(int argc, char **argv) {
108 thrd_t t1; thrd_t t2; thrd_t t3;
111 thrd_create(&t1, (thrd_start_t)&a, NULL);
112 thrd_create(&t2, (thrd_start_t)&b, NULL);
113 thrd_create(&t3, (thrd_start_t)&c, NULL);