From 59eb730e1d19a0825008c40eb521bfc5c29df5f9 Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Mon, 8 Oct 2012 01:15:06 -0700 Subject: [PATCH] add support for sleep sets... --- action.cc | 2 ++ model.cc | 61 +++++++++++++++++++++++++++++++++++++++++++--------- model.h | 3 ++- nodestack.cc | 4 ++-- nodestack.h | 1 + schedule.cc | 36 ++++++++++++++++++++++++++++++- schedule.h | 6 +++++- 7 files changed, 98 insertions(+), 15 deletions(-) diff --git a/action.cc b/action.cc index b4f4e43..8dba82f 100644 --- a/action.cc +++ b/action.cc @@ -8,6 +8,7 @@ #include "clockvector.h" #include "common.h" #include "threads.h" +#include "nodestack.h" #define ACTION_INITIAL_CLOCK 0 @@ -17,6 +18,7 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, uint location(loc), value(value), reads_from(NULL), + node(NULL), seq_number(ACTION_INITIAL_CLOCK), cv(NULL) { diff --git a/model.cc b/model.cc index c3f6372..2c27567 100644 --- a/model.cc +++ b/model.cc @@ -150,6 +150,9 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr) earliest_diverge=diverge; Node *nextnode = next->get_node(); + Node *prevnode = nextnode->get_parent(); + scheduler->update_sleep_set(prevnode); + /* Reached divergence point */ if (nextnode->increment_promise()) { /* The next node will try to satisfy a different set of promises. */ @@ -165,13 +168,18 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr) node_stack->pop_restofstack(2); } else { /* Make a different thread execute for next step */ - Node *node = nextnode->get_parent(); - tid = node->get_next_backtrack(); + scheduler->add_sleep(thread_map->get(id_to_int(next->get_tid()))); + tid = prevnode->get_next_backtrack(); + /* Make sure the backtracked thread isn't sleeping. */ + scheduler->remove_sleep(thread_map->get(id_to_int(tid))); node_stack->pop_restofstack(1); if (diverge==earliest_diverge) { - earliest_diverge=node->get_action(); + earliest_diverge=prevnode->get_action(); } } + /* The correct sleep set is in the parent node. */ + execute_sleep_set(); + DEBUG("*** Divergence point ***\n"); diverge = NULL; @@ -183,6 +191,40 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr) return thread_map->get(id_to_int(tid)); } +/** + * We need to know what the next actions of all threads in the sleep + * set will be. This method computes them and stores the actions at + * the corresponding thread object's pending action. + */ + +void ModelChecker::execute_sleep_set() { + for(unsigned int i=0;iget_enabled(thr) == THREAD_SLEEP_SET ) { + thr->set_state(THREAD_RUNNING); + scheduler->next_thread(thr); + Thread::swap(&system_context, thr); + thr->set_pending(priv->current_action); + } + } + priv->current_action = NULL; +} + +void ModelChecker::wake_up_sleeping_actions(ModelAction * curr) { + for(unsigned int i=0;iget_enabled(thr) == THREAD_SLEEP_SET ) { + ModelAction *pending_act=thr->get_pending(); + if (pending_act->could_synchronize_with(curr)) { + //Remove this thread from sleep set + scheduler->remove_sleep(thr); + } + } + } +} + /** * Queries the model-checker for more executions to explore and, if one * exists, resets the model-checker state to execute a new execution. @@ -270,7 +312,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) return NULL; } -/** This method find backtracking points where we should try to +/** This method finds backtracking points where we should try to * reorder the parameter ModelAction against. * * @param the ModelAction to find backtracking points for. @@ -295,9 +337,10 @@ void ModelChecker::set_backtracking(ModelAction *act) for(int i = low_tid; i < high_tid; i++) { thread_id_t tid = int_to_id(i); + if (!node->is_enabled(tid)) continue; - + /* Check if this has been explored already */ if (node->has_been_explored(tid)) continue; @@ -315,7 +358,6 @@ void ModelChecker::set_backtracking(ModelAction *act) if (unfair) continue; } - /* Cache the latest backtracking point */ if (!priv->next_backtrack || *prev > *priv->next_backtrack) priv->next_backtrack = prev; @@ -631,7 +673,6 @@ bool ModelChecker::check_action_enabled(ModelAction *curr) { Thread * ModelChecker::check_current_action(ModelAction *curr) { ASSERT(curr); - bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw(); if (!check_action_enabled(curr)) { @@ -642,8 +683,11 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) return get_next_thread(NULL); } + wake_up_sleeping_actions(curr); + ModelAction *newcurr = initialize_curr_action(curr); + /* Add the action to lists before any other model-checking tasks */ if (!second_part_of_rmw) add_action_to_lists(newcurr); @@ -655,7 +699,6 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) /* Initialize work_queue with the "current action" work */ work_queue_t work_queue(1, CheckCurrWorkEntry(curr)); - while (!work_queue.empty()) { WorkQueueEntry work = work_queue.front(); work_queue.pop_front(); @@ -714,9 +757,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) } check_curr_backtracking(curr); - set_backtracking(curr); - return get_next_thread(curr); } diff --git a/model.h b/model.h index d5dc422..d2baaf4 100644 --- a/model.h +++ b/model.h @@ -124,7 +124,8 @@ private: int num_executions; int num_feasible_executions; bool promises_expired(); - + void execute_sleep_set(); + void wake_up_sleeping_actions(ModelAction * curr); modelclock_t get_next_seq_num(); /** diff --git a/nodestack.cc b/nodestack.cc index 4cf8950..76d167d 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -265,13 +265,13 @@ thread_id_t Node::get_next_backtrack() bool Node::is_enabled(Thread *t) { int thread_id=id_to_int(t->get_id()); - return thread_id < num_threads && (enabled_array[thread_id] == THREAD_ENABLED); + return thread_id < num_threads && (enabled_array[thread_id] != THREAD_DISABLED); } bool Node::is_enabled(thread_id_t tid) { int thread_id=id_to_int(tid); - return thread_id < num_threads && (enabled_array[thread_id] == THREAD_ENABLED); + return thread_id < num_threads && (enabled_array[thread_id] != THREAD_DISABLED); } bool Node::has_priority(thread_id_t tid) diff --git a/nodestack.h b/nodestack.h index 55deac5..147b004 100644 --- a/nodestack.h +++ b/nodestack.h @@ -90,6 +90,7 @@ public: bool get_promise(unsigned int i); bool increment_promise(); bool promise_empty(); + enabled_type_t *get_enabled_array() {return enabled_array;} void print(); void print_may_read_from(); diff --git a/schedule.cc b/schedule.cc index a236bd0..c5e58fe 100644 --- a/schedule.cc +++ b/schedule.cc @@ -5,6 +5,7 @@ #include "schedule.h" #include "common.h" #include "model.h" +#include "nodestack.h" /** Constructor */ Scheduler::Scheduler() : @@ -30,6 +31,39 @@ void Scheduler::set_enabled(Thread *t, enabled_type_t enabled_status) { is_enabled[threadid]=enabled_status; } +enabled_type_t Scheduler::get_enabled(Thread *t) { + return is_enabled[id_to_int(t->get_id())]; +} + +void Scheduler::update_sleep_set(Node *n) { + enabled_type_t *enabled_array=n->get_enabled_array(); + for(int i=0;iget_id())); + set_enabled(t, THREAD_SLEEP_SET); +} + +/** + * Remove a Thread from the sleep set. + * @param t The Thread to remove + */ +void Scheduler::remove_sleep(Thread *t) +{ + DEBUG("thread %d\n", id_to_int(t->get_id())); + set_enabled(t, THREAD_ENABLED); +} + /** * Add a Thread to the scheduler's ready list. * @param t The Thread to add @@ -86,7 +120,7 @@ Thread * Scheduler::next_thread(Thread *t) int old_curr_thread = curr_thread_index; while(true) { curr_thread_index = (curr_thread_index+1) % enabled_len; - if (is_enabled[curr_thread_index]) { + if (is_enabled[curr_thread_index]==THREAD_ENABLED) { t = model->get_thread(int_to_id(curr_thread_index)); break; } diff --git a/schedule.h b/schedule.h index 18936b6..3a54e8c 100644 --- a/schedule.h +++ b/schedule.h @@ -10,6 +10,7 @@ /* Forward declaration */ class Thread; +class Node; typedef enum enabled_type { THREAD_DISABLED, @@ -30,7 +31,10 @@ public: Thread * get_current_thread() const; void print() const; enabled_type_t * get_enabled() { return is_enabled; }; - + void remove_sleep(Thread *t); + void add_sleep(Thread *t); + enabled_type_t get_enabled(Thread *t); + void update_sleep_set(Node *n); SNAPSHOTALLOC private: /** The list of available Threads that are not currently running */ -- 2.34.1