From: Brian Norris <banorris@uci.edu>
Date: Fri, 7 Dec 2012 06:42:10 +0000 (-0800)
Subject: model: generate UNINIT actions as new atomic operations form
X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=2ca6ef09383bf8845c18bb478396da3a260da08f;p=c11tester.git

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.
---

diff --git a/model.cc b/model.cc
index 771847ab..a5b06ddc 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<action_list_t> *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)