add another testcase for dekker-fences
[model-checker-benchmarks.git] / seqlock / seqlock.h
1 #include <stdatomic.h>
2 #include <threads.h>
3 #include "common.h"
4
5 typedef struct seqlock {
6         // Sequence for reader consistency check
7         atomic_int _seq;
8         // It needs to be atomic to avoid data races
9         atomic_int _data;
10
11         seqlock() {
12                 atomic_init(&_seq, 0);
13                 atomic_init(&_data, 0);
14         }
15
16         int read() {
17                 while (true) {
18                         int old_seq = _seq.load(memory_order_acquire); // acquire
19                         if (old_seq % 2 == 1) continue;
20
21                         int res = _data.load(memory_order_acquire); 
22                         if (_seq.load(memory_order_relaxed) == old_seq) { // relaxed
23                                 return res;
24                         }
25                 }
26         }
27         
28         void write(int new_data) {
29                 while (true) {
30                         // #1: either here or #2 must be acquire
31                         int old_seq = _seq.load(memory_order_acquire); // acquire
32                         // This might be a relaxed too
33                         if (old_seq % 2 == 1)
34                                 continue; // Retry
35
36                         // #2
37                         if (_seq.compare_exchange_strong(old_seq, old_seq + 1,
38                                 memory_order_relaxed, memory_order_relaxed)) 
39                                 break;
40                 }
41
42                 // Update the data
43                 _data.store(new_data, memory_order_release); // Can be relaxed
44
45                 _seq.fetch_add(1, memory_order_release); // release
46         }
47
48 } seqlock_t;