notes/register-example/register.cc

   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_WRAPPER__(atomic_int *loc) {
  22         return loc->load(memory_order_acquire);
  23 }
  24
  25 int Load(atomic_int *loc) {
  26         // Instrument with the INTERFACE_BEGIN annotation
  27         Method cur = _createInterfaceBeginAnnotation("LOAD");
  28         // Call the actual function
  29         int RET = Load_WRAPPER__(loc);
  30
  31         // Initialize the value struct
  32         LOAD *value = new LOAD;
  33         value->RET = RET;
  34         value->loc = loc;
  35
  36         // Store the value info into the current MethodCall
  37         cur->value = value;
  38
  39         // Return if there exists a return value
  40         return RET;
  41 }
  42
  43 /** @Interface: STORE
  44         @SideEffect: STATE(val) = val;
  45
  46 */
  47 void Store_WRAPPER__(atomic_int *loc, int val) {
  48         loc->store(val, memory_order_release);
  49 }
  50
  51 void Store(atomic_int *loc, int val) {
  52         // Instrument with the INTERFACE_BEGIN annotation
  53         Method cur = _createInterfaceBeginAnnotation("STORE");
  54         // Call the actual function
  55         Store_WRAPPER__(loc, val);
  56
  57         // Initialize the value struct
  58         STORE *value = new STORE;
  59         value->loc = loc;
  60         value->val = val;
  61
  62         // Store the value info into the current MethodCall
  63         cur->value = value;
  64 }
  65
  66 static void a(void *obj)
  67 {
  68         Store(&x, 1);
  69         Store(&x, 2);
  70 }
  71
  72 static void b(void *obj)
  73 {
  74         Store(&x, 3);
  75 }
  76
  77 static void c(void *obj)
  78 {
  79         int r1 = Load(&x);
  80         int r2 = Load(&x);
  81 }
  82
  83 int user_main(int argc, char **argv)
  84 {
  85         thrd_t t1, t2, t3;
  86
  87         /** @Entry */
  88         _createInitAnnotation();
  89
  90         thrd_create(&t1, (thrd_start_t)&a, NULL);
  91         thrd_create(&t2, (thrd_start_t)&b, NULL);
  92         thrd_create(&t3, (thrd_start_t)&c, NULL);
  93
  94         thrd_join(t1);
  95         thrd_join(t2);
  96         thrd_join(t3);
  97
  98         return 0;
  99 }