From: Brian Demsky Date: Mon, 8 Oct 2012 08:21:35 +0000 (-0700) Subject: merge massive speedup with release sequence support... X-Git-Tag: pldi2013~97 X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=b8b39c87557325a384faa45d0cae56a6f71f52b1;hp=07d9e344693c6d2b85f821447be80deaee118b65 merge massive speedup with release sequence support... Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker Conflicts: schedule.cc schedule.h --- diff --git a/action.cc b/action.cc index 09352da..c1adc2e 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 @@ -30,6 +31,7 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, 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 8267377..4f2719f 100644 --- a/model.cc +++ b/model.cc @@ -154,6 +154,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. */ @@ -173,13 +176,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; @@ -191,6 +199,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. @@ -278,7 +320,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. @@ -303,9 +345,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; @@ -323,7 +366,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; @@ -711,7 +753,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)) { @@ -722,8 +763,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); @@ -735,7 +779,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(); @@ -797,9 +840,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 68831b8..7bc3585 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 72c8d5c..3db80e8 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -267,13 +267,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 cb281ca..803d2b8 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 add_relseq_break(const ModelAction *write); const ModelAction * get_relseq_break(); diff --git a/schedule.cc b/schedule.cc index dd35237..ea1d582 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() : @@ -38,7 +39,40 @@ void Scheduler::set_enabled(Thread *t, enabled_type_t enabled_status) { bool Scheduler::is_enabled(Thread *t) const { int id = id_to_int(t->get_id()); - return (id >= enabled_len) ? false : (enabled[id] == THREAD_ENABLED); + return (id >= enabled_len) ? false : (enabled[id] != THREAD_DISABLED); +} + +enabled_type_t Scheduler::get_enabled(Thread *t) { + return 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); } /** @@ -99,7 +133,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 (enabled[curr_thread_index]) { + if (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 3feddd9..7267059 100644 --- a/schedule.h +++ b/schedule.h @@ -10,6 +10,7 @@ /* Forward declaration */ class Thread; +class Node; typedef enum enabled_type { THREAD_DISABLED, @@ -30,6 +31,10 @@ public: Thread * get_current_thread() const; void print() const; enabled_type_t * get_enabled() { return enabled; }; + void remove_sleep(Thread *t); + void add_sleep(Thread *t); + enabled_type_t get_enabled(Thread *t); + void update_sleep_set(Node *n); bool is_enabled(Thread *t) const; SNAPSHOTALLOC