X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=pthread.cc;h=3f0a1e4f69e278dcb67449a600922eb6d11df76c;hp=e5bc9018477a469288cb60235a8661ad31012d28;hb=38c72a8748ae74a5bb8b75e713f363a49b48e7af;hpb=82f6d9ab97a87e874fb1b5dfa237266f4bfc95d1

diff --git a/pthread.cc b/pthread.cc
index e5bc9018..3f0a1e4f 100644
--- a/pthread.cc
+++ b/pthread.cc
@@ -14,42 +14,6 @@
 #include "model.h"
 #include "execution.h"
 
-static void param_defaults(struct model_params *params)
-{
-        params->maxreads = 0;
-        params->fairwindow = 0;
-        params->yieldon = false;
-        params->yieldblock = false;
-        params->enabledcount = 1;
-        params->bound = 0;
-        params->verbose = !!DBG_ENABLED();
-        params->uninitvalue = 0;
-        params->maxexecutions = 0;
-}
-
-static void model_main()
-{
-        struct model_params params;
-
-        param_defaults(&params);
-
-        //parse_options(&params, main_argc, main_argv);
-
-        //Initialize race detector
-        initRaceDetector();
-
-        snapshot_stack_init();
-
-        model = new ModelChecker(params);       // L: Model thread is created
-//      install_trace_analyses(model->get_execution());         L: disable plugin
-
-        snapshot_record(0);
-        model->run();
-        delete model;
-
-        DEBUG("Exiting\n");
-}
-
 int pthread_create(pthread_t *t, const pthread_attr_t * attr,
           pthread_start_t start_routine, void * arg) {
 	struct pthread_params params = { start_routine, arg };
@@ -84,7 +48,7 @@ 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_main);
+	  model = new ModelChecker();
 	}
 
 	cdsc::mutex *m = new cdsc::mutex();
@@ -198,7 +162,7 @@ int pthread_cond_timedwait(pthread_cond_t *p_cond,
 	cdsc::condition_variable *v = execution->getCondMap()->get(p_cond);
 	cdsc::mutex *m = execution->getMutexMap()->get(p_mutex);
 
-	model->switch_to_master(new ModelAction(NOOP, std::memory_order_seq_cst, v, NULL));
+	model->switch_to_master(new ModelAction(NOOP, std::memory_order_seq_cst, v));
 //	v->wait(*m);
 //	printf("timed_wait called\n");
 	return 0;