From 2ca6ef09383bf8845c18bb478396da3a260da08f Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Thu, 6 Dec 2012 22:42:10 -0800 Subject: [PATCH] model: generate UNINIT actions as new atomic operations form The first time an atomic variable is accessed, we need to add an appropriate UNINIT action to the ModelChecker data structures. We assign these ModelActions to the special model-checker thread (Thread 0). Note that these actions will *not* appear in the NodeStack and will not be explored in check_current_action, etc. --- model.cc | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/model.cc b/model.cc index 771847a..a5b06dd 100644 --- a/model.cc +++ b/model.cc @@ -2102,18 +2102,32 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_ void ModelChecker::add_action_to_lists(ModelAction *act) { int tid = id_to_int(act->get_tid()); - action_trace->push_back(act); + ModelAction *uninit = NULL; + int uninit_id = -1; + action_list_t *list = get_safe_ptr_action(obj_map, act->get_location()); + if (list->empty()) { + uninit = new_uninitialized_action(act->get_location()); + uninit_id = id_to_int(uninit->get_tid()); + list->push_back(uninit); + } + list->push_back(act); - get_safe_ptr_action(obj_map, act->get_location())->push_back(act); + action_trace->push_back(act); + if (uninit) + action_trace->push_front(uninit); std::vector *vec = get_safe_ptr_vect_action(obj_thrd_map, act->get_location()); if (tid >= (int)vec->size()) vec->resize(priv->next_thread_id); (*vec)[tid].push_back(act); + if (uninit) + (*vec)[uninit_id].push_front(uninit); if ((int)thrd_last_action->size() <= tid) thrd_last_action->resize(get_num_threads()); (*thrd_last_action)[tid] = act; + if (uninit) + (*thrd_last_action)[uninit_id] = uninit; if (act->is_fence() && act->is_release()) { if ((int)thrd_last_fence_release->size() <= tid) -- 2.34.1