include common.mk
OBJECTS := libthreads.o schedule.o model.o threads.o librace.o action.o \
- clockvector.o main.o snapshot-interface.o cyclegraph.o \
+ clockvector.o main.o cyclegraph.o \
datarace.o impatomic.o cmodelint.o \
snapshot.o malloc.o mymemory.o common.o mutex.o conditionvariable.o \
context.o execution.o libannotate.o plugins.o pthread.o futex.o fuzzer.o \
/** Snapshotting configurables */
-/**
- * If USE_MPROTECT_SNAPSHOT=2, then snapshot by tuned mmap() algorithm
- * If USE_MPROTECT_SNAPSHOT=1, then snapshot by using mmap() and mprotect()
- * If USE_MPROTECT_SNAPSHOT=0, then snapshot by using fork() */
-#define USE_MPROTECT_SNAPSHOT 0
-
/** Size of signal stack */
#define SIGSTACKSIZE 65536
add_thread(model_thread);
fuzzer->register_engine(m->get_history(), this);
scheduler->register_engine(this);
+#ifdef TLS
+ pthread_key_create(&pthreadkey, tlsdestructor);
+#endif
}
/** @brief Destructor */
void setFinished() {isfinished = true;}
void restore_last_seq_num();
-
+#ifdef TLS
+ pthread_key_t getPthreadKey() {return pthreadkey;}
+#endif
SNAPSHOTALLOC
private:
+#ifdef TLS
+ pthread_key_t pthreadkey;
+#endif
int get_execution_number() const;
ModelChecker *model;
params->uninitvalue = 0;
params->maxexecutions = 10;
params->nofork = false;
- params->threadsnocleanup = false;
}
-static void print_usage(const char *program_name, struct model_params *params)
+static void print_usage(struct model_params *params)
{
ModelVector<TraceAnalysis *> * registeredanalysis=getRegisteredTraceAnalysis();
/* Reset defaults before printing */
"Distributed under the GPLv2\n"
"Written by Brian Norris and Brian Demsky\n"
"\n"
- "Usage: %s [MODEL-CHECKER OPTIONS] -- [PROGRAM ARGS]\n"
+ "Usage: C11TESTER=[MODEL-CHECKER OPTIONS]\n"
"\n"
"MODEL-CHECKER OPTIONS can be any of the model-checker options listed below. Arguments\n"
"provided after the `--' (the PROGRAM ARGS) are passed to the user program.\n"
"-x, --maxexec=NUM Maximum number of executions.\n"
" Default: %u\n"
" -o help for a list of options\n"
- "-n No fork\n"
-#ifdef TLS
- "-d Don't allow threads to cleanup\n"
-#endif
- " -- Program arguments follow.\n\n",
- program_name,
+ "-n No fork\n\n",
params->verbose,
params->uninitvalue,
params->maxexecutions);
return true;
}
-static void parse_options(struct model_params *params, int argc, char **argv)
-{
- const char *shortopts = "hdnt:o:u:x:v::";
+void parse_options(struct model_params *params) {
+ const char *shortopts = "hnt:o:u:x:v::";
const struct option longopts[] = {
{"help", no_argument, NULL, 'h'},
{"verbose", optional_argument, NULL, 'v'},
{0, 0, 0, 0} /* Terminator */
};
int opt, longindex;
+ int tmpoptind = optind;
bool error = false;
+ char * options = getenv("C11TESTER");
+
+ if (options == NULL)
+ return;
+ int argc = 1;
+ int index;
+ for(index = 0;options[index]!=0;index++) {
+ if (options[index] == ' ')
+ argc++;
+ }
+ argc++; //first parameter is executable name
+ char optcpy[index + 1];
+ memcpy(optcpy, options, index+1);
+ char * argv[argc + 1];
+ argv[0] = NULL;
+ argv[1] = optcpy;
+ int count = 2;
+ for(index = 0;optcpy[index]!=0;index++) {
+ if (optcpy[index] == ' ') {
+ argv[count++] = &optcpy[index+1];
+ optcpy[index] = 0;
+ }
+ }
+
while (!error && (opt = getopt_long(argc, argv, shortopts, longopts, &longindex)) != -1) {
switch (opt) {
case 'h':
- print_usage(argv[0], params);
- break;
- case 'd':
- params->threadsnocleanup = true;
+ print_usage(params);
break;
case 'n':
params->nofork = true;
}
}
- /* Pass remaining arguments to user program */
- params->argc = argc - (optind - 1);
- params->argv = argv + (optind - 1);
-
- /* Reset program name */
- params->argv[0] = argv[0];
-
- /* Reset (global) optind for potential use by user program */
- optind = 1;
+ /* Restore (global) optind for potential use by user program */
+ optind = tmpoptind;
if (error)
- print_usage(argv[0], params);
+ print_usage(params);
}
-int main_argc;
-char **main_argv;
-
-static void install_trace_analyses(ModelExecution *execution)
-{
+void install_trace_analyses(ModelExecution *execution) {
ModelVector<TraceAnalysis *> * installedanalysis=getInstalledTraceAnalysis();
for(unsigned int i=0;i<installedanalysis->size();i++) {
TraceAnalysis * ta=(*installedanalysis)[i];
ta->actionAtInstallation();
}
}
-
-/**
- * Main function. Just initializes snapshotting library and the
- * snapshotting library calls the model_main function.
- */
-int main(int argc, char **argv)
-{
- main_argc = argc;
- main_argv = argv;
-
- /*
- * If this printf statement is removed, C11Tester will fail on an
- * assert on some versions of glibc. The first time printf is
- * called, it allocated internal buffers. We can't easily snapshot
- * libc since we also use it.
- */
-
- printf("C11Tester\n"
- "Copyright (c) 2013 and 2019 Regents of the University of California. All rights reserved.\n"
- "Distributed under the GPLv2\n"
- "Written by Weiyu Luo, Brian Norris, and Brian Demsky\n\n");
-
-
- //Initialize snapshotting library and model checker object
- if (!model) {
- snapshot_system_init(10000, 1024, 1024, 40000);
- model = new ModelChecker();
- model->startChecker();
- }
-
- /* Configure output redirection for the model-checker */
- redirect_output();
-
- register_plugins();
-
- //Parse command line options
- model_params *params = model->getParams();
- parse_options(params, main_argc, main_argv);
-
-
- install_trace_analyses(model->get_execution());
-
- model->startMainThread();
- DEBUG("Exiting\n");
-}
#include "history.h"
#include "bugmessage.h"
#include "params.h"
+#include "plugins.h"
ModelChecker *model = NULL;
-/** Wrapper to run the user's main function, with appropriate arguments */
-void user_main_wrapper(void *)
-{
- user_main(model->params.argc, model->params.argv);
+void placeholder(void *) {
+ ASSERT(0);
}
/** @brief Constructor */
trace_analyses(),
inspect_plugin(NULL)
{
+ model_print("C11Tester\n"
+ "Copyright (c) 2013 and 2019 Regents of the University of California. All rights reserved.\n"
+ "Distributed under the GPLv2\n"
+ "Written by Weiyu Luo, Brian Norris, and Brian Demsky\n\n");
memset(&stats,0,sizeof(struct execution_stats));
- init_thread = new Thread(execution->get_next_id(), (thrd_t *) model_malloc(sizeof(thrd_t)), &user_main_wrapper, NULL, NULL);
+ init_thread = new Thread(execution->get_next_id(), (thrd_t *) model_malloc(sizeof(thrd_t)), &placeholder, NULL, NULL);
#ifdef TLS
init_thread->setTLS((char *)get_tls_addr());
#endif
execution->add_thread(init_thread);
scheduler->set_current_thread(init_thread);
+ register_plugins();
execution->setParams(¶ms);
param_defaults(¶ms);
+ parse_options(¶ms);
initRaceDetector();
+ /* Configure output redirection for the model-checker */
+ redirect_output();
+ install_trace_analyses(get_execution());
}
/** @brief Destructor */
for (unsigned int i = 0;i < get_num_threads();i++)
delete get_thread(int_to_id(i))->get_pending();
- snapshot_backtrack_before(0);
+ snapshot_roll_back(snapshot);
}
/** @return the number of user threads created during this execution */
void ModelChecker::startChecker() {
startExecution(get_system_context(), runChecker);
- snapshot_stack_init();
- snapshot_record(0);
+ snapshot = take_snapshot();
+ initMainThread();
}
bool ModelChecker::should_terminate_execution()
execution_number = 1;
}
-void ModelChecker::startMainThread() {
- init_thread->set_state(THREAD_RUNNING);
- scheduler->set_current_thread(init_thread);
- main_thread_startup();
-}
-
/** @brief Run ModelChecker for the user program */
void ModelChecker::run()
{
#include "context.h"
#include "params.h"
#include "classlist.h"
+#include "snapshot-interface.h"
typedef SnapList<ModelAction *> action_list_t;
model_params params;
void add_trace_analysis(TraceAnalysis *a) { trace_analyses.push_back(a); }
void set_inspect_plugin(TraceAnalysis *a) { inspect_plugin=a; }
- void startMainThread();
void startChecker();
Thread * getInitThread() {return init_thread;}
Scheduler * getScheduler() {return scheduler;}
/** Flag indicates whether to restart the model checker. */
bool restart_flag;
+ /** Snapshot id we return to restart. */
+ snapshot_id snapshot;
+
/** The scheduler to use: tracks the running/ready Threads */
Scheduler * const scheduler;
ModelHistory * history;
void print_bugs() const;
void print_execution(bool printbugs) const;
void print_stats() const;
-
- friend void user_main_wrapper();
};
extern ModelChecker *model;
+void parse_options(struct model_params *params);
+void install_trace_analyses(ModelExecution *execution);
+
#endif /* __MODEL_H__ */
size_t allocatedReqs[REQUESTS_BEFORE_ALLOC] = { 0 };
int nextRequest = 0;
int howManyFreed = 0;
-#if !USE_MPROTECT_SNAPSHOT
static mspace sStaticSpace = NULL;
-#endif
/** Non-snapshotting calloc for our use. */
void *model_calloc(size_t count, size_t size)
{
-#if USE_MPROTECT_SNAPSHOT
- static void *(*callocp)(size_t count, size_t size) = NULL;
- char *error;
- void *ptr;
-
- /* get address of libc malloc */
- if (!callocp) {
- callocp = (void * (*)(size_t, size_t))dlsym(RTLD_NEXT, "calloc");
- if ((error = dlerror()) != NULL) {
- fputs(error, stderr);
- exit(EXIT_FAILURE);
- }
- }
- ptr = callocp(count, size);
- return ptr;
-#else
if (!sStaticSpace)
sStaticSpace = create_shared_mspace();
return mspace_calloc(sStaticSpace, count, size);
-#endif
}
/** Non-snapshotting malloc for our use. */
void *model_malloc(size_t size)
{
-#if USE_MPROTECT_SNAPSHOT
- static void *(*mallocp)(size_t size) = NULL;
- char *error;
- void *ptr;
-
- /* get address of libc malloc */
- if (!mallocp) {
- mallocp = (void * (*)(size_t))dlsym(RTLD_NEXT, "malloc");
- if ((error = dlerror()) != NULL) {
- fputs(error, stderr);
- exit(EXIT_FAILURE);
- }
- }
- ptr = mallocp(size);
- return ptr;
-#else
if (!sStaticSpace)
sStaticSpace = create_shared_mspace();
return mspace_malloc(sStaticSpace, size);
-#endif
}
/** Non-snapshotting malloc for our use. */
void *model_realloc(void *ptr, size_t size)
{
-#if USE_MPROTECT_SNAPSHOT
- static void *(*reallocp)(void *ptr, size_t size) = NULL;
- char *error;
- void *newptr;
-
- /* get address of libc malloc */
- if (!reallocp) {
- reallocp = (void * (*)(size_t))dlsym(RTLD_NEXT, "realloc");
- if ((error = dlerror()) != NULL) {
- fputs(error, stderr);
- exit(EXIT_FAILURE);
- }
- }
- newptr = reallocp(ptr, size);
- return newptr;
-#else
if (!sStaticSpace)
sStaticSpace = create_shared_mspace();
return mspace_realloc(sStaticSpace, ptr, size);
-#endif
}
/** @brief Snapshotting malloc, for use by model-checker (not user progs) */
/** Non-snapshotting free for our use. */
void model_free(void *ptr)
{
-#if USE_MPROTECT_SNAPSHOT
- static void (*freep)(void *);
- char *error;
-
- /* get address of libc free */
- if (!freep) {
- freep = (void (*)(void *))dlsym(RTLD_NEXT, "free");
- if ((error = dlerror()) != NULL) {
- fputs(error, stderr);
- exit(EXIT_FAILURE);
- }
- }
- freep(ptr);
-#else
mspace_free(sStaticSpace, ptr);
-#endif
}
/** Bootstrap allocation. Problem is that the dynamic linker calls require
/** @brief Global mspace reference for the model-checker's snapshotting heap */
mspace model_snapshot_space = NULL;
-#if USE_MPROTECT_SNAPSHOT
-
-/** @brief Global mspace reference for the user's snapshotting heap */
-mspace user_snapshot_space = NULL;
-
-/** Check whether this is bootstrapped memory that we should not free */
-static bool DontFree(void *ptr)
-{
- return (ptr >= (&bootstrapmemory[0]) && ptr < (&bootstrapmemory[BOOTSTRAPBYTES]));
-}
-
-/**
- * @brief The allocator function for "user" allocation
- *
- * Should only be used for allocations which will not disturb the allocation
- * patterns of a user thread.
- */
-static void * user_malloc(size_t size)
-{
- void *tmp = mspace_malloc(user_snapshot_space, size);
- ASSERT(tmp);
- return tmp;
-}
-
-/**
- * @brief Snapshotting malloc implementation for user programs
- *
- * Do NOT call this function from a model-checker context. Doing so may disrupt
- * the allocation patterns of a user thread.
- */
-void *malloc(size_t size)
-{
- void *tmp;
- if (user_snapshot_space) {
- /* Only perform user allocations from user context */
- ASSERT(!model || thread_current());
- tmp = user_malloc(size);
- } else
- tmp = HandleEarlyAllocationRequest(size);
- recordCalloc(tmp, size);
- return tmp;
-}
-
-/** @brief Snapshotting free implementation for user programs */
-void free(void * ptr)
-{
- if (!DontFree(ptr)) {
- mspace_free(user_snapshot_space, ptr);
- }
-}
-
-/** @brief Snapshotting realloc implementation for user programs */
-void *realloc(void *ptr, size_t size)
-{
- void *tmp = mspace_realloc(user_snapshot_space, ptr, size);
- recordCalloc(tmp, size);
- ASSERT(tmp);
- return tmp;
-}
-
-/** @brief Snapshotting calloc implementation for user programs */
-void * calloc(size_t num, size_t size)
-{
- if (user_snapshot_space) {
- void *tmp = mspace_calloc(user_snapshot_space, num, size);
- ASSERT(tmp);
- recordAlloc(tmp, num*size);
- return tmp;
- } else {
- void *tmp = HandleEarlyAllocationRequest(size * num);
- memset(tmp, 0, size * num);
- recordAlloc(tmp, num*size);
- return tmp;
- }
-}
-
-/** @brief Snapshotting allocation function for use by the Thread class only */
-void * Thread_malloc(size_t size)
-{
- return user_malloc(size);
-}
-
-/** @brief Snapshotting free function for use by the Thread class only */
-void Thread_free(void *ptr)
-{
- free(ptr);
-}
-
-/** @brief Snapshotting new operator for user programs */
-void * operator new(size_t size) throw(std::bad_alloc)
-{
- return malloc(size);
-}
-
-/** @brief Snapshotting delete operator for user programs */
-void operator delete(void *p) throw()
-{
- free(p);
-}
-
-/** @brief Snapshotting new[] operator for user programs */
-void * operator new[](size_t size) throw(std::bad_alloc)
-{
- return malloc(size);
-}
-
-/** @brief Snapshotting delete[] operator for user programs */
-void operator delete[](void *p, size_t size)
-{
- free(p);
-}
-
-#else /* !USE_MPROTECT_SNAPSHOT */
-
/** @brief Snapshotting allocation function for use by the Thread class only */
void * Thread_malloc(size_t size)
{
{
snapshot_free(ptr);
}
-
-#endif /* !USE_MPROTECT_SNAPSHOT */
extern mspace create_mspace_with_base(void* base, size_t capacity, int locked);
extern mspace create_mspace(size_t capacity, int locked);
-#if USE_MPROTECT_SNAPSHOT
-extern mspace user_snapshot_space;
-#endif
-
extern mspace model_snapshot_space;
#ifdef __cplusplus
unsigned int uninitvalue;
int maxexecutions;
bool nofork;
- bool threadsnocleanup;
/** @brief Verbosity (0 = quiet; 1 = noisy; 2 = noisier) */
int verbose;
-
- /** @brief Command-line argument count to pass to user program */
- int argc;
-
- /** @brief Command-line arguments to pass to user program */
- char **argv;
};
void param_defaults(struct model_params *params);
+++ /dev/null
-#include <stdlib.h>
-#include <unistd.h>
-#include <cstring>
-#include <inttypes.h>
-
-#include "snapshot-interface.h"
-#include "snapshot.h"
-#include "common.h"
-#include "mymemory.h"
-#include "stl-model.h"
-
-/* MYBINARYNAME only works because our pathname usually includes 'model' (e.g.,
- * /.../model-checker/test/userprog.o) */
-#define MYBINARYNAME "model"
-#define MAPFILE "/proc/self/maps"
-
-struct snapshot_entry {
- snapshot_entry(snapshot_id id, int idx) : snapshotid(id), index(idx) { }
- snapshot_id snapshotid;
- int index;
- MEMALLOC
-};
-
-class SnapshotStack {
-public:
- int backTrackBeforeStep(int seq_index);
- void snapshotStep(int seq_index);
-
- MEMALLOC
-private:
- ModelVector<struct snapshot_entry> stack;
-};
-
-static SnapshotStack *snap_stack;
-
-#ifdef MAC
-/** The SnapshotGlobalSegments function computes the memory regions
- * that may contain globals and then configures the snapshotting
- * library to snapshot them.
- */
-static void SnapshotGlobalSegments()
-{
- int pid = getpid();
- char buf[9000], execname[100];
- FILE *map;
-
- sprintf(execname, "vmmap -interleaved %d", pid);
- map = popen(execname, "r");
-
- if (!map) {
- perror("popen");
- exit(EXIT_FAILURE);
- }
-
- /* Wait for correct part */
- while (fgets(buf, sizeof(buf), map)) {
- if (strstr(buf, "==== regions for process"))
- break;
- }
-
- while (fgets(buf, sizeof(buf), map)) {
- char regionname[200] = "";
- char type[23];
- char smstr[23];
- char r, w, x;
- char mr, mw, mx;
- void *begin, *end;
-
- //Skip out at the end of the section
- if (buf[0] == '\n')
- break;
-
- sscanf(buf, "%22s %p-%p", type, &begin, &end);
-
- char * secondpart = strstr(buf, "]");
-
- sscanf(&secondpart[2], "%c%c%c/%c%c%c SM=%3s %200s\n", &r, &w, &x, &mr, &mw, &mx, smstr, regionname);
- if (w == 'w' && strstr(regionname, MYBINARYNAME)) {
- size_t len = ((uintptr_t)end - (uintptr_t)begin) / PAGESIZE;
- if (len != 0)
- snapshot_add_memory_region(begin, len);
- }
- }
- pclose(map);
-}
-#else
-
-static void get_binary_name(char *buf, size_t len)
-{
- ssize_t size = readlink("/proc/self/exe", buf, len);
- if (size < 0) {
- perror("readlink");
- exit(EXIT_FAILURE);
- }
-
- /* Terminate string */
- if ((size_t)size > len)
- size = len;
- buf[size] = '\0';
-}
-
-/** The SnapshotGlobalSegments function computes the memory regions
- * that may contain globals and then configures the snapshotting
- * library to snapshot them.
- */
-static void SnapshotGlobalSegments()
-{
- char buf[9000];
- char binary_name[800];
- FILE *map;
-
- map = fopen(MAPFILE, "r");
- if (!map) {
- perror("fopen");
- exit(EXIT_FAILURE);
- }
- get_binary_name(binary_name, sizeof(binary_name));
- while (fgets(buf, sizeof(buf), map)) {
- char regionname[200] = "";
- char r, w, x, p;
- void *begin, *end;
-
- sscanf(buf, "%p-%p %c%c%c%c %*x %*x:%*x %*u %200s\n", &begin, &end, &r, &w, &x, &p, regionname);
- if (w == 'w' && strstr(regionname, binary_name)) {
- size_t len = ((uintptr_t)end - (uintptr_t)begin) / PAGESIZE;
- if (len != 0)
- snapshot_add_memory_region(begin, len);
- DEBUG("%55s: %18p - %18p\t%c%c%c%c\n", regionname, begin, end, r, w, x, p);
- }
- }
- fclose(map);
-}
-#endif
-
-/** This method returns to the last snapshot before the inputted
- * sequence number. This function must be called from the model
- * checking thread and not from a snapshotted stack.
- * @param seqindex is the sequence number to rollback before.
- * @return is the sequence number we actually rolled back to.
- */
-int SnapshotStack::backTrackBeforeStep(int seqindex)
-{
- int i;
- for (i = (int)stack.size() - 1;i >= 0;i++)
- if (stack[i].index <= seqindex)
- break;
- else
- stack.pop_back();
-
- ASSERT(i >= 0);
- snapshot_roll_back(stack[i].snapshotid);
- return stack[i].index;
-}
-
-/** This method takes a snapshot at the given sequence number. */
-void SnapshotStack::snapshotStep(int seqindex)
-{
- stack.push_back(snapshot_entry(take_snapshot(), seqindex));
-}
-
-void snapshot_stack_init()
-{
- snap_stack = new SnapshotStack();
- SnapshotGlobalSegments();
-}
-
-void snapshot_record(int seq_index)
-{
- snap_stack->snapshotStep(seq_index);
-}
-
-int snapshot_backtrack_before(int seq_index)
-{
- return snap_stack->backTrackBeforeStep(seq_index);
-}
unsigned int numsnapshots, unsigned int nummemoryregions,
unsigned int numheappages);
void startExecution(ucontext_t * context, VoidFuncPtr entryPoint);
-void snapshot_stack_init();
-void snapshot_record(int seq_index);
-int snapshot_backtrack_before(int seq_index);
+snapshot_id take_snapshot();
+void snapshot_roll_back(snapshot_id theSnapShot);
+
#endif
#include "model.h"
-#if USE_MPROTECT_SNAPSHOT
-
-/** PageAlignedAdressUpdate return a page aligned address for the
- * address being added as a side effect the numBytes are also changed.
- */
-static void * PageAlignAddressUpward(void *addr)
-{
- return (void *)((((uintptr_t)addr) + PAGESIZE - 1) & ~(PAGESIZE - 1));
-}
-
-/* Each SnapShotRecord lists the firstbackingpage that must be written to
- * revert to that snapshot */
-struct SnapShotRecord {
- unsigned int firstBackingPage;
-};
-
-/** @brief Backing store page */
-typedef unsigned char snapshot_page_t[PAGESIZE];
-
-/* List the base address of the corresponding page in the backing store so we
- * know where to copy it to */
-struct BackingPageRecord {
- void *basePtrOfPage;
-};
-
-/* Struct for each memory region */
-struct MemoryRegion {
- void *basePtr; // base of memory region
- int sizeInPages; // size of memory region in pages
-};
-
-/** ReturnPageAlignedAddress returns a page aligned address for the
- * address being added as a side effect the numBytes are also changed.
- */
-static void * ReturnPageAlignedAddress(void *addr)
-{
- return (void *)(((uintptr_t)addr) & ~(PAGESIZE - 1));
-}
-
-/* Primary struct for snapshotting system */
-struct mprot_snapshotter {
- mprot_snapshotter(unsigned int numbackingpages, unsigned int numsnapshots, unsigned int nummemoryregions);
- ~mprot_snapshotter();
-
- struct MemoryRegion *regionsToSnapShot; //This pointer references an array of memory regions to snapshot
- snapshot_page_t *backingStore; //This pointer references an array of snapshotpage's that form the backing store
- void *backingStoreBasePtr; //This pointer references an array of snapshotpage's that form the backing store
- struct BackingPageRecord *backingRecords; //This pointer references an array of backingpagerecord's (same number of elements as backingstore
- struct SnapShotRecord *snapShots; //This pointer references the snapshot array
-
- unsigned int lastSnapShot; //Stores the next snapshot record we should use
- unsigned int lastBackingPage; //Stores the next backingpage we should use
- unsigned int lastRegion; //Stores the next memory region to be used
-
- unsigned int maxRegions; //Stores the max number of memory regions we support
- unsigned int maxBackingPages; //Stores the total number of backing pages
- unsigned int maxSnapShots; //Stores the total number of snapshots we allow
-
- MEMALLOC
-};
-
-static struct mprot_snapshotter *mprot_snap = NULL;
-
-mprot_snapshotter::mprot_snapshotter(unsigned int backing_pages, unsigned int snapshots, unsigned int regions) :
- lastSnapShot(0),
- lastBackingPage(0),
- lastRegion(0),
- maxRegions(regions),
- maxBackingPages(backing_pages),
- maxSnapShots(snapshots)
-{
- regionsToSnapShot = (struct MemoryRegion *)model_malloc(sizeof(struct MemoryRegion) * regions);
- backingStoreBasePtr = (void *)model_malloc(sizeof(snapshot_page_t) * (backing_pages + 1));
- //Page align the backingstorepages
- backingStore = (snapshot_page_t *)PageAlignAddressUpward(backingStoreBasePtr);
- backingRecords = (struct BackingPageRecord *)model_malloc(sizeof(struct BackingPageRecord) * backing_pages);
- snapShots = (struct SnapShotRecord *)model_malloc(sizeof(struct SnapShotRecord) * snapshots);
-}
-
-mprot_snapshotter::~mprot_snapshotter()
-{
- model_free(regionsToSnapShot);
- model_free(backingStoreBasePtr);
- model_free(backingRecords);
- model_free(snapShots);
-}
-
-/** mprot_handle_pf is the page fault handler for mprotect based snapshotting
- * algorithm.
- */
-static void mprot_handle_pf(int sig, siginfo_t *si, void *unused)
-{
- if (si->si_code == SEGV_MAPERR) {
- model_print("Segmentation fault at %p\n", si->si_addr);
- model_print("For debugging, place breakpoint at: %s:%d\n",
- __FILE__, __LINE__);
- // print_trace(); // Trace printing may cause dynamic memory allocation
- exit(EXIT_FAILURE);
- }
- void* addr = ReturnPageAlignedAddress(si->si_addr);
-
- unsigned int backingpage = mprot_snap->lastBackingPage++; //Could run out of pages...
- if (backingpage == mprot_snap->maxBackingPages) {
- model_print("Out of backing pages at %p\n", si->si_addr);
- exit(EXIT_FAILURE);
- }
-
- //copy page
- memcpy(&(mprot_snap->backingStore[backingpage]), addr, sizeof(snapshot_page_t));
- //remember where to copy page back to
- mprot_snap->backingRecords[backingpage].basePtrOfPage = addr;
- //set protection to read/write
- if (mprotect(addr, sizeof(snapshot_page_t), PROT_READ | PROT_WRITE)) {
- perror("mprotect");
- // Handle error by quitting?
- }
-}
-
-static void mprot_snapshot_init(unsigned int numbackingpages,
- unsigned int numsnapshots, unsigned int nummemoryregions,
- unsigned int numheappages)
-{
- /* Setup a stack for our signal handler.... */
- stack_t ss;
- ss.ss_sp = PageAlignAddressUpward(model_malloc(SIGSTACKSIZE + PAGESIZE - 1));
- ss.ss_size = SIGSTACKSIZE;
- ss.ss_flags = 0;
- sigaltstack(&ss, NULL);
-
- struct sigaction sa;
- sa.sa_flags = SA_SIGINFO | SA_NODEFER | SA_RESTART | SA_ONSTACK;
- sigemptyset(&sa.sa_mask);
- sa.sa_sigaction = mprot_handle_pf;
-#ifdef MAC
- if (sigaction(SIGBUS, &sa, NULL) == -1) {
- perror("sigaction(SIGBUS)");
- exit(EXIT_FAILURE);
- }
-#endif
- if (sigaction(SIGSEGV, &sa, NULL) == -1) {
- perror("sigaction(SIGSEGV)");
- exit(EXIT_FAILURE);
- }
-
- mprot_snap = new mprot_snapshotter(numbackingpages, numsnapshots, nummemoryregions);
-
- // EVIL HACK: We need to make sure that calls into the mprot_handle_pf method don't cause dynamic links
- // The problem is that we end up protecting state in the dynamic linker...
- // Solution is to call our signal handler before we start protecting stuff...
-
- siginfo_t si;
- memset(&si, 0, sizeof(si));
- si.si_addr = ss.ss_sp;
- mprot_handle_pf(SIGSEGV, &si, NULL);
- mprot_snap->lastBackingPage--; //remove the fake page we copied
-
- void *basemySpace = model_malloc((numheappages + 1) * PAGESIZE);
- void *pagealignedbase = PageAlignAddressUpward(basemySpace);
- user_snapshot_space = create_mspace_with_base(pagealignedbase, numheappages * PAGESIZE, 1);
- snapshot_add_memory_region(pagealignedbase, numheappages);
-
- void *base_model_snapshot_space = model_malloc((numheappages + 1) * PAGESIZE);
- pagealignedbase = PageAlignAddressUpward(base_model_snapshot_space);
- model_snapshot_space = create_mspace_with_base(pagealignedbase, numheappages * PAGESIZE, 1);
- snapshot_add_memory_region(pagealignedbase, numheappages);
-}
-
-static void mprot_startExecution(ucontext_t * context, VoidFuncPtr entryPoint) {
- /* setup the shared-stack context */
- create_context(context, fork_snap->mStackBase, model_calloc(STACK_SIZE_DEFAULT, 1), STACK_SIZE_DEFAULT, entryPoint);
-}
-
-static void mprot_add_to_snapshot(void *addr, unsigned int numPages)
-{
- unsigned int memoryregion = mprot_snap->lastRegion++;
- if (memoryregion == mprot_snap->maxRegions) {
- model_print("Exceeded supported number of memory regions!\n");
- exit(EXIT_FAILURE);
- }
-
- DEBUG("snapshot region %p-%p (%u page%s)\n",
- addr, (char *)addr + numPages * PAGESIZE, numPages,
- numPages > 1 ? "s" : "");
- mprot_snap->regionsToSnapShot[memoryregion].basePtr = addr;
- mprot_snap->regionsToSnapShot[memoryregion].sizeInPages = numPages;
-}
-
-static snapshot_id mprot_take_snapshot()
-{
- for (unsigned int region = 0;region < mprot_snap->lastRegion;region++) {
- if (mprotect(mprot_snap->regionsToSnapShot[region].basePtr, mprot_snap->regionsToSnapShot[region].sizeInPages * sizeof(snapshot_page_t), PROT_READ) == -1) {
- perror("mprotect");
- model_print("Failed to mprotect inside of takeSnapShot\n");
- exit(EXIT_FAILURE);
- }
- }
- unsigned int snapshot = mprot_snap->lastSnapShot++;
- if (snapshot == mprot_snap->maxSnapShots) {
- model_print("Out of snapshots\n");
- exit(EXIT_FAILURE);
- }
- mprot_snap->snapShots[snapshot].firstBackingPage = mprot_snap->lastBackingPage;
-
- return snapshot;
-}
-
-static void mprot_roll_back(snapshot_id theID)
-{
-#if USE_MPROTECT_SNAPSHOT == 2
- if (mprot_snap->lastSnapShot == (theID + 1)) {
- for (unsigned int page = mprot_snap->snapShots[theID].firstBackingPage;page < mprot_snap->lastBackingPage;page++) {
- memcpy(mprot_snap->backingRecords[page].basePtrOfPage, &mprot_snap->backingStore[page], sizeof(snapshot_page_t));
- }
- return;
- }
-#endif
-
- HashTable< void *, bool, uintptr_t, 4, model_malloc, model_calloc, model_free> duplicateMap;
- for (unsigned int region = 0;region < mprot_snap->lastRegion;region++) {
- if (mprotect(mprot_snap->regionsToSnapShot[region].basePtr, mprot_snap->regionsToSnapShot[region].sizeInPages * sizeof(snapshot_page_t), PROT_READ | PROT_WRITE) == -1) {
- perror("mprotect");
- model_print("Failed to mprotect inside of takeSnapShot\n");
- exit(EXIT_FAILURE);
- }
- }
- for (unsigned int page = mprot_snap->snapShots[theID].firstBackingPage;page < mprot_snap->lastBackingPage;page++) {
- if (!duplicateMap.contains(mprot_snap->backingRecords[page].basePtrOfPage)) {
- duplicateMap.put(mprot_snap->backingRecords[page].basePtrOfPage, true);
- memcpy(mprot_snap->backingRecords[page].basePtrOfPage, &mprot_snap->backingStore[page], sizeof(snapshot_page_t));
- }
- }
- mprot_snap->lastSnapShot = theID;
- mprot_snap->lastBackingPage = mprot_snap->snapShots[theID].firstBackingPage;
- mprot_take_snapshot(); //Make sure current snapshot is still good...All later ones are cleared
-}
-
-#else /* !USE_MPROTECT_SNAPSHOT */
-
#define SHARED_MEMORY_DEFAULT (200 * ((size_t)1 << 20)) // 100mb for the shared memory
#define STACK_SIZE_DEFAULT (((size_t)1 << 20) * 20) // 20 mb out of the above 100 mb for my stack
fork_snap->mIDToRollback = -1;
}
-#endif /* !USE_MPROTECT_SNAPSHOT */
-
/**
* @brief Initializes the snapshot system
* @param entryPoint the function that should run the program.
unsigned int numsnapshots, unsigned int nummemoryregions,
unsigned int numheappages)
{
-#if USE_MPROTECT_SNAPSHOT
- mprot_snapshot_init(numbackingpages, numsnapshots, nummemoryregions, numheappages);
-#else
fork_snapshot_init(numbackingpages, numsnapshots, nummemoryregions, numheappages);
-#endif
}
void startExecution(ucontext_t *context, VoidFuncPtr entryPoint)
{
-#if USE_MPROTECT_SNAPSHOT
- mprot_startExecution(context, entryPoint);
-#else
fork_startExecution(context, entryPoint);
-#endif
-}
-
-/** Assumes that addr is page aligned. */
-void snapshot_add_memory_region(void *addr, unsigned int numPages)
-{
-#if USE_MPROTECT_SNAPSHOT
- mprot_add_to_snapshot(addr, numPages);
-#else
- /* not needed for fork-based snapshotting */
-#endif
}
/** Takes a snapshot of memory.
*/
snapshot_id take_snapshot()
{
-#if USE_MPROTECT_SNAPSHOT
- return mprot_take_snapshot();
-#else
return fork_take_snapshot();
-#endif
}
/** Rolls the memory state back to the given snapshot identifier.
*/
void snapshot_roll_back(snapshot_id theID)
{
-#if USE_MPROTECT_SNAPSHOT
- mprot_roll_back(theID);
-#else
fork_roll_back(theID);
-#endif
}
#include "config.h"
#include "mymemory.h"
-void snapshot_add_memory_region(void *ptr, unsigned int numPages);
-snapshot_id take_snapshot();
-void snapshot_roll_back(snapshot_id theSnapShot);
-
-#if !USE_MPROTECT_SNAPSHOT
mspace create_shared_mspace();
-#endif
#endif
+++ /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;
-}
ucontext_t context;
void *stack;
#ifdef TLS
+ void * helper_stack;
public:
char *tls;
ucontext_t helpercontext;
#ifdef TLS
uintptr_t get_tls_addr();
+void tlsdestructor(void *v);
#endif
Thread * thread_current();
void thread_startup();
-void main_thread_startup();
+void initMainThread();
static inline thread_id_t thrd_to_id(thrd_t t)
{
return model->get_current_thread();
}
-void main_thread_startup() {
-#ifdef TLS
+void modelexit() {
+ model->switch_to_master(new ModelAction(THREAD_FINISH, std::memory_order_seq_cst, thread_current()));
+}
+
+void initMainThread() {
+ atexit(modelexit);
Thread * curr_thread = thread_current();
- /* Add dummy "start" action, just to create a first clock vector */
model->switch_to_master(new ModelAction(THREAD_START, std::memory_order_seq_cst, curr_thread));
-#endif
- thread_startup();
}
/**
void *retval = curr_thread->pstart_routine(curr_thread->arg);
curr_thread->set_pthread_return(retval);
}
+#ifndef TLS
/* Finish thread properly */
model->switch_to_master(new ModelAction(THREAD_FINISH, std::memory_order_seq_cst, curr_thread));
+#endif
}
static int (*pthread_mutex_init_p)(pthread_mutex_t *__mutex, const pthread_mutexattr_t *__mutexattr) = NULL;
}
if (!pthread_exit_p) {
- pthread_exit_p = (void (*)(void *))dlsym(RTLD_NEXT, "pthread_exit");
+ *((void (**)(void *)) &pthread_exit_p) = (void (*)(void *))dlsym(RTLD_NEXT, "pthread_exit");
if ((error = dlerror()) != NULL) {
fputs(error, stderr);
exit(EXIT_FAILURE);
int ret = getcontext(&curr_thread->helpercontext);
ASSERT(!ret);
+ //Setup destructor
+ if (pthread_setspecific(model->get_execution()->getPthreadKey(), (const void *)4)) {
+ printf("Destructor setup failed\n");
+ exit(-1);
+ }
+
+
/* Initialize new managed context */
- void *helperstack = stack_allocate(STACK_SIZE);
- curr_thread->helpercontext.uc_stack.ss_sp = helperstack;
+ curr_thread->helper_stack = stack_allocate(STACK_SIZE);
+ curr_thread->helpercontext.uc_stack.ss_sp = curr_thread->helper_stack;
curr_thread->helpercontext.uc_stack.ss_size = STACK_SIZE;
curr_thread->helpercontext.uc_stack.ss_flags = 0;
curr_thread->helpercontext.uc_link = model->get_system_context();
model_swapcontext(&curr_thread->context, &curr_thread->helpercontext);
+
//start the real thread
thread_startup();
- //now the real thread has control again
- stack_free(helperstack);
-
return NULL;
}
+#ifdef TLS
+void tlsdestructor(void *v) {
+ uintptr_t count = (uintptr_t) v;
+ if (count > 1) {
+ if (pthread_setspecific(model->get_execution()->getPthreadKey(), (const void *)(count - 1))) {
+ printf("Destructor setup failed\n");
+ exit(-1);
+ }
+ return;
+ }
+ /* Finish thread properly */
+ model->switch_to_master(new ModelAction(THREAD_FINISH, std::memory_order_seq_cst, thread_current()));
+}
+#endif
+
void setup_context() {
Thread * curr_thread = thread_current();
context.uc_stack.ss_flags = 0;
context.uc_link = model->get_system_context();
#ifdef TLS
- if (model != NULL)
- makecontext(&context, setup_context, 0);
- else
- makecontext(&context, main_thread_startup, 0);
+ makecontext(&context, setup_context, 0);
#else
makecontext(&context, thread_startup, 0);
#endif
if (stack)
stack_free(stack);
#ifdef TLS
- if (this != model->getInitThread() && !model->getParams()->threadsnocleanup) {
- modellock = 1;
+ if (this != model->getInitThread()) {
ASSERT(thread_current()==NULL);
- Thread * curr_thread = model->getScheduler()->get_current_thread();
- //Make any current_thread calls work in code to free
- model->getScheduler()->set_current_thread(this);
real_pthread_mutex_unlock(&mutex2);
real_pthread_join(thread, NULL);
- model->getScheduler()->set_current_thread(curr_thread);
- modellock = 0;
+ stack_free(helper_stack);
}
#endif
}
projects / c11tester.git / commitdiff