4 #include "libinterface.h"
6 // Sequence for reader consistency check
8 // It needs to be atomic to avoid data races
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); // acquire
24 int _cond30 = old_seq % 2 == 1;
25 MCID _cond30_m = MC2_function_id(31, 1, sizeof(_cond30), _cond30, _mold_seq);
27 _br30 = MC2_branchUsesID(_cond30_m, 1, 2, true);
31 _br30 = MC2_branchUsesID(_cond30_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 _cond31 = MC2_equals(_mseq, (uint64_t)seq, _mold_seq, (uint64_t)old_seq, &_cond31_m);
40 if (_cond31) {_br31 = MC2_branchUsesID(_cond31_m, 1, 2, true);
44 _br31 = MC2_branchUsesID(_cond31_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);
60 int _cond32 = old_seq % 2 == 1;
61 MCID _cond32_m = MC2_function_id(32, 1, sizeof(_cond32), _cond32, _mold_seq);
63 _br32 = MC2_branchUsesID(_cond32_m, 1, 2, true);
67 MCID _fn0; _br32 = MC2_branchUsesID(_cond32_m, 0, 2, true);
68 int new_seq = old_seq + 1;
69 _fn0 = MC2_function_id(33, 1, sizeof (new_seq), (uint64_t)new_seq, _mold_seq);
70 MCID _rmw0 = MC2_nextRMW(MCID_NODEP, _mold_seq, _fn0);
71 int cas_value = rmw_32(CAS, &_seq, old_seq, new_seq);
77 int _cond33 = MC2_equals(_rmw0, (uint64_t)cas_value, _mold_seq, (uint64_t)old_seq, &_cond33_m);
80 _br33 = MC2_branchUsesID(_cond33_m, 1, 2, true);
81 MC2_nextOpStore(MCID_NODEP, _mnew_data);
82 store_32(&_data, new_data);
83 MCID _rmw1 = MC2_nextRMW(MCID_NODEP, MCID_NODEP, MCID_NODEP);
84 rmw_32(ADD, &_seq, /* dummy */0, 1);
88 _br33 = MC2_branchUsesID(_cond33_m, 0, 2, true);
98 static void a(void *obj) {
101 for (int i = 0; i < PROBLEMSIZE; i++) {
103 q = seqlock_write(MCID_NODEP, 30, &_rv0);
110 static void b(void *obj) {
113 for (int i = 0; i < PROBLEMSIZE; i++) {
115 r1 = seqlock_read(&_rv1);
122 static void c(void *obj) {
125 for (int i = 0; i < PROBLEMSIZE; i++) {
127 r1 = seqlock_read(&_rv2);
134 int user_main(int argc, char **argv) {
135 thrd_t t1; thrd_t t2; thrd_t t3;
138 thrd_create(&t1, (thrd_start_t)&a, NULL);
139 thrd_create(&t2, (thrd_start_t)&b, NULL);
140 thrd_create(&t3, (thrd_start_t)&c, NULL);