+++ /dev/null
-BASE := ..
-
-OBJECTS := $(patsubst %.c, %.o, $(wildcard *.c))
-OBJECTS += $(patsubst %.cc, %.o, $(wildcard *.cc))
-
-include $(BASE)/common.mk
-
-DIR := litmus
-include $(DIR)/Makefile
-
-DEPS := $(join $(addsuffix ., $(dir $(OBJECTS))), $(addsuffix .d, $(notdir $(OBJECTS))))
-
-CPPFLAGS += -I$(BASE) -I$(BASE)/include
-
-all: $(OBJECTS)
-
--include $(DEPS)
-
-%.o: %.c
- $(CC) -MMD -MF $(@D)/.$(@F).d -o $@ $< $(CPPFLAGS) -L$(BASE) -l$(LIB_NAME)
-
-%.o: %.cc
- $(CXX) -MMD -MF $(@D)/.$(@F).d -o $@ $< $(CPPFLAGS) -L$(BASE) -l$(LIB_NAME)
-
-clean::
- rm -f $(OBJECTS) $(DEPS)
+++ /dev/null
-/**
- * @file addr-satcycle.cc
- * @brief Address-based satisfaction cycle test
- *
- * This program has a peculiar behavior which is technically legal under the
- * current C++ memory model but which is a result of a type of satisfaction
- * cycle. We use this as justification for part of our modifications to the
- * memory model when proving our model-checker's correctness.
- */
-
-#include <atomic>
-#include <threads.h>
-#include <stdio.h>
-
-#include "model-assert.h"
-
-using namespace std;
-
-atomic_int x[2], idx, y;
-
-int r1, r2, r3; /* "local" variables */
-
-static void a(void *obj)
-{
- r1 = idx.load(memory_order_relaxed);
- x[r1].store(0, memory_order_relaxed);
-
- /* Key point: can we guarantee that &x[0] == &x[r1]? */
- r2 = x[0].load(memory_order_relaxed);
- y.store(r2);
-}
-
-static void b(void *obj)
-{
- r3 = y.load(memory_order_relaxed);
- idx.store(r3, memory_order_relaxed);
-}
-
-int user_main(int argc, char **argv)
-{
- thrd_t t1, t2;
-
- atomic_init(&x[0], 1);
- atomic_init(&idx, 0);
- atomic_init(&y, 0);
-
- printf("Main thread: creating 2 threads\n");
- thrd_create(&t1, (thrd_start_t)&a, NULL);
- thrd_create(&t2, (thrd_start_t)&b, NULL);
-
- thrd_join(t1);
- thrd_join(t2);
- printf("Main thread is finished\n");
-
- printf("r1 = %d\n", r1);
- printf("r2 = %d\n", r2);
- printf("r3 = %d\n", r3);
-
- /*
- * This condition should not be hit because it only occurs under a
- * satisfaction cycle
- */
- bool cycle = (r1 == 1 && r2 == 1 && r3 == 1);
- MODEL_ASSERT(!cycle);
-
- return 0;
-}
+++ /dev/null
-#include <stdio.h>
-
-#include "threads.h"
-#include "librace.h"
-#include "stdatomic2.h"
-#include <mutex.h>
-#include <condition_variable>
-
-cdsc::mutex * m;
-cdsc::condition_variable *v;
-int shareddata;
-
-static void a(void *obj)
-{
-
- m->lock();
- while(load_32(&shareddata)==0)
- v->wait(*m);
- m->unlock();
-
-}
-
-static void b(void *obj)
-{
- m->lock();
- store_32(&shareddata, (unsigned int) 1);
- v->notify_all();
- m->unlock();
-}
-
-int user_main(int argc, char **argv)
-{
- thrd_t t1, t2;
- store_32(&shareddata, (unsigned int) 0);
- m=new cdsc::mutex();
- v=new cdsc::condition_variable();
-
- thrd_create(&t1, (thrd_start_t)&a, NULL);
- thrd_create(&t2, (thrd_start_t)&b, NULL);
-
- thrd_join(t1);
- thrd_join(t2);
- return 0;
-}
+++ /dev/null
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#include "librace.h"
-
-atomic_int a;
-atomic_int b;
-
-static void r(void *obj)
-{
- int r1=atomic_load_explicit(&a, memory_order_relaxed);
- int r2=atomic_load_explicit(&a, memory_order_relaxed);
- if (r1==r2)
- atomic_store_explicit(&b, 2, memory_order_relaxed);
- printf("r1=%d\n",r1);
- printf("r2=%d\n",r2);
-}
-
-static void s(void *obj)
-{
- int r3=atomic_load_explicit(&b, memory_order_relaxed);
- atomic_store_explicit(&a, r3, memory_order_relaxed);
- printf("r3=%d\n",r3);
-}
-
-int user_main(int argc, char **argv)
-{
- thrd_t t1, t2;
-
- atomic_init(&a, 0);
- atomic_init(&b, 1);
-
- printf("Main thread: creating 2 threads\n");
- thrd_create(&t1, (thrd_start_t)&r, NULL);
- thrd_create(&t2, (thrd_start_t)&s, NULL);
-
- thrd_join(t1);
- thrd_join(t2);
- printf("Main thread is finished\n");
-
- return 0;
-}
+++ /dev/null
-#include <stdio.h>
-#include <threads.h>
-#include <mutex>
-
-#include "librace.h"
-
-std::mutex *x;
-std::mutex *y;
-uint32_t shared = 0;
-
-static void a(void *obj)
-{
- x->lock();
- y->lock();
- printf("shared = %u\n", load_32(&shared));
- y->unlock();
- x->unlock();
-}
-
-static void b(void *obj)
-{
- y->lock();
- x->lock();
- store_32(&shared, 16);
- printf("write shared = 16\n");
- x->unlock();
- y->unlock();
-}
-
-int user_main(int argc, char **argv)
-{
- thrd_t t1, t2;
-
- x = new std::mutex();
- y = new std::mutex();
-
- printf("Main thread: creating 2 threads\n");
- thrd_create(&t1, (thrd_start_t)&a, NULL);
- thrd_create(&t2, (thrd_start_t)&b, NULL);
-
- thrd_join(t1);
- thrd_join(t2);
- printf("Main thread is finished\n");
-
- return 0;
-}
+++ /dev/null
-/*
- * Try to read the same value as a future value twice.
- *
- * This test should be able to see r1 = r2 = 42. Currently, we never see that
- * (as of 2/21/13) because the r2 load won't have a potential future value of
- * 42 at the same time as r1, due to our scheduling (the loads for r1 and r2
- * must occur before the write of x = 42).
- *
- * Note that the atomic_int y is simply used to aid in forcing a particularly
- * interesting scheduling. It is superfluous.
- */
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#include "librace.h"
-
-atomic_int x;
-atomic_int y;
-
-static void a(void *obj)
-{
- int r1 = atomic_load_explicit(&x, memory_order_relaxed);
- int r2 = atomic_load_explicit(&x, memory_order_relaxed);
- printf("r1 = %d, r2 = %d\n", r1, r2);
-}
-
-static void b(void *obj)
-{
- atomic_store_explicit(&y, 43, memory_order_relaxed);
- atomic_store_explicit(&x, 42, memory_order_relaxed);
-}
-
-int user_main(int argc, char **argv)
-{
- thrd_t t1, t2;
-
- atomic_init(&x, 0);
- atomic_init(&y, 0);
-
- printf("Main thread: creating 2 threads\n");
- thrd_create(&t1, (thrd_start_t)&a, NULL);
- thrd_create(&t2, (thrd_start_t)&b, NULL);
-
- thrd_join(t1);
- thrd_join(t2);
- printf("Main thread is finished\n");
-
- return 0;
-}
+++ /dev/null
-/*
- * This test performs some relaxed, release, acquire opeations on a single
- * atomic variable. It can give some rough idea of release sequence support but
- * probably should be improved to give better information.
- *
- * This test tries to establish two release sequences, where we should always
- * either establish both or establish neither. (Note that this is only true for
- * a few executions of interest, where both load-acquire's read from the same
- * write.)
- */
-
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#include "librace.h"
-
-atomic_int x;
-int var = 0;
-
-static void a(void *obj)
-{
- store_32(&var, 1);
- atomic_store_explicit(&x, 1, memory_order_release);
- atomic_store_explicit(&x, 42, memory_order_relaxed);
-}
-
-static void b(void *obj)
-{
- int r = atomic_load_explicit(&x, memory_order_acquire);
- printf("r = %d\n", r);
- printf("load %d\n", load_32(&var));
-}
-
-static void c(void *obj)
-{
- atomic_store_explicit(&x, 2, memory_order_relaxed);
-}
-
-int user_main(int argc, char **argv)
-{
- thrd_t t1, t2, t3, t4;
-
- atomic_init(&x, 0);
-
- printf("Main thread: creating 4 threads\n");
- thrd_create(&t1, (thrd_start_t)&a, NULL);
- thrd_create(&t2, (thrd_start_t)&b, NULL);
- thrd_create(&t3, (thrd_start_t)&b, NULL);
- thrd_create(&t4, (thrd_start_t)&c, NULL);
-
- thrd_join(t1);
- thrd_join(t2);
- thrd_join(t3);
- thrd_join(t4);
- printf("Main thread is finished\n");
-
- return 0;
-}
+++ /dev/null
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#include "librace.h"
-
-atomic_int x;
-atomic_int y;
-
-static void a(void *obj)
-{
- atomic_store_explicit(&x, 1, memory_order_relaxed);
- atomic_store_explicit(&x, 2, memory_order_relaxed);
- atomic_thread_fence(memory_order_seq_cst);
- printf("Thread A reads: %d\n", atomic_load_explicit(&y, memory_order_relaxed));
-}
-
-static void b(void *obj)
-{
- atomic_store_explicit(&y, 1, memory_order_relaxed);
- atomic_store_explicit(&y, 2, memory_order_relaxed);
- atomic_thread_fence(memory_order_seq_cst);
- printf("Thread B reads: %d\n", atomic_load_explicit(&x, memory_order_relaxed));
-}
-
-int user_main(int argc, char **argv)
-{
- thrd_t t1, t2;
-
- atomic_init(&x, 0);
- atomic_init(&y, 0);
-
- printf("Main thread: creating 2 threads\n");
- thrd_create(&t1, (thrd_start_t)&a, NULL);
- thrd_create(&t2, (thrd_start_t)&b, NULL);
-
- thrd_join(t1);
- thrd_join(t2);
- printf("Main thread is finishing\n");
-
- return 0;
-}
+++ /dev/null
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#include "librace.h"
-#include "model-assert.h"
-
-atomic_int x;
-atomic_int y;
-
-static void a(void *obj)
-{
- atomic_store_explicit(&x, 1, memory_order_relaxed);
- atomic_thread_fence(memory_order_release);
- atomic_store_explicit(&x, 2, memory_order_relaxed);
-}
-
-static void b(void *obj)
-{
- int r1, r2;
- r1 = atomic_load_explicit(&x, memory_order_relaxed);
- atomic_thread_fence(memory_order_acquire);
- r2 = atomic_load_explicit(&x, memory_order_relaxed);
-
- printf("FENCES: r1 = %d, r2 = %d\n", r1, r2);
- if (r1 == 2)
- MODEL_ASSERT(r2 != 1);
-}
-
-int user_main(int argc, char **argv)
-{
- thrd_t t1, t2;
-
- atomic_init(&x, 0);
- atomic_init(&y, 0);
-
- printf("Main thread: creating 2 threads\n");
- thrd_create(&t1, (thrd_start_t)&a, NULL);
- thrd_create(&t2, (thrd_start_t)&b, NULL);
-
- thrd_join(t1);
- thrd_join(t2);
- printf("Main thread is finishing\n");
-
- return 0;
-}
+++ /dev/null
-#include <stdlib.h>
-#include <stdio.h>
-#include <threads.h>
-#include <atomic>
-
-#include "librace.h"
-#include "model-assert.h"
-
-using namespace std;
-
-atomic_int x, y;
-atomic_intptr_t z, z2;
-
-int r1, r2, r3; /* "local" variables */
-
-/**
- This example illustrates a self-satisfying cycle involving
- synchronization. A failed synchronization creates the store that
- causes the synchronization to fail.
-
- The C++11 memory model nominally allows r1=0, r2=1, r3=5.
-
- This example is insane, we don't support that behavior.
- */
-
-
-static void a(void *obj)
-{
- z.store((intptr_t)&y, memory_order_relaxed);
- r1 = y.fetch_add(1, memory_order_release);
- z.store((intptr_t)&x, memory_order_relaxed);
- r2 = y.fetch_add(1, memory_order_release);
-}
-
-
-static void b(void *obj)
-{
- r3 = y.fetch_add(1, memory_order_acquire);
- intptr_t ptr = z.load(memory_order_relaxed);
- z2.store(ptr, memory_order_relaxed);
-}
-
-static void c(void *obj)
-{
- atomic_int *ptr2 = (atomic_int *)z2.load(memory_order_relaxed);
- (*ptr2).store(5, memory_order_relaxed);
-}
-
-int user_main(int argc, char **argv)
-{
- thrd_t t1, t2, t3;
-
- atomic_init(&x, 0);
- atomic_init(&y, 0);
- atomic_init(&z, (intptr_t) &x);
- atomic_init(&z2, (intptr_t) &x);
-
- 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);
-
- printf("r1=%d, r2=%d, r3=%d\n", r1, r2, r3);
-
- return 0;
-}
+++ /dev/null
-/**
- * @file iriw.cc
- * @brief Independent read and independent write test
- */
-
-#include <atomic>
-#include <threads.h>
-#include <stdio.h>
-
-#include "wildcard.h"
-#include "model-assert.h"
-
-using namespace std;
-
-atomic_int x, y;
-int r1, r2, r3, r4; /* "local" variables */
-
-static void a(void *obj)
-{
- x.store(1, memory_order_seq_cst);
-}
-
-static void b(void *obj)
-{
- y.store(1, memory_order_seq_cst);
-}
-
-static void c(void *obj)
-{
- r1 = x.load(memory_order_acquire);
- r2 = y.load(memory_order_seq_cst);
-}
-
-static void d(void *obj)
-{
- r3 = y.load(memory_order_acquire);
- r4 = x.load(memory_order_seq_cst);
-}
-
-
-int user_main(int argc, char **argv)
-{
- thrd_t t1, t2, t3, t4;
-
- atomic_init(&x, 0);
- atomic_init(&y, 0);
-
- printf("Main thread: creating 4 threads\n");
- 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_create(&t4, (thrd_start_t)&d, NULL);
-
- thrd_join(t1);
- thrd_join(t2);
- thrd_join(t3);
- thrd_join(t4);
- printf("Main thread is finished\n");
-
- /*
- * This condition should not be hit if the execution is SC */
- bool sc = (r1 == 1 && r2 == 0 && r3 == 1 && r4 == 0);
- printf("r1 = %d, r2 = %d, r3 = %d and r4 = %d\n", r1, r2, r3, r4);
- MODEL_ASSERT(!sc);
- return 0;
-}
+++ /dev/null
-/**
- * @file iriw.cc
- * @brief Independent read and independent write test
- */
-
-#include <atomic>
-#include <threads.h>
-#include <stdio.h>
-
-#include "wildcard.h"
-#include "model-assert.h"
-
-using namespace std;
-
-atomic_int x, y;
-int r1, r2, r3, r4; /* "local" variables */
-
-static void a(void *obj)
-{
- x.store(1, wildcard(1));
-}
-
-static void b(void *obj)
-{
- y.store(1, wildcard(2));
-}
-
-static void c(void *obj)
-{
- r1 = x.load(wildcard(3));
- r2 = y.load(wildcard(4));
-}
-
-static void d(void *obj)
-{
- r3 = y.load(wildcard(5));
- r4 = x.load(wildcard(6));
-}
-
-
-int user_main(int argc, char **argv)
-{
- thrd_t t1, t2, t3, t4;
-
- atomic_init(&x, 0);
- atomic_init(&y, 0);
-
- printf("Main thread: creating 4 threads\n");
- 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_create(&t4, (thrd_start_t)&d, NULL);
-
- thrd_join(t1);
- thrd_join(t2);
- thrd_join(t3);
- thrd_join(t4);
- printf("Main thread is finished\n");
-
- /*
- * This condition should not be hit if the execution is SC */
- bool sc = (r1 == 1 && r2 == 0 && r3 == 1 && r4 == 0);
- //MODEL_ASSERT(!sc);
-
- return 0;
-}
+++ /dev/null
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#include "librace.h"
-
-#define RW_LOCK_BIAS 0x00100000
-#define WRITE_LOCK_CMP RW_LOCK_BIAS
-
-/** Example implementation of linux rw lock along with 2 thread test
- * driver... */
-
-typedef union {
- atomic_int lock;
-} rwlock_t;
-
-static inline int read_can_lock(rwlock_t *lock)
-{
- return atomic_load_explicit(&lock->lock, memory_order_relaxed) > 0;
-}
-
-static inline int write_can_lock(rwlock_t *lock)
-{
- return atomic_load_explicit(&lock->lock, memory_order_relaxed) == RW_LOCK_BIAS;
-}
-
-static inline void read_lock(rwlock_t *rw)
-{
- int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
- while (priorvalue <= 0) {
- atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
- do {
- priorvalue = atomic_load_explicit(&rw->lock, memory_order_relaxed);
- } while (priorvalue <= 0);
- priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
- }
-}
-
-static inline void write_lock(rwlock_t *rw)
-{
- int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
- while (priorvalue != RW_LOCK_BIAS) {
- atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
- do {
- priorvalue = atomic_load_explicit(&rw->lock, memory_order_relaxed);
- } while (priorvalue != RW_LOCK_BIAS);
- priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
- }
-}
-
-static inline int read_trylock(rwlock_t *rw)
-{
- int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
- if (priorvalue > 0)
- return 1;
-
- atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
- return 0;
-}
-
-static inline int write_trylock(rwlock_t *rw)
-{
- int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
- if (priorvalue == RW_LOCK_BIAS)
- return 1;
-
- atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
- return 0;
-}
-
-static inline void read_unlock(rwlock_t *rw)
-{
- atomic_fetch_add_explicit(&rw->lock, 1, memory_order_release);
-}
-
-static inline void write_unlock(rwlock_t *rw)
-{
- atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_release);
-}
-
-rwlock_t mylock;
-int shareddata;
-
-static void a(void *obj)
-{
- int i;
- for(i = 0;i < 2;i++) {
- if ((i % 2) == 0) {
- read_lock(&mylock);
- load_32(&shareddata);
- read_unlock(&mylock);
- } else {
- write_lock(&mylock);
- store_32(&shareddata,(unsigned int)i);
- write_unlock(&mylock);
- }
- }
-}
-
-int user_main(int argc, char **argv)
-{
- thrd_t t1, t2;
- atomic_init(&mylock.lock, RW_LOCK_BIAS);
-
- thrd_create(&t1, (thrd_start_t)&a, NULL);
- thrd_create(&t2, (thrd_start_t)&a, NULL);
-
- thrd_join(t1);
- thrd_join(t2);
-
- return 0;
-}
+++ /dev/null
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#include "librace.h"
-
-#define RW_LOCK_BIAS 0x00100000
-#define WRITE_LOCK_CMP RW_LOCK_BIAS
-
-/** Example implementation of linux rw lock along with 2 thread test
- * driver... */
-
-typedef union {
- atomic_int lock;
-} rwlock_t;
-
-static inline int read_can_lock(rwlock_t *lock)
-{
- return atomic_load_explicit(&lock->lock, memory_order_relaxed) > 0;
-}
-
-static inline int write_can_lock(rwlock_t *lock)
-{
- return atomic_load_explicit(&lock->lock, memory_order_relaxed) == RW_LOCK_BIAS;
-}
-
-static inline void read_lock(rwlock_t *rw)
-{
- int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
- while (priorvalue <= 0) {
- atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
- while (atomic_load_explicit(&rw->lock, memory_order_relaxed) <= 0) {
- thrd_yield();
- }
- priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
- }
-}
-
-static inline void write_lock(rwlock_t *rw)
-{
- int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
- while (priorvalue != RW_LOCK_BIAS) {
- atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
- while (atomic_load_explicit(&rw->lock, memory_order_relaxed) != RW_LOCK_BIAS) {
- thrd_yield();
- }
- priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
- }
-}
-
-static inline int read_trylock(rwlock_t *rw)
-{
- int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
- if (priorvalue > 0)
- return 1;
-
- atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
- return 0;
-}
-
-static inline int write_trylock(rwlock_t *rw)
-{
- int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
- if (priorvalue == RW_LOCK_BIAS)
- return 1;
-
- atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
- return 0;
-}
-
-static inline void read_unlock(rwlock_t *rw)
-{
- atomic_fetch_add_explicit(&rw->lock, 1, memory_order_release);
-}
-
-static inline void write_unlock(rwlock_t *rw)
-{
- atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_release);
-}
-
-rwlock_t mylock;
-int shareddata;
-
-static void a(void *obj)
-{
- int i;
- for(i = 0;i < 2;i++) {
- if ((i % 2) == 0) {
- read_lock(&mylock);
- load_32(&shareddata);
- read_unlock(&mylock);
- } else {
- write_lock(&mylock);
- store_32(&shareddata,(unsigned int)i);
- write_unlock(&mylock);
- }
- }
-}
-
-int user_main(int argc, char **argv)
-{
- thrd_t t1, t2;
- atomic_init(&mylock.lock, RW_LOCK_BIAS);
-
- thrd_create(&t1, (thrd_start_t)&a, NULL);
- thrd_create(&t2, (thrd_start_t)&a, NULL);
-
- thrd_join(t1);
- thrd_join(t2);
-
- return 0;
-}
+++ /dev/null
-D := $(DIR)
-
-OBJECTS += $(patsubst %.c, %.o, $(wildcard $(D)/*.c))
-OBJECTS += $(patsubst %.cc, %.o, $(wildcard $(D)/*.cc))
+++ /dev/null
-#include <stdio.h>
-#include <threads.h>
-#include <atomic>
-
-std::atomic_int x;
-std::atomic_int y;
-
-std::memory_order store_mo = std::memory_order_release;
-std::memory_order load_mo = std::memory_order_acquire;
-
-static void a(void *obj)
-{
- x.store(1, store_mo);
-}
-
-static void b(void *obj)
-{
- y.store(1, store_mo);
-}
-
-static void c(void *obj)
-{
- printf("x1: %d\n", x.load(load_mo));
- printf("y1: %d\n", y.load(load_mo));
-}
-
-static void d(void *obj)
-{
- printf("y2: %d\n", y.load(load_mo));
- printf("x2: %d\n", x.load(load_mo));
-}
-
-int user_main(int argc, char **argv)
-{
- thrd_t t1, t2, t3, t4;
-
- /* Command-line argument 's' enables seq_cst test */
- if (argc > 1 && *argv[1] == 's')
- store_mo = load_mo = std::memory_order_seq_cst;
-
- atomic_init(&x, 0);
- atomic_init(&y, 0);
-
- printf("Main thread: creating 4 threads\n");
- 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_create(&t4, (thrd_start_t)&d, NULL);
-
- thrd_join(t1);
- thrd_join(t2);
- thrd_join(t3);
- thrd_join(t4);
- printf("Main thread is finished\n");
-
- return 0;
-}
+++ /dev/null
-#include <stdio.h>
-#include <threads.h>
-#include <atomic>
-
-std::atomic_int x;
-std::atomic_int y;
-
-static void a(void *obj)
-{
- printf("x: %d\n", x.load(std::memory_order_relaxed));
- y.store(1, std::memory_order_relaxed);
-}
-
-static void b(void *obj)
-{
- printf("y: %d\n", y.load(std::memory_order_relaxed));
- x.store(1, std::memory_order_relaxed);
-}
-
-int user_main(int argc, char **argv)
-{
- thrd_t t1, t2;
-
- atomic_init(&x, 0);
- atomic_init(&y, 0);
-
- printf("Main thread: creating 2 threads\n");
- thrd_create(&t1, (thrd_start_t)&a, NULL);
- thrd_create(&t2, (thrd_start_t)&b, NULL);
-
- thrd_join(t1);
- thrd_join(t2);
- printf("Main thread is finished\n");
-
- return 0;
-}
+++ /dev/null
-#include <stdio.h>
-#include <threads.h>
-#include <atomic>
-
-std::atomic_int x;
-std::atomic_int y;
-
-static void a(void *obj)
-{
- x.store(1, std::memory_order_relaxed);
- y.store(1, std::memory_order_relaxed);
-}
-
-static void b(void *obj)
-{
- printf("y1: %d\n", y.load(std::memory_order_relaxed));
- printf("x1: %d\n", x.load(std::memory_order_relaxed));
-}
-
-static void c(void *obj)
-{
- printf("x2: %d\n", x.load(std::memory_order_relaxed));
- printf("y2: %d\n", y.load(std::memory_order_relaxed));
-}
-
-int user_main(int argc, char **argv)
-{
- thrd_t t1, t2, t3;
-
- atomic_init(&x, 0);
- atomic_init(&y, 0);
-
- printf("Main thread: creating 3 threads\n");
- 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);
- printf("Main thread is finished\n");
-
- return 0;
-}
+++ /dev/null
-#include <stdlib.h>
-#include <stdio.h>
-#include <threads.h>
-#include <atomic>
-
-#include "model-assert.h"
-
-/*
- * This 'seqlock' example should never trigger the MODEL_ASSERT() for
- * release/acquire; it may trigger the MODEL_ASSERT() for release/consume
- */
-
-std::atomic_int x;
-std::atomic_int y;
-std::atomic_int z;
-
-static int N = 1;
-
-static void a(void *obj)
-{
- for (int i = 0; i < N; i++) {
- x.store(2 * i + 1, std::memory_order_release);
- y.store(i + 1, std::memory_order_release);
- z.store(i + 1, std::memory_order_release);
- x.store(2 * i + 2, std::memory_order_release);
- }
-}
-
-static void b(void *obj)
-{
- int x1, y1, z1, x2;
- x1 = x.load(std::memory_order_acquire);
- y1 = y.load(std::memory_order_acquire);
- z1 = z.load(std::memory_order_acquire);
- x2 = x.load(std::memory_order_acquire);
- printf("x: %d\n", x1);
- printf("y: %d\n", y1);
- printf("z: %d\n", z1);
- printf("x: %d\n", x2);
-
- /* If x1 and x2 are the same, even value, then y1 must equal z1 */
- MODEL_ASSERT(x1 != x2 || x1 & 0x1 || y1 == z1);
-}
-
-int user_main(int argc, char **argv)
-{
- thrd_t t1, t2;
-
- if (argc > 1)
- N = atoi(argv[1]);
-
- printf("N: %d\n", N);
-
- atomic_init(&x, 0);
- atomic_init(&y, 0);
- atomic_init(&z, 0);
-
- printf("Main thread: creating 2 threads\n");
- thrd_create(&t1, (thrd_start_t)&a, NULL);
- thrd_create(&t2, (thrd_start_t)&b, NULL);
-
- thrd_join(t1);
- thrd_join(t2);
- printf("Main thread is finished\n");
-
- return 0;
-}
+++ /dev/null
-#include <stdio.h>
-#include <threads.h>
-#include <atomic>
-
-std::atomic_int x;
-std::atomic_int y;
-
-static void a(void *obj)
-{
- x.store(1, std::memory_order_relaxed);
- printf("y: %d\n", y.load(std::memory_order_relaxed));
-}
-
-static void b(void *obj)
-{
- y.store(1, std::memory_order_relaxed);
- printf("x: %d\n", x.load(std::memory_order_relaxed));
-}
-
-int user_main(int argc, char **argv)
-{
- thrd_t t1, t2;
-
- atomic_init(&x, 0);
- atomic_init(&y, 0);
-
- printf("Main thread: creating 2 threads\n");
- thrd_create(&t1, (thrd_start_t)&a, NULL);
- thrd_create(&t2, (thrd_start_t)&b, NULL);
-
- thrd_join(t1);
- thrd_join(t2);
- printf("Main thread is finished\n");
-
- return 0;
-}
+++ /dev/null
-#include <stdlib.h>
-#include <stdio.h>
-#include <threads.h>
-#include <atomic>
-
-static int N = 2;
-
-/* Can be tested for different behavior with relaxed vs. release/acquire/seq-cst */
-#define load_mo std::memory_order_relaxed
-#define store_mo std::memory_order_relaxed
-
-static std::atomic_int *x;
-
-static void a(void *obj)
-{
- int idx = *((int *)obj);
-
- if (idx > 0)
- x[idx - 1].load(load_mo);
-
- if (idx < N)
- x[idx].store(1, store_mo);
- else
- x[0].load(load_mo);
-}
-
-int user_main(int argc, char **argv)
-{
- thrd_t *threads;
- int *indexes;
-
- if (argc > 1)
- N = atoi(argv[1]);
- if (N < 2) {
- printf("Error: must have N >= 2\n");
- return 1;
- }
- printf("N: %d\n", N);
-
- threads = (thrd_t *)malloc((N + 1) * sizeof(thrd_t));
- x = (std::atomic_int *)malloc(N * sizeof(std::atomic_int));
- indexes = (int *)malloc((N + 1) * sizeof(int));
-
- for (int i = 0; i < N + 1; i++)
- indexes[i] = i;
-
- for (int i = 0; i < N; i++)
- atomic_init(&x[i], 0);
-
- for (int i = 0; i < N + 1; i++)
- thrd_create(&threads[i], (thrd_start_t)&a, (void *)&indexes[i]);
-
- for (int i = 0; i < N + 1; i++)
- thrd_join(threads[i]);
-
- return 0;
-}
+++ /dev/null
-#!/bin/sh
-
-clang -Xclang -load -Xclang /scratch/llvm/build/lib/libSkeletonPass.so -c -I/scratch/random-fuzzer/include/ /scratch/random-fuzzer/test/userprog.c
-
-gcc -o userprog userprog.o -L/scratch/random-fuzzer -lmodel
-
-#clang -Xclang -load -Xclang /scratch/llvm/build/lib/libSkeletonPass.so -c -I/scratch/random-fuzzer/include/ /scratch/random-fuzzer/test/double-read-fv.c
-
-#gcc -o double-read-fv double-read-fv.o -L/scratch/random-fuzzer -lmodel
-
-#clang -Xclang -load -Xclang /scratch/llvm/build/lib/libSkeletonPass.so -c -I/scratch/random-fuzzer/include/ /scratch/random-fuzzer/test/rmw2prog.c
-
-#gcc -o rmw2prog rmw2prog.o -L/scratch/random-fuzzer -lmodel
-
-#clang -Xclang -load -Xclang /scratch/llvm/build/lib/libSkeletonPass.so -c -I/scratch/random-fuzzer/include/ /scratch/random-fuzzer/test/fences.c
-
-#gcc -o fences fences.o -L/scratch/random-fuzzer -lmodel
-
-export LD_LIBRARY_PATH=/scratch/random-fuzzer
+++ /dev/null
-/**
- * @file mo-satcycle.cc
- * @brief MO satisfaction cycle test
- *
- * This program has a peculiar behavior which is technically legal under the
- * current C++ memory model but which is a result of a type of satisfaction
- * cycle. We use this as justification for part of our modifications to the
- * memory model when proving our model-checker's correctness.
- */
-
-#include <atomic>
-#include <threads.h>
-#include <stdio.h>
-
-#include "model-assert.h"
-
-using namespace std;
-
-atomic_int x, y;
-int r0, r1, r2, r3; /* "local" variables */
-
-static void a(void *obj)
-{
- y.store(10, memory_order_relaxed);
- x.store(1, memory_order_release);
-}
-
-static void b(void *obj)
-{
- r0 = x.load(memory_order_relaxed);
- r1 = x.load(memory_order_acquire);
- y.store(11, memory_order_relaxed);
-}
-
-static void c(void *obj)
-{
- r2 = y.load(memory_order_relaxed);
- r3 = y.load(memory_order_relaxed);
- if (r2 == 11 && r3 == 10)
- x.store(0, memory_order_relaxed);
-}
-
-int user_main(int argc, char **argv)
-{
- thrd_t t1, t2, t3;
-
- atomic_init(&x, 0);
- atomic_init(&y, 0);
-
- printf("Main thread: creating 3 threads\n");
- 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);
- printf("Main thread is finished\n");
-
- /*
- * This condition should not be hit because it only occurs under a
- * satisfaction cycle
- */
- bool cycle = (r0 == 1 && r1 == 0 && r2 == 11 && r3 == 10);
- MODEL_ASSERT(!cycle);
-
- return 0;
-}
+++ /dev/null
-#include <stdio.h>
-
-#include "threads.h"
-#include "librace.h"
-#include "stdatomic2.h"
-#include <mutex>
-std::mutex * m;
-int shareddata;
-
-static void a(void *obj)
-{
- int i;
- for(i=0;i<2;i++) {
- if ((i%2)==0) {
- m->lock();
- store_32(&shareddata,(unsigned int)i);
- m->unlock();
- } else {
- while(!m->try_lock())
- thrd_yield();
- store_32(&shareddata,(unsigned int)i);
- m->unlock();
- }
- }
-}
-
-int user_main(int argc, char **argv)
-{
- thrd_t t1, t2;
- m=new std::mutex();
-
- thrd_create(&t1, (thrd_start_t)&a, NULL);
- thrd_create(&t2, (thrd_start_t)&a, NULL);
-
- thrd_join(t1);
- thrd_join(t2);
- return 0;
-}
+++ /dev/null
-#include <stdlib.h>
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#include "librace.h"
-#include "model-assert.h"
-
-atomic_int x;
-atomic_int y;
-atomic_int z;
-static void a(void *obj)
-{
- (void)atomic_load_explicit(&z, memory_order_relaxed); // this is only for schedule control
- int t1=atomic_load_explicit(&x, memory_order_relaxed);
- atomic_store_explicit(&y, 1, memory_order_relaxed);
- printf("t1=%d\n",t1);
-}
-
-static void b(void *obj)
-{
- int t2=atomic_load_explicit(&y, memory_order_relaxed);
- atomic_store_explicit(&x, t2, memory_order_relaxed);
-}
-
-int user_main(int argc, char **argv)
-{
- thrd_t t1, t2;
-
-
- atomic_init(&x, 0);
- atomic_init(&y, 0);
- atomic_init(&z, 0);
- thrd_create(&t1, (thrd_start_t)&a, NULL);
- thrd_create(&t2, (thrd_start_t)&b, NULL);
-
- thrd_join(t1);
- thrd_join(t2);
-
-
- return 0;
-}
+++ /dev/null
-/*
- * This test performs some relaxes, release, acquire opeations on a single
- * atomic variable. It is designed for creating a difficult set of pending
- * release sequences to resolve at the end of an execution. However, it
- * utilizes 6 threads, so it blows up into a lot of executions quickly.
- */
-
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#include "librace.h"
-
-atomic_int x;
-int var = 0;
-
-static void a(void *obj)
-{
- store_32(&var, 1);
- atomic_store_explicit(&x, *((int *)obj), memory_order_release);
- atomic_store_explicit(&x, *((int *)obj) + 1, memory_order_relaxed);
-}
-
-static void b2(void *obj)
-{
- int r = atomic_load_explicit(&x, memory_order_acquire);
- printf("r = %d\n", r);
- store_32(&var, 3);
-}
-
-static void b1(void *obj)
-{
- thrd_t t3, t4;
- int i = 7;
- int r = atomic_load_explicit(&x, memory_order_acquire);
- printf("r = %d\n", r);
- store_32(&var, 2);
- thrd_create(&t3, (thrd_start_t)&a, &i);
- thrd_create(&t4, (thrd_start_t)&b2, NULL);
- thrd_join(t3);
- thrd_join(t4);
-}
-
-static void c(void *obj)
-{
- atomic_store_explicit(&x, 22, memory_order_relaxed);
-}
-
-int user_main(int argc, char **argv)
-{
- thrd_t t1, t2, t5;
- int i = 4;
-
- atomic_init(&x, 0);
-
- thrd_create(&t1, (thrd_start_t)&a, &i);
- thrd_create(&t2, (thrd_start_t)&b1, NULL);
- thrd_create(&t5, (thrd_start_t)&c, NULL);
-
- thrd_join(t1);
- thrd_join(t2);
- thrd_join(t5);
-
- return 0;
-}
+++ /dev/null
-/*
- * This test performs some relaxes, release, acquire opeations on a single
- * atomic variable. It can give some rough idea of release sequence support but
- * probably should be improved to give better information.
- */
-
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#include "librace.h"
-
-atomic_int x;
-int var = 0;
-
-static void a(void *obj)
-{
- store_32(&var, 1);
- atomic_store_explicit(&x, 1, memory_order_release);
- atomic_store_explicit(&x, 42, memory_order_relaxed);
-}
-
-static void b(void *obj)
-{
- int r = atomic_load_explicit(&x, memory_order_acquire);
- printf("r = %d\n", r);
- printf("load %d\n", load_32(&var));
-}
-
-static void c(void *obj)
-{
- atomic_store_explicit(&x, 2, memory_order_relaxed);
-}
-
-int user_main(int argc, char **argv)
-{
- thrd_t t1, t2, t3;
-
- atomic_init(&x, 0);
-
- printf("Main thread: creating 3 threads\n");
- 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);
- printf("Main thread is finished\n");
-
- return 0;
-}
+++ /dev/null
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#include "librace.h"
-
-atomic_short x;
-atomic_short y;
-
-static void a(void *obj)
-{
- short desire = 315;
- short expected = 0;
- short * pt = &expected;
-
- printf("expected was %d, but x is %d\n", expected, x);
-
- short v1 = atomic_compare_exchange_weak_explicit(&x, pt, desire, memory_order_relaxed, memory_order_acquire);
- printf("Then v1 = %d, x = %d\n", v1, x);
- printf("expected: %d\n", expected);
-/*
- short v1 = atomic_exchange_explicit(&x, 8, memory_order_relaxed);
- short v2 = atomic_exchange_explicit(&x, -10, memory_order_relaxed);
- short v3 = atomic_load_explicit(&x, memory_order_relaxed);
- printf("v1 = %d, v2 = %d, v3 = %d\n", v1, v2, v3);
- */
-}
-
-static void b(void *obj)
-{
- int v3=atomic_fetch_add_explicit(&y, 2, memory_order_relaxed);
- int v4=atomic_fetch_add_explicit(&x, -5, memory_order_relaxed);
- printf("v3 = %d, v4=%d\n", v3, v4);
-}
-
-int user_main(int argc, char **argv)
-{
- thrd_t t1, t2;
-
- atomic_init(&x, 0);
- atomic_init(&y, 0);
-
- thrd_create(&t1, (thrd_start_t)&a, NULL);
-// thrd_create(&t2, (thrd_start_t)&b, NULL);
-
- thrd_join(t1);
-// thrd_join(t2);
-
- return 0;
-}
+++ /dev/null
-#include <stdlib.h>
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#include "librace.h"
-#include "model-assert.h"
-
-atomic_int x;
-static int N = 2;
-
-static void a(void *obj)
-{
- int i;
- for (i = 0;i < N;i++)
- atomic_fetch_add_explicit(&x, 1, memory_order_relaxed);
-}
-
-int user_main(int argc, char **argv)
-{
- thrd_t t1, t2;
-
- if (argc > 1)
- N = atoi(argv[1]);
-
- atomic_init(&x, 0);
- thrd_create(&t1, (thrd_start_t)&a, NULL);
- thrd_create(&t2, (thrd_start_t)&a, NULL);
-
- thrd_join(t1);
- thrd_join(t2);
-
- MODEL_ASSERT(atomic_load(&x) == N * 2);
-
- return 0;
-}
+++ /dev/null
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#include "librace.h"
-
-atomic_int x;
-atomic_int y;
-atomic_int z;
-
-static int r1, r2, r3;
-
-static void a(void *obj)
-{
- atomic_store_explicit(&z, 1, memory_order_relaxed);
-}
-
-static void b(void *obj)
-{
- atomic_store_explicit(&x, 1, memory_order_relaxed);
- atomic_store_explicit(&y, 1, memory_order_relaxed);
- r1=atomic_load_explicit(&z, memory_order_relaxed);
-}
-static void c(void *obj)
-{
- atomic_store_explicit(&z, 2, memory_order_relaxed);
- atomic_store_explicit(&x, 2, memory_order_relaxed);
- r2=atomic_load_explicit(&y, memory_order_relaxed);
-}
-
-static void d(void *obj)
-{
- atomic_store_explicit(&z, 3, memory_order_relaxed);
- atomic_store_explicit(&y, 2, memory_order_relaxed);
- r3=atomic_load_explicit(&x, memory_order_relaxed);
-}
-
-int user_main(int argc, char **argv)
-{
- thrd_t t1, t2,t3, t4;
-
- atomic_init(&x, 0);
- atomic_init(&y, 0);
- atomic_init(&z, 0);
-
- 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_create(&t4, (thrd_start_t)&d, NULL);
-
- thrd_join(t1);
- thrd_join(t2);
- thrd_join(t3);
- thrd_join(t4);
-
- /* Check and/or print r1, r2, r3? */
-
- return 0;
-}
+++ /dev/null
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#include "librace.h"
-
-atomic_int x;
-atomic_int y;
-
-static void a(void *obj)
-{
- int r1=atomic_load_explicit(&x, memory_order_relaxed);
- atomic_store_explicit(&y, r1, memory_order_relaxed);
- printf("r1=%d\n",r1);
-}
-
-static void b(void *obj)
-{
- int r2=atomic_load_explicit(&y, memory_order_relaxed);
- atomic_store_explicit(&x, r2, memory_order_relaxed);
- atomic_store_explicit(&x, r2 + 1, memory_order_relaxed);
- printf("r2=%d\n",r2);
-}
-
-int user_main(int argc, char **argv)
-{
- thrd_t t1, t2;
-
- atomic_init(&x, -1);
- atomic_init(&y, 0);
-
- printf("Main thread: creating 2 threads\n");
- thrd_create(&t1, (thrd_start_t)&a, NULL);
- thrd_create(&t2, (thrd_start_t)&b, NULL);
-
- thrd_join(t1);
- thrd_join(t2);
- printf("Main thread is finished\n");
-
- return 0;
-}
+++ /dev/null
-/**
- * @file uninit.cc
- * @brief Uninitialized loads test
- *
- * This is a test of the "uninitialized loads" code. While we don't explicitly
- * initialize y, this example's synchronization pattern should guarantee we
- * never see it uninitialized.
- */
-#include <stdio.h>
-#include <threads.h>
-#include <atomic>
-
-#include "librace.h"
-
-std::atomic_int x;
-std::atomic_int y;
-
-static void a(void *obj)
-{
- int flag = x.load(std::memory_order_acquire);
- printf("flag: %d\n", flag);
- if (flag == 2)
- printf("Load: %d\n", y.load(std::memory_order_relaxed));
-}
-
-static void b(void *obj)
-{
- printf("fetch_add: %d\n", x.fetch_add(1, std::memory_order_relaxed));
-}
-
-static void c(void *obj)
-{
- y.store(3, std::memory_order_relaxed);
- x.store(1, std::memory_order_release);
-}
-
-int user_main(int argc, char **argv)
-{
- thrd_t t1, t2, t3;
-
- std::atomic_init(&x, 0);
-
- printf("Main thread: creating 3 threads\n");
- 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);
- printf("Main thread is finished\n");
-
- return 0;
-}
+++ /dev/null
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#include "librace.h"
-
-atomic_int x;
-atomic_int y;
-int z;
-
-static void a(void *obj)
-{
- int r1=atomic_load_explicit(&y, memory_order_relaxed);
- atomic_store_explicit(&x, r1, memory_order_relaxed);
-// z = 1;
- printf("r1=%d\n",r1);
-}
-
-static void b(void *obj)
-{
- int r2=atomic_load_explicit(&x, memory_order_relaxed);
- atomic_store_explicit(&y, 42, memory_order_relaxed);
-// z = 2;
- printf("r2=%d\n",r2);
-}
-
-int user_main(int argc, char **argv)
-{
- thrd_t t1, t2;
-
- atomic_init(&x, 30);
- atomic_init(&y, 0);
-
- printf("Main thread: creating 2 threads\n");
- thrd_create(&t1, (thrd_start_t)&a, NULL);
- thrd_create(&t2, (thrd_start_t)&b, NULL);
-
- thrd_join(t1);
- thrd_join(t2);
- printf("Main thread is finished\n");
-
- return 0;
-}
+++ /dev/null
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-#include "librace.h"
-atomic_int x1;
-atomic_int x2;
-atomic_int x3;
-atomic_int x4;
-atomic_int x5;
-atomic_int x6;
-atomic_int x7;
-static void a(void *obj)
-{
- atomic_store_explicit(&x1, 1,memory_order_relaxed);
-}
-
-static void b(void *obj)
-{
- (void)atomic_load_explicit(&x1, memory_order_relaxed);
- atomic_store_explicit(&x2, 1,memory_order_relaxed);
-}
-
-static void c(void *obj)
-{
- (void)atomic_load_explicit(&x2, memory_order_relaxed);
- atomic_store_explicit(&x3, 1,memory_order_relaxed);
-}
-
-static void d(void *obj)
-{
- (void)atomic_load_explicit(&x3, memory_order_relaxed);
- atomic_store_explicit(&x4, 1,memory_order_relaxed);
-}
-
-static void e(void *obj)
-{
- (void)atomic_load_explicit(&x4, memory_order_relaxed);
- atomic_store_explicit(&x5, 1,memory_order_relaxed);
-}
-
-static void f(void *obj)
-{
- (void)atomic_load_explicit(&x5, memory_order_relaxed);
- atomic_store_explicit(&x6, 1,memory_order_relaxed);
-}
-
-static void g(void *obj)
-{
- (void)atomic_load_explicit(&x6, memory_order_relaxed);
- atomic_store_explicit(&x7, 1,memory_order_relaxed);
-}
-static void h(void *obj)
-{
- (void)atomic_load_explicit(&x7, memory_order_relaxed);
- (void)atomic_load_explicit(&x1, memory_order_relaxed);
-}
-
-int user_main(int argc, char **argv)
-{
- thrd_t t1, t2, t3, t4, t5, t6, t7, t8;
- atomic_init(&x1, 0);
- atomic_init(&x2, 0);
- atomic_init(&x3, 0);
- atomic_init(&x4, 0);
- atomic_init(&x5, 0);
- atomic_init(&x6, 0);
- atomic_init(&x7, 0);
-
-
- 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_create(&t4, (thrd_start_t)&d, NULL);
- thrd_create(&t5, (thrd_start_t)&e, NULL);
- thrd_create(&t6, (thrd_start_t)&f, NULL);
- thrd_create(&t7, (thrd_start_t)&g, NULL);
- thrd_create(&t8, (thrd_start_t)&h, NULL);
-
- thrd_join(t1);
- thrd_join(t2);
- thrd_join(t3);
- thrd_join(t4);
- thrd_join(t5);
- thrd_join(t6);
- thrd_join(t7);
- thrd_join(t8);
-
- return 0;
-}
+++ /dev/null
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-#include "librace.h"
-atomic_int x1;
-atomic_int x2;
-atomic_int x3;
-atomic_int x4;
-atomic_int x5;
-atomic_int x6;
-atomic_int x7;
-static void a(void *obj)
-{
- atomic_store_explicit(&x1, 1,memory_order_seq_cst);
-}
-
-static void b(void *obj)
-{
- (void)atomic_load_explicit(&x1, memory_order_seq_cst);
- atomic_store_explicit(&x2, 1,memory_order_seq_cst);
-}
-
-static void c(void *obj)
-{
- (void)atomic_load_explicit(&x2, memory_order_seq_cst);
- atomic_store_explicit(&x3, 1,memory_order_seq_cst);
-}
-
-static void d(void *obj)
-{
- (void)atomic_load_explicit(&x3, memory_order_seq_cst);
- atomic_store_explicit(&x4, 1,memory_order_seq_cst);
-}
-
-static void e(void *obj)
-{
- (void)atomic_load_explicit(&x4, memory_order_seq_cst);
- atomic_store_explicit(&x5, 1,memory_order_seq_cst);
-}
-
-static void f(void *obj)
-{
- (void)atomic_load_explicit(&x5, memory_order_seq_cst);
- atomic_store_explicit(&x6, 1,memory_order_seq_cst);
-}
-
-static void g(void *obj)
-{
- (void)atomic_load_explicit(&x6, memory_order_seq_cst);
- atomic_store_explicit(&x7, 1,memory_order_seq_cst);
-}
-static void h(void *obj)
-{
- (void)atomic_load_explicit(&x7, memory_order_seq_cst);
- (void)atomic_load_explicit(&x1, memory_order_seq_cst);
-}
-
-int user_main(int argc, char **argv)
-{
- thrd_t t1, t2, t3, t4, t5, t6, t7, t8;
- atomic_init(&x1, 0);
- atomic_init(&x2, 0);
- atomic_init(&x3, 0);
- atomic_init(&x4, 0);
- atomic_init(&x5, 0);
- atomic_init(&x6, 0);
- atomic_init(&x7, 0);
-
-
- 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_create(&t4, (thrd_start_t)&d, NULL);
- thrd_create(&t5, (thrd_start_t)&e, NULL);
- thrd_create(&t6, (thrd_start_t)&f, NULL);
- thrd_create(&t7, (thrd_start_t)&g, NULL);
- thrd_create(&t8, (thrd_start_t)&h, NULL);
-
- thrd_join(t1);
- thrd_join(t2);
- thrd_join(t3);
- thrd_join(t4);
- thrd_join(t5);
- thrd_join(t6);
- thrd_join(t7);
- thrd_join(t8);
-
- return 0;
-}
return model->get_current_thread();
}
-#ifdef TLS
void modelexit() {
model->switch_to_master(new ModelAction(THREAD_FINISH, std::memory_order_seq_cst, thread_current()));
}
-#endif
void initMainThread() {
atexit(modelexit);
projects / c11tester.git / commitdiff