summary |
shortlog |
log |
commit | commitdiff |
tree
raw |
patch |
inline | side by side (from parent 1:
188fd67)
if an action was sleeping, it should only read from a value that could potentially result in synchronization with a release done while it was sleeping
reads_from(NULL),
node(NULL),
seq_number(ACTION_INITIAL_CLOCK),
reads_from(NULL),
node(NULL),
seq_number(ACTION_INITIAL_CLOCK),
+ cv(NULL),
+ sleep_flag(false)
{
Thread *t = thread ? thread : thread_current();
this->tid = t->get_id();
{
Thread *t = thread ? thread : thread_current();
this->tid = t->get_id();
void process_rmw(ModelAction * act);
void copy_typeandorder(ModelAction * act);
void process_rmw(ModelAction * act);
void copy_typeandorder(ModelAction * act);
+ void set_sleep_flag() { sleep_flag=true; }
+ bool get_sleep_flag() { return sleep_flag; }
+
/** The clock vector stored with this action; only needed if this
* action is a store release? */
ClockVector *cv;
/** The clock vector stored with this action; only needed if this
* action is a store release? */
ClockVector *cv;
};
typedef std::list< ModelAction *, SnapshotAlloc<ModelAction *> > action_list_t;
};
typedef std::list< ModelAction *, SnapshotAlloc<ModelAction *> > action_list_t;
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->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=prevnode->get_action();
node_stack->pop_restofstack(1);
if (diverge==earliest_diverge) {
earliest_diverge=prevnode->get_action();
thr->set_state(THREAD_RUNNING);
scheduler->next_thread(thr);
Thread::swap(&system_context, thr);
thr->set_state(THREAD_RUNNING);
scheduler->next_thread(thr);
Thread::swap(&system_context, thr);
+ priv->current_action->set_sleep_flag();
thr->set_pending(priv->current_action);
}
}
thr->set_pending(priv->current_action);
}
}
for(int i = low_tid; i < high_tid; i++) {
thread_id_t tid = int_to_id(i);
for(int i = low_tid; i < high_tid; i++) {
thread_id_t tid = int_to_id(i);
- if (!node->is_enabled(tid))
+ /* Don't backtrack into a point where the thread is disabled or sleeping. */
+ if (node->get_enabled_array()[i]!=THREAD_ENABLED)
continue;
/* Check if this has been explored already */
continue;
/* Check if this has been explored already */
act->print();
curr->print();
}
act->print();
curr->print();
}
- curr->get_node()->add_read_from(act);
+
+ if (curr->get_sleep_flag()) {
+ if (sleep_can_read_from(curr, act))
+ curr->get_node()->add_read_from(act);
+ } else
+ curr->get_node()->add_read_from(act);
}
/* Include at most one act per-thread that "happens before" curr */
}
/* Include at most one act per-thread that "happens before" curr */
+bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) {
+ while(true) {
+ Node *prevnode=write->get_node()->get_parent();
+ bool thread_sleep=prevnode->get_enabled_array()[id_to_int(curr->get_tid())]==THREAD_SLEEP_SET;
+ if (write->is_release()&&thread_sleep)
+ return true;
+ if (!write->is_rmw())
+ return false;
+ if (write->get_reads_from()==NULL)
+ return true;
+ write=write->get_reads_from();
+ }
+}
+
static void print_list(action_list_t *list)
{
action_list_t::iterator it;
static void print_list(action_list_t *list)
{
action_list_t::iterator it;
/** The scheduler to use: tracks the running/ready Threads */
Scheduler *scheduler;
/** The scheduler to use: tracks the running/ready Threads */
Scheduler *scheduler;
+ bool sleep_can_read_from(ModelAction * curr, const ModelAction *write);
bool thin_air_constraint_may_allow(const ModelAction * writer, const ModelAction *reader);
bool has_asserted() {return asserted;}
void reset_asserted() {asserted=false;}
bool thin_air_constraint_may_allow(const ModelAction * writer, const ModelAction *reader);
bool has_asserted() {return asserted;}
void reset_asserted() {asserted=false;}