--- /dev/null
+****************************************
+CDSChecker Readme
+****************************************
+
+This is an evaluation-only version of CDSChecker. Please do not distribute.
+
+CDSChecker compiles as a dynamically-linked shared library by simply running
+'make'. It should compile on Linux and Mac OSX, and has been tested with LLVM
+(clang/clang++) and GCC.
+
+Test programs should use the standard C11/C++11 library headers
+(<atomic>/<stdatomic.h>, <mutex>, <condition_variable>, <thread.h>) and must
+name their main routine as user_main(int, char**) rather than main(int, char**).
+We only support C11 thread syntax (thrd_t, etc. from <thread.h>).
+
+Test programs may also use our included happens-before race detector by
+including <librace.h> and utilizing the appropriate functions
+(store_{8,16,32,64}() and load_{8,16,32,64}()) for loading/storing data from/to
+from non-atomic shared memory.
+
+Test programs should be compiled against our shared library (libmodel.so) using
+the headers in the include/ directory. Then the shared library must be made
+available to the dynamic linker, using the LD_LIBRARY_PATH environment
+variable, for instance.
+
+Sample run instructions:
+
+$ make
+$ export LD_LIBRARY_PATH=.
+$ ./test/userprog.o # Runs simple test program
+$ ./test/userprog.o -h # Prints help information
+Usage: <program name> [MC_OPTIONS] -- [PROGRAM ARGUMENTS]
+
+Options:
+-h Display this help message and exit
+-m Maximum times a thread can read from the same write
+ while other writes exist. Default: 0
+-M Maximum number of future values that can be sent to
+ the same read. Default: 0
+-s Maximum actions that the model checker will wait for
+ a write from the future past the expected number of
+ actions. Default: 100
+-S Future value expiration sloppiness. Default: 10
+-f Specify a fairness window in which actions that are
+ enabled sufficiently many times should receive
+ priority for execution. Default: 0
+-e Enabled count. Default: 1
+-b Upper length bound. Default: 0
+-- Program arguments follow.
+
+
+Note that we also provide a series of benchmarks (distributed separately),
+which can be placed under the benchmarks/ directory. After building CDSChecker,
+you can build and run the benchmarks as follows:
+
+ cd benchmarks
+ make
+ ./run.sh barrier/barrier -f 10 -m 2 # runs barrier test with fairness/memory liveness
+ ./bench.sh <dir> # run all benchmarks twice, with timing results; all logged to <dir>
/* Size of stack to allocate for a thread. */
#define STACK_SIZE (1024 * 1024)
+/** How many shadow tables of memory to preallocate for data race detector. */
#define SHADOWBASETABLES 4
+/** Enable debugging assertions (via ASSERT()) */
+#define CONFIG_ASSERT
+
#endif
/** This function looks up the entry in the shadow table corresponding to a
* given address.*/
-static uint64_t * lookupAddressEntry(void * address) {
+static uint64_t * lookupAddressEntry(const void * address) {
struct ShadowTable *currtable=root;
#if BIT48
currtable=(struct ShadowTable *) currtable->array[(((uintptr_t)address)>>32)&MASK16BIT];
}
/** This function is called when we detect a data race.*/
-static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool isoldwrite, ModelAction *newaction, bool isnewwrite, void *address) {
+static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool isoldwrite, ModelAction *newaction, bool isnewwrite, const void *address) {
struct DataRace *race = (struct DataRace *)snapshot_malloc(sizeof(struct DataRace));
race->oldthread=oldthread;
race->oldclock=oldclock;
}
/** This function does race detection on a read for an expanded record. */
-void fullRaceCheckRead(thread_id_t thread, void *location, uint64_t * shadow, ClockVector *currClock) {
+void fullRaceCheckRead(thread_id_t thread, const void *location, uint64_t * shadow, ClockVector *currClock) {
struct RaceRecord * record=(struct RaceRecord *) (*shadow);
/* Check for datarace against last write. */
}
/** This function does race detection on a read. */
-void raceCheckRead(thread_id_t thread, void *location, ClockVector *currClock) {
+void raceCheckRead(thread_id_t thread, const void *location, ClockVector *currClock) {
uint64_t * shadow=lookupAddressEntry(location);
uint64_t shadowval=*shadow;
bool isnewwrite;
/* Address of data race. */
- void *address;
+ const void *address;
};
#define MASK16BIT 0xffff
void initRaceDetector();
void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock);
-void raceCheckRead(thread_id_t thread, void *location, ClockVector *currClock);
+void raceCheckRead(thread_id_t thread, const void *location, ClockVector *currClock);
bool checkDataRaces();
void printRace(struct DataRace *race);
void store_32(void *addr, uint32_t val);
void store_64(void *addr, uint64_t val);
- uint8_t load_8(void *addr);
- uint16_t load_16(void *addr);
- uint32_t load_32(void *addr);
- uint64_t load_64(void *addr);
+ uint8_t load_8(const void *addr);
+ uint16_t load_16(const void *addr);
+ uint32_t load_32(const void *addr);
+ uint64_t load_64(const void *addr);
#ifdef __cplusplus
}
(*(uint64_t *)addr) = val;
}
-uint8_t load_8(void *addr)
+uint8_t load_8(const void *addr)
{
DEBUG("addr = %p\n", addr);
thread_id_t tid=thread_current()->get_id();
return *((uint8_t *)addr);
}
-uint16_t load_16(void *addr)
+uint16_t load_16(const void *addr)
{
DEBUG("addr = %p\n", addr);
thread_id_t tid=thread_current()->get_id();
ClockVector * cv=model->get_cv(tid);
raceCheckRead(tid, addr, cv);
- raceCheckRead(tid, (void *)(((uintptr_t)addr)+1), cv);
+ raceCheckRead(tid, (const void *)(((uintptr_t)addr)+1), cv);
return *((uint16_t *)addr);
}
-uint32_t load_32(void *addr)
+uint32_t load_32(const void *addr)
{
DEBUG("addr = %p\n", addr);
thread_id_t tid=thread_current()->get_id();
ClockVector * cv=model->get_cv(tid);
raceCheckRead(tid, addr, cv);
- raceCheckRead(tid, (void *)(((uintptr_t)addr)+1), cv);
- raceCheckRead(tid, (void *)(((uintptr_t)addr)+2), cv);
- raceCheckRead(tid, (void *)(((uintptr_t)addr)+3), cv);
+ raceCheckRead(tid, (const void *)(((uintptr_t)addr)+1), cv);
+ raceCheckRead(tid, (const void *)(((uintptr_t)addr)+2), cv);
+ raceCheckRead(tid, (const void *)(((uintptr_t)addr)+3), cv);
return *((uint32_t *)addr);
}
-uint64_t load_64(void *addr)
+uint64_t load_64(const void *addr)
{
DEBUG("addr = %p\n", addr);
thread_id_t tid=thread_current()->get_id();
ClockVector * cv=model->get_cv(tid);
raceCheckRead(tid, addr, cv);
- raceCheckRead(tid, (void *)(((uintptr_t)addr)+1), cv);
- raceCheckRead(tid, (void *)(((uintptr_t)addr)+2), cv);
- raceCheckRead(tid, (void *)(((uintptr_t)addr)+3), cv);
- raceCheckRead(tid, (void *)(((uintptr_t)addr)+4), cv);
- raceCheckRead(tid, (void *)(((uintptr_t)addr)+5), cv);
- raceCheckRead(tid, (void *)(((uintptr_t)addr)+6), cv);
- raceCheckRead(tid, (void *)(((uintptr_t)addr)+7), cv);
+ raceCheckRead(tid, (const void *)(((uintptr_t)addr)+1), cv);
+ raceCheckRead(tid, (const void *)(((uintptr_t)addr)+2), cv);
+ raceCheckRead(tid, (const void *)(((uintptr_t)addr)+3), cv);
+ raceCheckRead(tid, (const void *)(((uintptr_t)addr)+4), cv);
+ raceCheckRead(tid, (const void *)(((uintptr_t)addr)+5), cv);
+ raceCheckRead(tid, (const void *)(((uintptr_t)addr)+6), cv);
+ raceCheckRead(tid, (const void *)(((uintptr_t)addr)+7), cv);
return *((uint64_t *)addr);
}
ModelChecker *model;
+/**
+ * Structure for holding small ModelChecker members that should be snapshotted
+ */
+struct model_snapshot_members {
+ ModelAction *current_action;
+ unsigned int next_thread_id;
+ modelclock_t used_sequence_numbers;
+ Thread *nextThread;
+ ModelAction *next_backtrack;
+};
+
/** @brief Constructor */
ModelChecker::ModelChecker(struct model_params params) :
/* Initialize default scheduler */
{
bool blocking_threads = false;
for (unsigned int i = 0; i < get_num_threads(); i++) {
- Thread *t = get_thread(int_to_id(i));
- if (scheduler->is_enabled(t) != THREAD_DISABLED)
+ thread_id_t tid = int_to_id(i);
+ if (is_enabled(tid))
return false;
- else if (!t->is_model_thread() && t->get_pending())
+ Thread *t = get_thread(tid);
+ if (!t->is_model_thread() && t->get_pending())
blocking_threads = true;
}
return blocking_threads;
pending_rel_seqs->size());
- if (isfinalfeasible() || (params.bound != 0 && priv->used_sequence_numbers > params.bound ) || DBG_ENABLED() ) {
+ if (isfinalfeasible() || DBG_ENABLED()) {
checkDataRaces();
print_summary();
}
return true;
}
+/**
+ * Stores the ModelAction for the current thread action. Call this
+ * immediately before switching from user- to system-context to pass
+ * data between them.
+ * @param act The ModelAction created by the user-thread action
+ */
+void ModelChecker::set_current_action(ModelAction *act) {
+ priv->current_action = act;
+}
+
/**
* This is the heart of the model checker routine. It performs model-checking
* actions corresponding to a given "current action." Among other processes, it
ModelAction *last = get_last_action(int_to_id(i));
Thread *th = get_thread(int_to_id(i));
if ((last && rf->happens_before(last)) ||
- !scheduler->is_enabled(th) ||
+ !is_enabled(th) ||
th->is_complete())
future_ordered = true;
return get_thread(act->get_tid());
}
+/**
+ * @brief Check if a Thread is currently enabled
+ * @param t The Thread to check
+ * @return True if the Thread is currently enabled
+ */
+bool ModelChecker::is_enabled(Thread *t) const
+{
+ return scheduler->is_enabled(t);
+}
+
+/**
+ * @brief Check if a Thread is currently enabled
+ * @param tid The ID of the Thread to check
+ * @return True if the Thread is currently enabled
+ */
+bool ModelChecker::is_enabled(thread_id_t tid) const
+{
+ return scheduler->is_enabled(tid);
+}
+
/**
* Switch from a user-context to the "master thread" context (a.k.a. system
* context). This switch is made with the intention of exploring a particular
class Promise;
class Scheduler;
class Thread;
+struct model_snapshot_members;
/** @brief Shorthand for a list of release sequence heads */
typedef std::vector< const ModelAction *, ModelAlloc<const ModelAction *> > rel_heads_list_t;
struct PendingFutureValue {
ModelAction *writer;
- ModelAction * act;
-};
-
-/**
- * Structure for holding small ModelChecker members that should be snapshotted
- */
-struct model_snapshot_members {
- ModelAction *current_action;
- unsigned int next_thread_id;
- modelclock_t used_sequence_numbers;
- Thread *nextThread;
- ModelAction *next_backtrack;
+ ModelAction *act;
};
/** @brief Records information regarding a single pending release sequence */
Thread * get_thread(thread_id_t tid) const;
Thread * get_thread(ModelAction *act) const;
+ bool is_enabled(Thread *t) const;
+ bool is_enabled(thread_id_t tid) const;
+
thread_id_t get_next_id();
unsigned int get_num_threads() const;
Thread * get_current_thread();
void set_bad_synchronization() { bad_synchronization = true; }
const model_params params;
- Scheduler * get_scheduler() { return scheduler;}
Node * get_curr_node();
MEMALLOC
void wake_up_sleeping_actions(ModelAction * curr);
modelclock_t get_next_seq_num();
- /**
- * Stores the ModelAction for the current thread action. Call this
- * immediately before switching from user- to system-context to pass
- * data between them.
- * @param act The ModelAction created by the user-thread action
- */
- void set_current_action(ModelAction *act) { priv->current_action = act; }
+ void set_current_action(ModelAction *act);
Thread * check_current_action(ModelAction *curr);
bool initialize_curr_action(ModelAction **curr);
bool process_read(ModelAction *curr, bool second_part_of_rmw);
return false;
synced_thread[id]=true;
- enabled_type_t * enabled=model->get_scheduler()->get_enabled();
unsigned int sync_size=synced_thread.size();
int promise_tid=id_to_int(read->get_tid());
for(unsigned int i=1;i<model->get_num_threads();i++) {
- if ((i >= sync_size || !synced_thread[i]) && ( (int)i != promise_tid ) && (enabled[i] != THREAD_DISABLED)) {
+ if ((i >= sync_size || !synced_thread[i]) && ( (int)i != promise_tid ) && model->is_enabled(int_to_id(i))) {
return false;
}
}
}
bool Promise::check_promise() {
- enabled_type_t * enabled=model->get_scheduler()->get_enabled();
unsigned int sync_size=synced_thread.size();
for(unsigned int i=1;i<model->get_num_threads();i++) {
- if ((i >= sync_size || !synced_thread[i]) && (enabled[i] != THREAD_DISABLED)) {
+ if ((i >= sync_size || !synced_thread[i]) && model->is_enabled(int_to_id(i))) {
return false;
}
}
/**
* @brief Check if a Thread is currently enabled
+ *
+ * Check if a Thread is currently enabled. "Enabled" includes both
+ * THREAD_ENABLED and THREAD_SLEEP_SET.
* @param t The Thread to check
* @return True if the Thread is currently enabled
*/
bool Scheduler::is_enabled(Thread *t) const
{
- int id = id_to_int(t->get_id());
- return (id >= enabled_len) ? false : (enabled[id] != THREAD_DISABLED);
+ return is_enabled(t->get_id());
+}
+
+/**
+ * @brief Check if a Thread is currently enabled
+ *
+ * Check if a Thread is currently enabled. "Enabled" includes both
+ * THREAD_ENABLED and THREAD_SLEEP_SET.
+ * @param tid The ID of the Thread to check
+ * @return True if the Thread is currently enabled
+ */
+bool Scheduler::is_enabled(thread_id_t tid) const
+{
+ int i = id_to_int(tid);
+ return (i >= enabled_len) ? false : (enabled[i] != THREAD_DISABLED);
}
enabled_type_t Scheduler::get_enabled(Thread *t) {
enabled_type_t get_enabled(Thread *t);
void update_sleep_set(Node *n);
bool is_enabled(Thread *t) const;
+ bool is_enabled(thread_id_t tid) const;
SNAPSHOTALLOC
private:
projects / cdsspec-compiler.git / commitdiff