4 #include "libinterface.h"
5 #define PROBLEMSIZE 100
11 MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
13 MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
17 int seqlock_read(MCID * retval) {
19 MCID _mold_seq; _mold_seq=MC2_nextOpLoad(MCID_NODEP); int old_seq = load_32(&_seq);
23 int _cond0 = old_seq % 2 == 1;
24 MCID _cond0_m = MC2_function_id(1, 1, sizeof(_cond0), _cond0, _mold_seq);
26 _br0 = MC2_branchUsesID(_cond0_m, 1, 2, true);
30 _br0 = MC2_branchUsesID(_cond0_m, 0, 2, true);
31 _mres=MC2_nextOpLoad(MCID_NODEP), res = load_32(&_data);
32 MCID _mseq; _mseq=MC2_nextOpLoad(MCID_NODEP); int seq = load_32(&_seq);
38 int _cond1 = MC2_equals(_mseq, seq, _mold_seq, old_seq, &_cond1_m);
39 if (_cond1) {_br1 = MC2_branchUsesID(_cond1_m, 1, 2, true);
43 _br1 = MC2_branchUsesID(_cond1_m, 0, 2, true);
53 int seqlock_write(MCID _mnew_data, int new_data, MCID * retval) {
54 MCID _mold_seq; _mold_seq=MC2_nextOpLoad(MCID_NODEP); int old_seq = load_32(&_seq);
58 int _cond2 = old_seq % 2 == 1;
59 MCID _cond2_m = MC2_function_id(2, 1, sizeof(_cond2), _cond2, _mold_seq);
61 _br2 = MC2_branchUsesID(_cond2_m, 1, 2, true);
65 MCID _fn0; _br2 = MC2_branchUsesID(_cond2_m, 0, 2, true);
66 int new_seq = old_seq + 1;
67 _fn0 = MC2_function_id(3, 1, sizeof (new_seq), new_seq, _mold_seq);
68 MCID _rmw0 = MC2_nextRMW(MCID_NODEP, _mold_seq, _fn0);
69 int cas_value = rmw_32(CAS, &_seq, old_seq, new_seq);
74 int _cond3 = MC2_equals(_rmw0, cas_value, _mold_seq, old_seq, &_cond3_m);
76 _br3 = MC2_branchUsesID(_cond3_m, 1, 2, true);
77 MC2_nextOpStore(MCID_NODEP, _mnew_data);
78 store_32(&_data, new_data);
79 MCID _rmw1 = MC2_nextRMW(MCID_NODEP, MCID_NODEP, MCID_NODEP);
80 rmw_32(ADD, &_seq, /*dummy */0, 1);
84 _br3 = MC2_branchUsesID(_cond3_m, 0, 2, true);
94 static void a(void *obj) {
96 for (int i = 0; i < PROBLEMSIZE; i++)
102 static void b(void *obj) {
105 for (int i = 0; i < PROBLEMSIZE; i++)
107 r1 = seqlock_read(&_rv0);
112 static void c(void *obj) {
115 for (int i = 0; i < PROBLEMSIZE; i++)
117 r1 = seqlock_read(&_rv1);
122 int user_main(int argc, char **argv) {
123 thrd_t t1; thrd_t t2; thrd_t t3;
126 thrd_create(&t1, (thrd_start_t)&a, NULL);
127 thrd_create(&t2, (thrd_start_t)&b, NULL);
128 thrd_create(&t3, (thrd_start_t)&c, NULL);