memory_order_release, memory_order_acq_rel, memory_order_seq_cst,
};
-static void ensureModel() {
- if (!model) {
- snapshot_system_init(10000, 1024, 1024, 40000);
- model = new ModelChecker();
- model->startChecker();
- }
-}
-
/* --- helper functions --- */
uint64_t model_rmwrcas_action_helper(void *obj, int atomic_index, uint64_t oldval, int size, const char *position) {
- ensureModel();
+ createModelIfNotExist();
return model->switch_thread(new ModelAction(ATOMIC_RMWRCAS, position, orders[atomic_index], obj, oldval, size));
}
uint64_t model_rmwr_action_helper(void *obj, int atomic_index, const char *position) {
- ensureModel();
+ createModelIfNotExist();
return model->switch_thread(new ModelAction(ATOMIC_RMWR, position, orders[atomic_index], obj));
}
void model_rmw_action_helper(void *obj, uint64_t val, int atomic_index, const char * position) {
- ensureModel();
+ createModelIfNotExist();
model->switch_thread(new ModelAction(ATOMIC_RMW, position, orders[atomic_index], obj, val));
}
void model_rmwc_action_helper(void *obj, int atomic_index, const char *position) {
- ensureModel();
+ createModelIfNotExist();
model->switch_thread(new ModelAction(ATOMIC_RMWC, position, orders[atomic_index], obj));
}
// cds volatile loads
#define VOLATILELOAD(size) \
uint ## size ## _t cds_volatile_load ## size(void * obj, const char * position) { \
- ensureModel(); \
+ createModelIfNotExist(); \
return (uint ## size ## _t)model->switch_thread(new ModelAction(ATOMIC_READ, position, memory_order_volatile_load, obj)); \
}
// cds volatile stores
#define VOLATILESTORE(size) \
void cds_volatile_store ## size (void * obj, uint ## size ## _t val, const char * position) { \
- ensureModel(); \
+ createModelIfNotExist(); \
model->switch_thread(new ModelAction(ATOMIC_WRITE, position, memory_order_volatile_store, obj, (uint64_t) val)); \
*((volatile uint ## size ## _t *)obj) = val; \
thread_id_t tid = thread_current_id(); \
// cds atomic inits
#define CDSATOMICINT(size) \
void cds_atomic_init ## size (void * obj, uint ## size ## _t val, const char * position) { \
- ensureModel(); \
+ createModelIfNotExist(); \
model->switch_thread(new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val)); \
*((volatile uint ## size ## _t *)obj) = val; \
thread_id_t tid = thread_current_id(); \
// cds atomic loads
#define CDSATOMICLOAD(size) \
uint ## size ## _t cds_atomic_load ## size(void * obj, int atomic_index, const char * position) { \
- ensureModel(); \
+ createModelIfNotExist(); \
uint ## size ## _t val = (uint ## size ## _t)model->switch_thread( \
new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj)); \
thread_id_t tid = thread_current_id(); \
// cds atomic stores
#define CDSATOMICSTORE(size) \
void cds_atomic_store ## size(void * obj, uint ## size ## _t val, int atomic_index, const char * position) { \
- ensureModel(); \
+ createModelIfNotExist(); \
model->switch_thread(new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val)); \
*((volatile uint ## size ## _t *)obj) = val; \
thread_id_t tid = thread_current_id(); \
void cds_func_entry(const char * funcName) {
#ifdef NEWFUZZER
- ensureModel();
+ createModelIfNotExist();
thread_id_t tid = thread_current_id();
uint32_t func_id;
void cds_func_exit(const char * funcName) {
#ifdef NEWFUZZER
- ensureModel();
+ createModelIfNotExist();
thread_id_t tid = thread_current_id();
uint32_t func_id;
perror("sigaction(SIGSEGV)");
exit(EXIT_FAILURE);
}
+}
+void createModelIfNotExist() {
+ if (!model) {
+ snapshot_system_init(100000);
+ model = new ModelChecker();
+ model->startChecker();
+ }
}
/** @brief Constructor */
extern ModelChecker *model;
void parse_options(struct model_params *params);
void install_trace_analyses(ModelExecution *execution);
+void createModelIfNotExist();
#endif /* __MODEL_H__ */
size_t allocatedReqs[REQUESTS_BEFORE_ALLOC] = { 0 };
int nextRequest = 0;
int howManyFreed = 0;
-static mspace sStaticSpace = NULL;
+mspace sStaticSpace = NULL;
/** Non-snapshotting calloc for our use. */
void *model_calloc(size_t count, size_t size)
{
- if (!sStaticSpace)
- sStaticSpace = create_shared_mspace();
return mspace_calloc(sStaticSpace, count, size);
}
/** Non-snapshotting malloc for our use. */
void *model_malloc(size_t size)
{
- if (!sStaticSpace)
- sStaticSpace = create_shared_mspace();
return mspace_malloc(sStaticSpace, size);
}
/** Non-snapshotting malloc for our use. */
void *model_realloc(void *ptr, size_t size)
{
- if (!sStaticSpace)
- sStaticSpace = create_shared_mspace();
return mspace_realloc(sStaticSpace, ptr, size);
}
void * snapshot_realloc(void *ptr, size_t size);
void snapshot_free(void *ptr);
+typedef void * mspace;
+extern mspace sStaticSpace;
+
void * Thread_malloc(size_t size);
void Thread_free(void *ptr);
static int (*pipe_init_p)(int filep[2]) = NULL;
int pipe(int fildes[2]) {
- if (!model) {
- snapshot_system_init(10000, 1024, 1024, 40000);
- model = new ModelChecker();
- model->startChecker();
- }
+ createModelIfNotExist();
if (!pipe_init_p) {
pipe_init_p = (int (*)(int fildes[2]))dlsym(RTLD_NEXT, "pipe");
char *error = dlerror();
int pthread_create(pthread_t *t, const pthread_attr_t * attr,
pthread_start_t start_routine, void * arg) {
- if (!model) {
- snapshot_system_init(10000, 1024, 1024, 40000);
- model = new ModelChecker();
- model->startChecker();
- }
-
+ createModelIfNotExist();
struct pthread_params params = { start_routine, arg };
/* seq_cst is just a 'don't care' parameter */
}
int pthread_mutex_init(pthread_mutex_t *p_mutex, const pthread_mutexattr_t * attr) {
- if (!model) {
- snapshot_system_init(10000, 1024, 1024, 40000);
- model = new ModelChecker();
- model->startChecker();
- }
-
+ createModelIfNotExist();
int mutex_type = PTHREAD_MUTEX_DEFAULT;
if (attr != NULL)
pthread_mutexattr_gettype(attr, &mutex_type);
}
int pthread_mutex_lock(pthread_mutex_t *p_mutex) {
- if (!model) {
- snapshot_system_init(10000, 1024, 1024, 40000);
- model = new ModelChecker();
- model->startChecker();
- }
-
+ createModelIfNotExist();
ModelExecution *execution = model->get_execution();
/* to protect the case where PTHREAD_MUTEX_INITIALIZER is used
}
int pthread_mutex_trylock(pthread_mutex_t *p_mutex) {
- if (!model) {
- snapshot_system_init(10000, 1024, 1024, 40000);
- model = new ModelChecker();
- model->startChecker();
- }
-
+ createModelIfNotExist();
ModelExecution *execution = model->get_execution();
cdsc::snapmutex *m = execution->getMutexMap()->get(p_mutex);
return m->try_lock() ? 0 : EBUSY;
int pthread_mutex_timedlock (pthread_mutex_t *__restrict p_mutex,
const struct timespec *__restrict abstime) {
// timedlock just gives the option of giving up the lock, so return and let the scheduler decide which thread goes next
-
- if (!model) {
- snapshot_system_init(10000, 1024, 1024, 40000);
- model = new ModelChecker();
- model->startChecker();
- }
-
+ createModelIfNotExist();
ModelExecution *execution = model->get_execution();
/* to protect the case where PTHREAD_MUTEX_INITIALIZER is used
}
pthread_t pthread_self() {
- if (!model) {
- snapshot_system_init(10000, 1024, 1024, 40000);
- model = new ModelChecker();
- model->startChecker();
- }
-
+ createModelIfNotExist();
Thread* th = model->get_current_thread();
return (pthread_t)th->get_id();
}
typedef unsigned int snapshot_id;
typedef void (*VoidFuncPtr)();
-void snapshot_system_init(unsigned int numbackingpages,
- unsigned int numsnapshots, unsigned int nummemoryregions,
- unsigned int numheappages);
+void snapshot_system_init(unsigned int numheappages);
void startExecution();
snapshot_id take_snapshot();
void snapshot_roll_back(snapshot_id theSnapShot);
fork_snap->mStackSize = STACK_SIZE_DEFAULT;
fork_snap->mIDToRollback = -1;
fork_snap->currSnapShotID = 0;
+ sStaticSpace = create_shared_mspace();
}
/**
return create_mspace_with_base((void *)(fork_snap->mSharedMemoryBase), SHARED_MEMORY_DEFAULT - sizeof(*fork_snap), 1);
}
-static void fork_snapshot_init(unsigned int numbackingpages,
- unsigned int numsnapshots, unsigned int nummemoryregions,
- unsigned int numheappages)
+static void fork_snapshot_init(unsigned int numheappages)
{
if (!fork_snap)
createSharedMemory();
* @brief Initializes the snapshot system
* @param entryPoint the function that should run the program.
*/
-void snapshot_system_init(unsigned int numbackingpages,
- unsigned int numsnapshots, unsigned int nummemoryregions,
- unsigned int numheappages)
+void snapshot_system_init(unsigned int numheappages)
{
- fork_snapshot_init(numbackingpages, numsnapshots, nummemoryregions, numheappages);
+ fork_snapshot_init(numheappages);
}
void startExecution() {