#include <stdio.h>
#include <algorithm>
#include <mutex>
+#include <new>
#include "model.h"
#include "action.h"
for(unsigned int i=0;i<get_num_threads();i++) {
thread_id_t tid=int_to_id(i);
Thread *thr=get_thread(tid);
- if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET &&
- thr->get_pending() == NULL ) {
+ if (scheduler->is_sleep_set(thr) && thr->get_pending() == NULL) {
thr->set_state(THREAD_RUNNING);
scheduler->next_thread(thr);
Thread::swap(&system_context, thr);
priv->current_action = NULL;
}
-void ModelChecker::wake_up_sleeping_actions(ModelAction * curr) {
- for(unsigned int i=0;i<get_num_threads();i++) {
- thread_id_t tid=int_to_id(i);
- Thread *thr=get_thread(tid);
- if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET ) {
- ModelAction *pending_act=thr->get_pending();
- if ((!curr->is_rmwr())&&pending_act->could_synchronize_with(curr)) {
+void ModelChecker::wake_up_sleeping_actions(ModelAction *curr)
+{
+ for (unsigned int i = 0; i < get_num_threads(); i++) {
+ Thread *thr = get_thread(int_to_id(i));
+ if (scheduler->is_sleep_set(thr)) {
+ ModelAction *pending_act = thr->get_pending();
+ if ((!curr->is_rmwr()) && pending_act->could_synchronize_with(curr))
//Remove this thread from sleep set
scheduler->remove_sleep(thr);
- }
}
}
}
/* Read from future value */
value = curr->get_node()->get_future_value();
modelclock_t expiration = curr->get_node()->get_future_value_expiration();
- read_from(curr, NULL);
+ curr->set_read_from(NULL);
Promise *valuepromise = new Promise(curr, value, expiration);
promises->push_back(valuepromise);
}
*act < *last_sc_fence_thread_local) {
mo_graph->addEdge(act, rf);
added = true;
+ break;
}
/* C++, Section 29.3 statement 4 */
else if (act->is_seqcst() && last_sc_fence_local &&
*act < *last_sc_fence_local) {
mo_graph->addEdge(act, rf);
added = true;
+ break;
}
/* C++, Section 29.3 statement 6 */
else if (last_sc_fence_thread_before &&
*act < *last_sc_fence_thread_before) {
mo_graph->addEdge(act, rf);
added = true;
+ break;
}
}
*act < *last_sc_fence_thread_before) {
mo_graph->addEdge(act, curr);
added = true;
+ break;
}
/*
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)
}
}
+/**
+ * @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;