6 #include "model-assert.h"
9 * This 'seqlock' example should never trigger the MODEL_ASSERT() for
10 * release/acquire; it may trigger the MODEL_ASSERT() for release/consume
19 static void a(void *obj)
21 for (int i = 0; i < N; i++) {
22 x.store(2 * i + 1, std::memory_order_release);
23 y.store(i + 1, std::memory_order_release);
24 z.store(i + 1, std::memory_order_release);
25 x.store(2 * i + 2, std::memory_order_release);
29 static void b(void *obj)
32 x1 = x.load(std::memory_order_acquire);
33 y1 = y.load(std::memory_order_acquire);
34 z1 = z.load(std::memory_order_acquire);
35 x2 = x.load(std::memory_order_acquire);
36 printf("x: %d\n", x1);
37 printf("y: %d\n", y1);
38 printf("z: %d\n", z1);
39 printf("x: %d\n", x2);
41 /* If x1 and x2 are the same, even value, then y1 must equal z1 */
42 MODEL_ASSERT(x1 != x2 || x1 & 0x1 || y1 == z1);
45 int user_main(int argc, char **argv)
58 printf("Main thread: creating 2 threads\n");
59 thrd_create(&t1, (thrd_start_t)&a, NULL);
60 thrd_create(&t2, (thrd_start_t)&b, NULL);
64 printf("Main thread is finished\n");