#include <stdio.h>
#include <algorithm>
#include <mutex>
+#include <new>
#include "model.h"
#include "action.h"
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)
ModelAction *last_sc_write = NULL;
- /* Track whether this object has been initialized */
- bool initialized = false;
-
- if (curr->is_seqcst()) {
+ if (curr->is_seqcst())
last_sc_write = get_last_seq_cst_write(curr);
- /* We have to at least see the last sequentially consistent write,
- so we are initialized. */
- if (last_sc_write != NULL)
- initialized = true;
- }
/* Iterate over all threads */
for (i = 0; i < thrd_lists->size(); i++) {
}
/* Include at most one act per-thread that "happens before" curr */
- if (act->happens_before(curr)) {
- initialized = true;
+ if (act->happens_before(curr))
break;
- }
}
}
- if (!initialized)
- assert_bug("May read from uninitialized atomic");
-
- if (DBG_ENABLED() || !initialized) {
+ if (DBG_ENABLED()) {
model_print("Reached read action:\n");
curr->print();
model_print("Printing may_read_from\n");
}
bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) {
- while(true) {
+ while (true) {
+ /* UNINIT actions don't have a Node, and they never sleep */
+ if (write->is_uninitialized())
+ return true;
Node *prevnode=write->get_node()->get_parent();
bool thread_sleep=prevnode->enabled_status(curr->get_tid())==THREAD_SLEEP_SET;
}
}
+/**
+ * @brief Create a new action representing an uninitialized atomic
+ * @param location The memory location of the atomic object
+ * @return A pointer to a new ModelAction
+ */
+ModelAction * ModelChecker::new_uninitialized_action(void *location) const
+{
+ ModelAction *act = (ModelAction *)snapshot_malloc(sizeof(class ModelAction));
+ act = new (act) ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, location, 0, model_thread);
+ act->create_cv(NULL);
+ return act;
+}
+
static void print_list(action_list_t *list, int exec_num = -1)
{
action_list_t::iterator it;