projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
mymemory: define SNAPSHOTALLOC appropriately
[model-checker.git]
/
model.cc
diff --git
a/model.cc
b/model.cc
index 40519e5315a62b12d78d6427a5ab5001236c267f..c01122191d0e712750b382f87b9c0edbfecf9aa2 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-139,6
+139,9
@@
Thread * ModelChecker::get_next_thread(ModelAction *curr)
ModelAction *next = node_stack->get_next()->get_action();
if (next == diverge) {
ModelAction *next = node_stack->get_next()->get_action();
if (next == diverge) {
+ if (earliest_diverge == NULL || *diverge < *earliest_diverge)
+ earliest_diverge=diverge;
+
Node *nextnode = next->get_node();
/* Reached divergence point */
if (nextnode->increment_promise()) {
Node *nextnode = next->get_node();
/* Reached divergence point */
if (nextnode->increment_promise()) {
@@
-158,8
+161,12
@@
Thread * ModelChecker::get_next_thread(ModelAction *curr)
Node *node = nextnode->get_parent();
tid = node->get_next_backtrack();
node_stack->pop_restofstack(1);
Node *node = nextnode->get_parent();
tid = node->get_next_backtrack();
node_stack->pop_restofstack(1);
+ if (diverge==earliest_diverge) {
+ earliest_diverge=node->get_action();
+ }
}
DEBUG("*** Divergence point ***\n");
}
DEBUG("*** Divergence point ***\n");
+
diverge = NULL;
} else {
tid = next->get_tid();
diverge = NULL;
} else {
tid = next->get_tid();
@@
-181,6
+188,7
@@
bool ModelChecker::next_execution()
DBG();
num_executions++;
DBG();
num_executions++;
+
if (isfinalfeasible()) {
printf("Earliest divergence point since last feasible execution:\n");
if (earliest_diverge)
if (isfinalfeasible()) {
printf("Earliest divergence point since last feasible execution:\n");
if (earliest_diverge)
@@
-192,15
+200,15
@@
bool ModelChecker::next_execution()
num_feasible_executions++;
}
num_feasible_executions++;
}
+ DEBUG("Number of acquires waiting on pending release sequences: %lu\n",
+ pending_acq_rel_seq->size());
+
if (isfinalfeasible() || DBG_ENABLED())
print_summary();
if ((diverge = get_next_backtrack()) == NULL)
return false;
if (isfinalfeasible() || DBG_ENABLED())
print_summary();
if ((diverge = get_next_backtrack()) == NULL)
return false;
- if (earliest_diverge == NULL || *diverge < *earliest_diverge)
- earliest_diverge=diverge;
-
if (DBG_ENABLED()) {
printf("Next execution will diverge at:\n");
diverge->print();
if (DBG_ENABLED()) {
printf("Next execution will diverge at:\n");
diverge->print();
@@
-426,7
+434,7
@@
bool ModelChecker::process_mutex(ModelAction *curr) {
action_list_t *waiters = lock_waiters_map->get_safe_ptr(curr->get_location());
//activate all the waiting threads
for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
action_list_t *waiters = lock_waiters_map->get_safe_ptr(curr->get_location());
//activate all the waiting threads
for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
- scheduler->
add_thread(get_thread((*rit)->get_tid()
));
+ scheduler->
wake(get_thread(*rit
));
}
waiters->clear();
break;
}
waiters->clear();
break;
@@
-471,11
+479,11
@@
bool ModelChecker::process_write(ModelAction *curr)
* (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
*
* @param curr The current action
* (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
*
* @param curr The current action
- * @return True if synchronization was updated
+ * @return True if synchronization was updated
or a thread completed
*/
bool ModelChecker::process_thread_action(ModelAction *curr)
{
*/
bool ModelChecker::process_thread_action(ModelAction *curr)
{
- bool
synchroniz
ed = false;
+ bool
updat
ed = false;
switch (curr->get_type()) {
case THREAD_CREATE: {
switch (curr->get_type()) {
case THREAD_CREATE: {
@@
-492,7
+500,7
@@
bool ModelChecker::process_thread_action(ModelAction *curr)
scheduler->sleep(waiting);
} else {
do_complete_join(curr);
scheduler->sleep(waiting);
} else {
do_complete_join(curr);
- synchronized = true;
+ updated = true; /* trigger rel-seq checks */
}
break;
}
}
break;
}
@@
-503,9
+511,10
@@
bool ModelChecker::process_thread_action(ModelAction *curr)
Thread *wake = get_thread(act);
scheduler->wake(wake);
do_complete_join(act);
Thread *wake = get_thread(act);
scheduler->wake(wake);
do_complete_join(act);
- synchronized = true;
+ updated = true; /* trigger rel-seq checks */
}
th->complete();
}
th->complete();
+ updated = true; /* trigger rel-seq checks */
break;
}
case THREAD_START: {
break;
}
case THREAD_START: {
@@
-516,7
+525,7
@@
bool ModelChecker::process_thread_action(ModelAction *curr)
break;
}
break;
}
- return
synchroniz
ed;
+ return
updat
ed;
}
/**
}
/**
@@
-543,6
+552,8
@@
ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
return newcurr;
}
return newcurr;
}
+ curr->set_seq_number(get_next_seq_num());
+
newcurr = node_stack->explore_action(curr, scheduler->get_enabled());
if (newcurr) {
/* First restore type and order in case of RMW operation */
newcurr = node_stack->explore_action(curr, scheduler->get_enabled());
if (newcurr) {
/* First restore type and order in case of RMW operation */
@@
-615,7
+626,7
@@
Thread * ModelChecker::check_current_action(ModelAction *curr)
/* Make the execution look like we chose to run this action
* much later, when a lock is actually available to release */
get_current_thread()->set_pending(curr);
/* Make the execution look like we chose to run this action
* much later, when a lock is actually available to release */
get_current_thread()->set_pending(curr);
-
remove_thread
(get_current_thread());
+
scheduler->sleep
(get_current_thread());
return get_next_thread(NULL);
}
return get_next_thread(NULL);
}
@@
-1317,6
+1328,8
@@
bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
}
if (updated) {
}
if (updated) {
+ /* Re-check all pending release sequences */
+ work_queue->push_back(CheckRelSeqWorkEntry(NULL));
/* Re-check act for mo_graph edges */
work_queue->push_back(MOEdgeWorkEntry(act));
/* Re-check act for mo_graph edges */
work_queue->push_back(MOEdgeWorkEntry(act));
@@
-1468,6
+1481,7
@@
bool ModelChecker::resolve_promises(ModelAction *write)
//Make sure the promise's value matches the write's value
ASSERT(promise->get_value() == write->get_value());
//Make sure the promise's value matches the write's value
ASSERT(promise->get_value() == write->get_value());
+ delete(promise);
promises->erase(promises->begin() + promise_index);
resolved = true;
} else
promises->erase(promises->begin() + promise_index);
resolved = true;
} else