5 #include "libinterface.h"
7 // Sequence for reader consistency check
9 // It needs to be atomic to avoid data races
10 /*atomic_*/ int _data;
13 MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
15 MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
19 int seqlock_read(MCID * retval) {
21 MCID _mold_seq; _mold_seq=MC2_nextOpLoad(MCID_NODEP); int old_seq = load_32(&_seq); // acquire
25 int _cond30 = old_seq % 2 == 1;
26 MCID _cond30_m = MC2_function_id(31, 1, sizeof(_cond30), _cond30, _mold_seq);
28 _br30 = MC2_branchUsesID(_cond30_m, 1, 2, true);
32 _br30 = MC2_branchUsesID(_cond30_m, 0, 2, true);
33 _mres=MC2_nextOpLoad(MCID_NODEP), res = load_32(&_data);
34 MCID _mseq; _mseq=MC2_nextOpLoad(MCID_NODEP); int seq = load_32(&_seq);
40 int _cond31 = MC2_equals(_mseq, (uint64_t)seq, _mold_seq, (uint64_t)old_seq, &_cond31_m);
41 if (_cond31) {_br31 = MC2_branchUsesID(_cond31_m, 1, 2, true);
45 _br31 = MC2_branchUsesID(_cond31_m, 0, 2, true);
55 int seqlock_write(MCID _mnew_data, int new_data, MCID * retval) {
56 MCID _mold_seq; _mold_seq=MC2_nextOpLoad(MCID_NODEP); int old_seq = load_32(&_seq);
61 int _cond32 = old_seq % 2 == 1;
62 MCID _cond32_m = MC2_function_id(32, 1, sizeof(_cond32), _cond32, _mold_seq);
64 _br32 = MC2_branchUsesID(_cond32_m, 1, 2, true);
68 MCID _fn0; _br32 = MC2_branchUsesID(_cond32_m, 0, 2, true);
69 int new_seq = old_seq + 1;
70 _fn0 = MC2_function_id(33, 1, sizeof (new_seq), (uint64_t)new_seq, _mold_seq);
71 MCID _rmw0 = MC2_nextRMW(MCID_NODEP, _mold_seq, _fn0);
72 int cas_value = rmw_32(CAS, &_seq, old_seq, new_seq);
78 int _cond33 = MC2_equals(_rmw0, (uint64_t)cas_value, _mold_seq, (uint64_t)old_seq, &_cond33_m);
81 _br33 = MC2_branchUsesID(_cond33_m, 1, 2, true);
82 MC2_nextOpStore(MCID_NODEP, _mnew_data);
83 store_32(&_data, new_data);
84 MCID _rmw1 = MC2_nextRMW(MCID_NODEP, MCID_NODEP, MCID_NODEP);
85 rmw_32(ADD, &_seq, /* dummy */0, 1);
89 _br33 = MC2_branchUsesID(_cond33_m, 0, 2, true);
99 static void a(void *obj) {
102 for (int i = 0; i < PROBLEMSIZE; i++) {
104 q = seqlock_write(MCID_NODEP, 30, &_rv0);
111 static void b(void *obj) {
114 for (int i = 0; i < PROBLEMSIZE; i++) {
116 r1 = seqlock_read(&_rv1);
123 static void c(void *obj) {
126 for (int i = 0; i < PROBLEMSIZE; i++) {
128 r1 = seqlock_read(&_rv2);
135 int user_main(int argc, char **argv) {
136 thrd_t t1; thrd_t t2; thrd_t t3;
139 thrd_create(&t1, (thrd_start_t)&a, NULL);
140 thrd_create(&t2, (thrd_start_t)&b, NULL);
141 thrd_create(&t3, (thrd_start_t)&c, NULL);