projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Merge remote-tracking branch 'origin/master' into pldi13
[model-checker.git]
/
model.cc
diff --git
a/model.cc
b/model.cc
index 775b796f167d68ee8394a0e828b0791e122a4937..da982d0db415395ed2be39e9dfcf3b34f74c1efe 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-218,7
+218,8
@@
void ModelChecker::execute_sleep_set() {
for(unsigned int i=0;i<get_num_threads();i++) {
thread_id_t tid=int_to_id(i);
Thread *thr=get_thread(tid);
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 ) {
+ if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET &&
+ thr->get_pending() == NULL ) {
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);
@@
-271,8
+272,10
@@
bool ModelChecker::next_execution()
pending_rel_seqs->size());
pending_rel_seqs->size());
- if (isfinalfeasible() || (params.bound != 0 && priv->used_sequence_numbers > params.bound ) || DBG_ENABLED() )
+ if (isfinalfeasible() || (params.bound != 0 && priv->used_sequence_numbers > params.bound ) || DBG_ENABLED() ) {
+ checkDataRaces();
print_summary();
print_summary();
+ }
if ((diverge = get_next_backtrack()) == NULL)
return false;
if ((diverge = get_next_backtrack()) == NULL)
return false;
@@
-383,8
+386,12
@@
void ModelChecker::set_backtracking(ModelAction *act)
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);
+ /* Make sure this thread can be enabled here. */
+ if (i >= node->get_num_threads())
+ break;
+
/* Don't backtrack into a point where the thread is disabled or sleeping. */
/* Don't backtrack into a point where the thread is disabled or sleeping. */
- if (node->
get_enabled_array()[i]
!=THREAD_ENABLED)
+ if (node->
enabled_status(tid)
!=THREAD_ENABLED)
continue;
/* Check if this has been explored already */
continue;
/* Check if this has been explored already */
@@
-744,41
+751,46
@@
void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_qu
* initializing clock vectors, and computing the promises to fulfill.
*
* @param curr The current action, as passed from the user context; may be
* initializing clock vectors, and computing the promises to fulfill.
*
* @param curr The current action, as passed from the user context; may be
- * freed/invalidated after the execution of this function
- *
@return The current action, as processed by the ModelChecker. Is only the
- *
same as the parameter @a curr if this is a newly-explored action.
+ * freed/invalidated after the execution of this function
, with a different
+ *
action "returned" its place (pass-by-reference)
+ *
@return True if curr is a newly-explored action; false otherwise
*/
*/
-
ModelAction * ModelChecker::initialize_curr_action(ModelAction
*curr)
+
bool ModelChecker::initialize_curr_action(ModelAction *
*curr)
{
ModelAction *newcurr;
{
ModelAction *newcurr;
- if (
curr->is_rmwc() || curr
->is_rmw()) {
- newcurr = process_rmw(curr);
- delete curr;
+ if (
(*curr)->is_rmwc() || (*curr)
->is_rmw()) {
+ newcurr = process_rmw(
*
curr);
+ delete
*
curr;
if (newcurr->is_rmw())
compute_promises(newcurr);
if (newcurr->is_rmw())
compute_promises(newcurr);
- return newcurr;
+
+ *curr = newcurr;
+ return false;
}
}
-
curr
->set_seq_number(get_next_seq_num());
+
(*curr)
->set_seq_number(get_next_seq_num());
- newcurr = node_stack->explore_action(curr, scheduler->get_enabled());
+ newcurr = node_stack->explore_action(
*
curr, scheduler->get_enabled());
if (newcurr) {
/* First restore type and order in case of RMW operation */
if (newcurr) {
/* First restore type and order in case of RMW operation */
- if (
curr
->is_rmwr())
- newcurr->copy_typeandorder(curr);
+ if (
(*curr)
->is_rmwr())
+ newcurr->copy_typeandorder(
*
curr);
- ASSERT(
curr
->get_location() == newcurr->get_location());
- newcurr->copy_from_new(curr);
+ ASSERT(
(*curr)
->get_location() == newcurr->get_location());
+ newcurr->copy_from_new(
*
curr);
/* Discard duplicate ModelAction; use action from NodeStack */
/* Discard duplicate ModelAction; use action from NodeStack */
- delete curr;
+ delete
*
curr;
/* Always compute new clock vector */
newcurr->create_cv(get_parent_action(newcurr->get_tid()));
/* Always compute new clock vector */
newcurr->create_cv(get_parent_action(newcurr->get_tid()));
+
+ *curr = newcurr;
+ return false; /* Action was explored previously */
} else {
} else {
- newcurr = curr;
+ newcurr =
*
curr;
/* Always compute new clock vector */
newcurr->create_cv(get_parent_action(newcurr->get_tid()));
/* Always compute new clock vector */
newcurr->create_cv(get_parent_action(newcurr->get_tid()));
@@
-795,8
+807,8
@@
ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
else if (newcurr->is_notify_one()) {
newcurr->get_node()->set_misc_max(condvar_waiters_map->get_safe_ptr(newcurr->get_location())->size());
}
else if (newcurr->is_notify_one()) {
newcurr->get_node()->set_misc_max(condvar_waiters_map->get_safe_ptr(newcurr->get_location())->size());
}
+ return true; /* This was a new ModelAction */
}
}
- return newcurr;
}
/**
}
/**
@@
-854,18
+866,17
@@
Thread * ModelChecker::check_current_action(ModelAction *curr)
return get_next_thread(NULL);
}
return get_next_thread(NULL);
}
-
ModelAction *newcurr = initialize_curr_action(
curr);
+
bool newly_explored = initialize_curr_action(&
curr);
- wake_up_sleeping_actions(
new
curr);
+ wake_up_sleeping_actions(curr);
/* Add the action to lists before any other model-checking tasks */
if (!second_part_of_rmw)
/* Add the action to lists before any other model-checking tasks */
if (!second_part_of_rmw)
- add_action_to_lists(
new
curr);
+ add_action_to_lists(curr);
/* Build may_read_from set for newly-created actions */
/* Build may_read_from set for newly-created actions */
- if (
curr == newcurr
&& curr->is_read())
+ if (
newly_explored
&& curr->is_read())
build_reads_from_past(curr);
build_reads_from_past(curr);
- curr = newcurr;
/* Initialize work_queue with the "current action" work */
work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
/* Initialize work_queue with the "current action" work */
work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
@@
-963,7
+974,7
@@
bool ModelChecker::promises_expired() {
/** @return whether the current partial trace must be a prefix of a
* feasible trace. */
bool ModelChecker::isfeasibleprefix() {
/** @return whether the current partial trace must be a prefix of a
* feasible trace. */
bool ModelChecker::isfeasibleprefix() {
- return promises->size() == 0 && pending_rel_seqs->size() == 0;
+ return promises->size() == 0 && pending_rel_seqs->size() == 0
&& isfeasible()
;
}
/** @return whether the current partial trace is feasible. */
}
/** @return whether the current partial trace is feasible. */
@@
-1086,7
+1097,7
@@
void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) {
ModelAction *act=*rit;
bool foundvalue = false;
for (int j = 0; j<act->get_node()->get_read_from_size(); j++) {
ModelAction *act=*rit;
bool foundvalue = false;
for (int j = 0; j<act->get_node()->get_read_from_size(); j++) {
- if (act->get_node()->get_read_from_at(
i
)==write) {
+ if (act->get_node()->get_read_from_at(
j
)==write) {
foundvalue = true;
break;
}
foundvalue = true;
break;
}
@@
-1377,10
+1388,9
@@
bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *re
{
std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(reader->get_location());
unsigned int i;
{
std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(reader->get_location());
unsigned int i;
-
/* Iterate over all threads */
for (i = 0; i < thrd_lists->size(); i++) {
/* Iterate over all threads */
for (i = 0; i < thrd_lists->size(); i++) {
- ModelAction *write_after_read = NULL;
+
const
ModelAction *write_after_read = NULL;
/* Iterate over actions in thread, starting from most recent */
action_list_t *list = &(*thrd_lists)[i];
/* Iterate over actions in thread, starting from most recent */
action_list_t *list = &(*thrd_lists)[i];
@@
-1392,12
+1402,14
@@
bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *re
break;
else if (act->is_write())
write_after_read = act;
break;
else if (act->is_write())
write_after_read = act;
+ else if (act->is_read()&&act->get_reads_from()!=NULL&&act!=reader) {
+ write_after_read = act->get_reads_from();
+ }
}
}
-
- if (write_after_read && mo_graph->checkReachable(write_after_read, writer))
+
+ if (write_after_read &&
write_after_read!=writer &&
mo_graph->checkReachable(write_after_read, writer))
return false;
}
return false;
}
-
return true;
}
return true;
}
@@
-1825,7
+1837,7
@@
void ModelChecker::compute_promises(ModelAction *curr)
!act->same_thread(curr) &&
act->get_location() == curr->get_location() &&
promise->get_value() == curr->get_value()) {
!act->same_thread(curr) &&
act->get_location() == curr->get_location() &&
promise->get_value() == curr->get_value()) {
- curr->get_node()->set_promise(i);
+ curr->get_node()->set_promise(i
, act->is_rmw()
);
}
}
}
}
}
}
@@
-1847,6
+1859,16
@@
void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVec
}
}
}
}
+void ModelChecker::check_promises_thread_disabled() {
+ for (unsigned int i = 0; i < promises->size(); i++) {
+ Promise *promise = (*promises)[i];
+ if (promise->check_promise()) {
+ failed_promise = true;
+ return;
+ }
+ }
+}
+
/** Checks promises in response to addition to modification order for threads.
* Definitions:
* pthread is the thread that performed the read that created the promise
/** Checks promises in response to addition to modification order for threads.
* Definitions:
* pthread is the thread that performed the read that created the promise
@@
-1906,7
+1928,7
@@
void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write)
if (promise->has_sync_thread(tid))
continue;
if (promise->has_sync_thread(tid))
continue;
- if (mo_graph->checkReachable(promise->get_write(), write)) {
+ if (
promise->get_write()&&
mo_graph->checkReachable(promise->get_write(), write)) {
if (promise->increment_threads(tid)) {
failed_promise = true;
return;
if (promise->increment_threads(tid)) {
failed_promise = true;
return;
@@
-2017,7
+2039,8
@@
void ModelChecker::build_reads_from_past(ModelAction *curr)
bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) {
while(true) {
Node *prevnode=write->get_node()->get_parent();
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;
+
+ bool thread_sleep=prevnode->enabled_status(curr->get_tid())==THREAD_SLEEP_SET;
if (write->is_release()&&thread_sleep)
return true;
if (!write->is_rmw()) {
if (write->is_release()&&thread_sleep)
return true;
if (!write->is_rmw()) {