From 803cd3e461cf355c118a8b1e6cd54bac6b14284c Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Wed, 26 Jun 2019 13:02:28 -0700
Subject: [PATCH] More changes
---
cmodelint.cc | 36 +++++++++++++++++-------------------
execution.h | 2 +-
main.cc | 7 +++++--
model.cc | 33 ++++++++++++++++++---------------
model.h | 2 ++
pthread.cc | 16 ++++++++++------
6 files changed, 53 insertions(+), 43 deletions(-)
diff --git a/cmodelint.cc b/cmodelint.cc
index c55b9386..96cd1c49 100644
--- a/cmodelint.cc
+++ b/cmodelint.cc
@@ -1,5 +1,6 @@
#include <stdio.h>
#include "model.h"
+#include "execution.h"
#include "action.h"
#include "cmodelint.h"
#include "snapshot-interface.h"
@@ -10,10 +11,15 @@ memory_order orders[6] = {
memory_order_release, memory_order_acq_rel, memory_order_seq_cst
};
-static void ensureModel() {
+static void ensureModel(ModelAction * action) {
if (!model) {
- snapshot_system_init(10000, 1024, 1024, 40000);
- model = new ModelChecker();
+ if (!model_init) {
+ snapshot_system_init(10000, 1024, 1024, 40000);
+ model_init = new ModelChecker();
+ }
+ model_init->get_execution()->check_current_action(action);
+ } else {
+ model->switch_to_master(action);
}
}
@@ -93,26 +99,22 @@ void model_rmwc_action_helper(void *obj, int atomic_index, const char *position)
// cds atomic inits
void cds_atomic_init8(void * obj, uint8_t val, const char * position) {
- ensureModel();
- model->switch_to_master(
+ ensureModel(
new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val)
);
}
void cds_atomic_init16(void * obj, uint16_t val, const char * position) {
- ensureModel();
- model->switch_to_master(
+ ensureModel(
new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val)
);
}
void cds_atomic_init32(void * obj, uint32_t val, const char * position) {
- ensureModel();
- model->switch_to_master(
+ ensureModel(
new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val)
);
}
void cds_atomic_init64(void * obj, uint64_t val, const char * position) {
- ensureModel();
- model->switch_to_master(
+ ensureModel(
new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, val)
);
}
@@ -142,26 +144,22 @@ uint64_t cds_atomic_load64(void * obj, int atomic_index, const char * position)
// cds atomic stores
void cds_atomic_store8(void * obj, uint8_t val, int atomic_index, const char * position) {
- ensureModel();
- model->switch_to_master(
+ ensureModel(
new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val)
);
}
void cds_atomic_store16(void * obj, uint16_t val, int atomic_index, const char * position) {
- ensureModel();
- model->switch_to_master(
+ ensureModel(
new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val)
);
}
void cds_atomic_store32(void * obj, uint32_t val, int atomic_index, const char * position) {
- ensureModel();
- model->switch_to_master(
+ ensureModel(
new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val)
);
}
void cds_atomic_store64(void * obj, uint64_t val, int atomic_index, const char * position) {
- ensureModel();
- model->switch_to_master(
+ ensureModel(
new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, val)
);
}
diff --git a/execution.h b/execution.h
index 20bbfdc6..4d5ef866 100644
--- a/execution.h
+++ b/execution.h
@@ -105,6 +105,7 @@ public:
CycleGraph * const get_mo_graph() { return mo_graph; }
HashTable<pthread_cond_t *, cdsc::condition_variable *, uintptr_t, 4> * getCondMap() {return &cond_map;}
HashTable<pthread_mutex_t *, cdsc::mutex *, uintptr_t, 4> * getMutexMap() {return &mutex_map;}
+ ModelAction * check_current_action(ModelAction *curr);
SNAPSHOTALLOC
private:
@@ -124,7 +125,6 @@ private:
modelclock_t get_next_seq_num();
bool next_execution();
- ModelAction * check_current_action(ModelAction *curr);
bool initialize_curr_action(ModelAction **curr);
void process_read(ModelAction *curr, SnapVector<const ModelAction *> * rf_set);
void process_write(ModelAction *curr);
diff --git a/main.cc b/main.cc
index 56ad5805..cc3fcbf0 100644
--- a/main.cc
+++ b/main.cc
@@ -196,7 +196,7 @@ int main(int argc, char **argv)
redirect_output();
//Initialize snapshotting library
- if (!model)
+ if (!model_init)
snapshot_system_init(10000, 1024, 1024, 40000);
struct model_params params;
@@ -210,8 +210,11 @@ int main(int argc, char **argv)
snapshot_stack_init();
- if (!model)
+ if (!model_init)
model = new ModelChecker();
+ else
+ model = model_init;
+
model->setParams(params);
install_trace_analyses(model->get_execution());
diff --git a/model.cc b/model.cc
index 84a60a51..4b159aa5 100644
--- a/model.cc
+++ b/model.cc
@@ -18,7 +18,14 @@
#include "execution.h"
#include "bugmessage.h"
-ModelChecker *model;
+ModelChecker *model = NULL;
+ModelChecker *model_init = 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);
+}
/** @brief Constructor */
ModelChecker::ModelChecker() :
@@ -33,6 +40,9 @@ ModelChecker::ModelChecker() :
inspect_plugin(NULL)
{
memset(&stats,0,sizeof(struct execution_stats));
+ init_thread = new Thread(execution->get_next_id(), (thrd_t *) malloc(sizeof(thrd_t)), &user_main_wrapper, NULL, NULL); // L: user_main_wrapper passes the user program
+ execution->add_thread(init_thread);
+ scheduler->set_current_thread(init_thread);
}
/** @brief Destructor */
@@ -313,10 +323,11 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act)
Thread *old = thread_current();
scheduler->set_current_thread(NULL);
ASSERT(!old->get_pending());
-/* W: No plugin
- if (inspect_plugin != NULL) {
- inspect_plugin->inspectModelAction(act);
- }*/
+
+ if (inspect_plugin != NULL) {
+ inspect_plugin->inspectModelAction(act);
+ }
+
old->set_pending(act);
if (Thread::swap(old, &system_context) < 0) {
perror("swap threads");
@@ -325,12 +336,6 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act)
return old->get_return_value();
}
-/** Wrapper to run the user's main function, with appropriate arguments */
-void user_main_wrapper(void *)
-{
- user_main(model->params.argc, model->params.argv);
-}
-
bool ModelChecker::should_terminate_execution()
{
/* Infeasible -> don't take any more steps */
@@ -367,10 +372,8 @@ void ModelChecker::run()
initstate(423121, random_state, sizeof(random_state));
for(int exec = 0;exec < params.maxexecutions;exec++) {
- thrd_t user_thread;
- Thread *t = new Thread(execution->get_next_id(), &user_thread, &user_main_wrapper, NULL, NULL); // L: user_main_wrapper passes the user program
- execution->add_thread(t);
- //Need to seed random number generator, otherwise its state gets reset
+ Thread * t = init_thread;
+
do {
/*
* Stash next pending action(s) for thread(s). There
diff --git a/model.h b/model.h
index 2a505c3d..46c24543 100644
--- a/model.h
+++ b/model.h
@@ -72,6 +72,7 @@ private:
Scheduler * const scheduler;
NodeStack * const node_stack;
ModelExecution *execution;
+ Thread * init_thread;
int execution_number;
@@ -103,5 +104,6 @@ private:
};
extern ModelChecker *model;
+extern ModelChecker *model_init;
#endif /* __MODEL_H__ */
diff --git a/pthread.cc b/pthread.cc
index 35af63e6..79e90425 100644
--- a/pthread.cc
+++ b/pthread.cc
@@ -48,15 +48,19 @@ void pthread_exit(void *value_ptr) {
}
int pthread_mutex_init(pthread_mutex_t *p_mutex, const pthread_mutexattr_t *) {
- if (!model) {
- snapshot_system_init(10000, 1024, 1024, 40000);
- model = new ModelChecker();
- }
-
cdsc::mutex *m = new cdsc::mutex();
+ ModelExecution *execution;
- ModelExecution *execution = model->get_execution();
+ if (!model) {
+ if (!model_init) {
+ snapshot_system_init(10000, 1024, 1024, 40000);
+ model_init = new ModelChecker();
+ }
+ execution = model_init->get_execution();
+ } else
+ execution = model->get_execution();
execution->getMutexMap()->put(p_mutex, m);
+
return 0;
}
--
2.34.1