notes/register-example/register.cc.original

   1 #include <stdio.h>
   2 #include <threads.h>
   3 #include <stdatomic.h>
   4
   5 #include "librace.h"
   6 #include "register.h"
   7
   8 /**     @DeclareState: int val;
   9         @Initial: val = 0;
  10         @Commutativity: LOAD <-> LOAD (true)
  11         @Commutativity: STORE <-> LOAD (true)
  12         @Commutativity: STORE <-> STORE (true)
  13 */
  14
  15 /** @Interface: LOAD
  16         @PreCondition:
  17         return HasItem(PREV, STATE(val) == RET);
  18         @SideEffect: STATE(val) = RET;
  19
  20 */
  21 int Load(atomic_int *loc) {
  22         return loc->load(memory_order_acquire);
  23 }
  24
  25 /** @Interface: STORE
  26         @SideEffect: STATE(val) = val;
  27
  28 */
  29 void Store(atomic_int *loc, int val) {
  30         loc->store(val, memory_order_release);
  31 }
  32
  33 static void a(void *obj)
  34 {
  35         Store(&x, 1);
  36         Store(&x, 2);
  37 }
  38
  39 static void b(void *obj)
  40 {
  41         Store(&x, 3);
  42 }
  43
  44 static void c(void *obj)
  45 {
  46         int r1 = Load(&x);
  47         int r2 = Load(&x);
  48 }
  49
  50 int user_main(int argc, char **argv)
  51 {
  52         thrd_t t1, t2, t3;
  53
  54         /** @Entry */
  55
  56         thrd_create(&t1, (thrd_start_t)&a, NULL);
  57         thrd_create(&t2, (thrd_start_t)&b, NULL);
  58         thrd_create(&t3, (thrd_start_t)&c, NULL);
  59
  60         thrd_join(t1);
  61         thrd_join(t2);
  62         thrd_join(t3);
  63
  64         return 0;
  65 }