5 #include "libinterface.h"
6 #define PROBLEMSIZE 100
12 MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
14 MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
18 int seqlock_read(MCID * retval) {
20 MCID _mold_seq; _mold_seq=MC2_nextOpLoad(MCID_NODEP); int old_seq = load_32(&_seq);
24 int _cond0 = old_seq % 2 == 1;
25 MCID _cond0_m = MC2_function_id(1, 1, sizeof(_cond0), _cond0, _mold_seq);
27 _br0 = MC2_branchUsesID(_cond0_m, 1, 2, true);
31 _br0 = MC2_branchUsesID(_cond0_m, 0, 2, true);
32 _mres=MC2_nextOpLoad(MCID_NODEP), res = load_32(&_data);
33 MCID _mseq; _mseq=MC2_nextOpLoad(MCID_NODEP); int seq = load_32(&_seq);
39 int _cond1 = MC2_equals(_mseq, seq, _mold_seq, old_seq, &_cond1_m);
40 if (_cond1) {_br1 = MC2_branchUsesID(_cond1_m, 1, 2, true);
44 _br1 = MC2_branchUsesID(_cond1_m, 0, 2, true);
54 int seqlock_write(MCID _mnew_data, int new_data, MCID * retval) {
55 MCID _mold_seq; _mold_seq=MC2_nextOpLoad(MCID_NODEP); int old_seq = load_32(&_seq);
59 int _cond2 = old_seq % 2 == 1;
60 MCID _cond2_m = MC2_function_id(2, 1, sizeof(_cond2), _cond2, _mold_seq);
62 _br2 = MC2_branchUsesID(_cond2_m, 1, 2, true);
66 MCID _fn0; _br2 = MC2_branchUsesID(_cond2_m, 0, 2, true);
67 int new_seq = old_seq + 1;
68 _fn0 = MC2_function_id(3, 1, sizeof (new_seq), new_seq, _mold_seq);
69 MCID _rmw0 = MC2_nextRMW(MCID_NODEP, _mold_seq, _fn0);
70 int cas_value = rmw_32(CAS, &_seq, old_seq, new_seq);
75 int _cond3 = MC2_equals(_rmw0, cas_value, _mold_seq, old_seq, &_cond3_m);
77 _br3 = MC2_branchUsesID(_cond3_m, 1, 2, true);
78 MC2_nextOpStore(MCID_NODEP, _mnew_data);
79 store_32(&_data, new_data);
80 MCID _rmw1 = MC2_nextRMW(MCID_NODEP, MCID_NODEP, MCID_NODEP);
81 rmw_32(ADD, &_seq, /*dummy */0, 1);
85 _br3 = MC2_branchUsesID(_cond3_m, 0, 2, true);
95 static void a(void *obj) {
97 for (int i = 0; i < PROBLEMSIZE; i++)
103 static void b(void *obj) {
106 for (int i = 0; i < PROBLEMSIZE; i++)
108 r1 = seqlock_read(&_rv0);
113 static void c(void *obj) {
116 for (int i = 0; i < PROBLEMSIZE; i++)
118 r1 = seqlock_read(&_rv1);
123 int user_main(int argc, char **argv) {
124 thrd_t t1; thrd_t t2; thrd_t t3;
127 thrd_create(&t1, (thrd_start_t)&a, NULL);
128 thrd_create(&t2, (thrd_start_t)&b, NULL);
129 thrd_create(&t3, (thrd_start_t)&c, NULL);