--- /dev/null
+#include <stdio.h>
+#include <threads.h>
+#include <stdatomic.h>
+
+#include "librace.h"
+#include "register.h"
+
+/** @DeclareState: int val;
+ @Initial: val = 0;
+ @Commutativity: LOAD <-> LOAD (true)
+ @Commutativity: STORE <-> LOAD (true)
+ @Commutativity: STORE <-> STORE (true)
+*/
+
+/** @Interface: LOAD
+ @PreCondition:
+ return HasItem(PREV, STATE(val) == RET);
+ @SideEffect: STATE(val) = RET;
+
+*/
+int Load(atomic_int *loc) {
+ return loc->load(memory_order_acquire);
+}
+
+/** @Interface: STORE
+ @SideEffect: STATE(val) = val;
+
+*/
+void Store(atomic_int *loc, int val) {
+ loc->store(val, memory_order_release);
+}
+
+static void a(void *obj)
+{
+ Store(&x, 1);
+ Store(&x, 2);
+}
+
+static void b(void *obj)
+{
+ Store(&x, 3);
+}
+
+static void c(void *obj)
+{
+ int r1 = Load(&x);
+ int r2 = Load(&x);
+}
+
+int user_main(int argc, char **argv)
+{
+ thrd_t t1, t2, t3;
+
+ /** @Entry */
+
+ thrd_create(&t1, (thrd_start_t)&a, NULL);
+ thrd_create(&t2, (thrd_start_t)&b, NULL);
+ thrd_create(&t3, (thrd_start_t)&c, NULL);
+
+ thrd_join(t1);
+ thrd_join(t2);
+ thrd_join(t3);
+
+ return 0;
+}