X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=execution.cc;h=828502686d0194e642e8b2335c910c33f86ff049;hb=bf80445c97bd34afcfd208cc3ecb31edcd631bb6;hp=0006c66c70a3acf89433bfd4013e03ad3f5b3e1c;hpb=a22d12cff31e5309eb0033324d3dd0258de53cb5;p=model-checker.git diff --git a/execution.cc b/execution.cc index 0006c66..8285026 100644 --- a/execution.cc +++ b/execution.cc @@ -82,6 +82,7 @@ ModelExecution::ModelExecution(struct model_params *params, Scheduler *scheduler /* Initialize a model-checker thread, for special ModelActions */ model_thread = new Thread(get_next_id()); thread_map->put(id_to_int(model_thread->get_id()), model_thread); + scheduler->register_engine(this); } /** @brief Destructor */ @@ -128,7 +129,8 @@ static SnapVector * get_safe_ptr_vect_action(HashTable *wrv=obj_thrd_map->get(obj); if (wrv==NULL) return NULL; @@ -615,7 +617,7 @@ bool ModelExecution::process_read(ModelAction *curr) case READ_FROM_FUTURE: { /* Read from future value */ struct future_value fv = node->get_future_value(); - Promise *promise = new Promise(curr, fv); + Promise *promise = new Promise(this, curr, fv); curr->set_read_from_promise(promise); promises->push_back(promise); mo_graph->startChanges(); @@ -910,7 +912,7 @@ bool ModelExecution::process_thread_action(ModelAction *curr) case THREAD_CREATE: { thrd_t *thrd = (thrd_t *)curr->get_location(); struct thread_params *params = (struct thread_params *)curr->get_value(); - Thread *th = new Thread(thrd, params->func, params->arg, get_thread(curr)); + Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr)); add_thread(th); th->set_creation(curr); /* Promises can be satisfied by children */