projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
action: add get_thread_operand() method
[model-checker.git]
/
model.cc
diff --git
a/model.cc
b/model.cc
index d6b84c3ef457ddbaf3c6838d1efe243487f24d16..84c42689425f257d594c969df0b758038001ab83 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-174,7
+174,12
@@
unsigned int ModelChecker::get_num_threads() const
return priv->next_thread_id;
}
return priv->next_thread_id;
}
-/** @return The currently executing Thread. */
+/**
+ * Must be called from user-thread context (e.g., through the global
+ * thread_current() interface)
+ *
+ * @return The currently executing Thread.
+ */
Thread * ModelChecker::get_current_thread() const
{
return scheduler->get_current_thread();
Thread * ModelChecker::get_current_thread() const
{
return scheduler->get_current_thread();
@@
-212,9
+217,8
@@
Thread * ModelChecker::get_next_thread(ModelAction *curr)
/* Do not split atomic actions. */
if (curr->is_rmwr())
return thread_current();
/* Do not split atomic actions. */
if (curr->is_rmwr())
return thread_current();
- /* The THREAD_CREATE action points to the created Thread */
else if (curr->get_type() == THREAD_CREATE)
else if (curr->get_type() == THREAD_CREATE)
- return
(Thread *)curr->get_location
();
+ return
curr->get_thread_operand
();
}
/* Have we completed exploring the preselected path? */
}
/* Have we completed exploring the preselected path? */
@@
-254,8
+258,9
@@
Thread * ModelChecker::get_next_thread(ModelAction *curr)
tid = next->get_tid();
node_stack->pop_restofstack(2);
} else {
tid = next->get_tid();
node_stack->pop_restofstack(2);
} else {
+ ASSERT(prevnode);
/* Make a different thread execute for next step */
/* Make a different thread execute for next step */
- scheduler->add_sleep(
thread_map->get(id_to_int(next->get_tid()
)));
+ scheduler->add_sleep(
get_thread(next->get_tid(
)));
tid = prevnode->get_next_backtrack();
/* Make sure the backtracked thread isn't sleeping. */
node_stack->pop_restofstack(1);
tid = prevnode->get_next_backtrack();
/* Make sure the backtracked thread isn't sleeping. */
node_stack->pop_restofstack(1);
@@
-557,7
+562,7
@@
ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *prev = *rit;
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *prev = *rit;
- if (!act->same_thread(prev)
&&
prev->is_failed_trylock())
+ if (!act->same_thread(prev)
&&
prev->is_failed_trylock())
return prev;
}
break;
return prev;
}
break;
@@
-568,9
+573,9
@@
ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *prev = *rit;
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *prev = *rit;
- if (!act->same_thread(prev)
&&
prev->is_failed_trylock())
+ if (!act->same_thread(prev)
&&
prev->is_failed_trylock())
return prev;
return prev;
- if (!act->same_thread(prev)
&&
prev->is_notify())
+ if (!act->same_thread(prev)
&&
prev->is_notify())
return prev;
}
break;
return prev;
}
break;
@@
-583,7
+588,7
@@
ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *prev = *rit;
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *prev = *rit;
- if (!act->same_thread(prev)
&&
prev->is_wait())
+ if (!act->same_thread(prev)
&&
prev->is_wait())
return prev;
}
break;
return prev;
}
break;
@@
-617,7
+622,7
@@
void ModelChecker::set_backtracking(ModelAction *act)
high_tid = get_num_threads();
}
high_tid = get_num_threads();
}
- for(int i = low_tid; i < high_tid; 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. */
thread_id_t tid = int_to_id(i);
/* Make sure this thread can be enabled here. */
@@
-717,7
+722,7
@@
bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
}
}
- if (!second_part_of_rmw
&&is_infeasible()&&(curr->get_node()->increment_read_from()||
curr->get_node()->increment_future_value())) {
+ if (!second_part_of_rmw
&& is_infeasible() && (curr->get_node()->increment_read_from() ||
curr->get_node()->increment_future_value())) {
mo_graph->rollbackChanges();
priv->too_many_reads = false;
continue;
mo_graph->rollbackChanges();
priv->too_many_reads = false;
continue;
@@
-765,7
+770,7
@@
bool ModelChecker::process_mutex(ModelAction *curr)
if (curr->is_trylock() || curr->is_lock() || curr->is_unlock()) {
mutex = (std::mutex *)curr->get_location();
state = mutex->get_state();
if (curr->is_trylock() || curr->is_lock() || curr->is_unlock()) {
mutex = (std::mutex *)curr->get_location();
state = mutex->get_state();
- } else if(curr->is_wait()) {
+ } else if
(curr->is_wait()) {
mutex = (std::mutex *)curr->get_value();
state = mutex->get_state();
}
mutex = (std::mutex *)curr->get_value();
state = mutex->get_state();
}
@@
-819,7
+824,7
@@
bool ModelChecker::process_mutex(ModelAction *curr)
if (curr->get_node()->get_misc() == 0) {
get_safe_ptr_action(condvar_waiters_map, curr->get_location())->push_back(curr);
//disable us
if (curr->get_node()->get_misc() == 0) {
get_safe_ptr_action(condvar_waiters_map, curr->get_location())->push_back(curr);
//disable us
- scheduler->sleep(get_
current_thread(
));
+ scheduler->sleep(get_
thread(curr
));
}
break;
}
}
break;
}
@@
-943,12
+948,12
@@
bool ModelChecker::process_thread_action(ModelAction *curr)
switch (curr->get_type()) {
case THREAD_CREATE: {
switch (curr->get_type()) {
case THREAD_CREATE: {
- Thread *th =
(Thread *)curr->get_location
();
+ Thread *th =
curr->get_thread_operand
();
th->set_creation(curr);
break;
}
case THREAD_JOIN: {
th->set_creation(curr);
break;
}
case THREAD_JOIN: {
- Thread *blocking =
(Thread *)curr->get_location
();
+ Thread *blocking =
curr->get_thread_operand
();
ModelAction *act = get_last_action(blocking->get_id());
curr->synchronize_with(act);
updated = true; /* trigger rel-seq checks */
ModelAction *act = get_last_action(blocking->get_id());
curr->synchronize_with(act);
updated = true; /* trigger rel-seq checks */
@@
-1191,11
+1196,10
@@
void ModelChecker::set_current_action(ModelAction *act) {
* execution when running permutations of previously-observed executions.
*
* @param curr The current action to process
* execution when running permutations of previously-observed executions.
*
* @param curr The current action to process
- * @return The next Thread that must be executed. May be NULL if ModelChecker
- * makes no choice (e.g., according to replay execution, combining RMW actions,
- * etc.)
+ * @return The ModelAction that is actually executed; may be different than
+ * curr; may be NULL, if the current action is not enabled to run
*/
*/
-
Thread
* ModelChecker::check_current_action(ModelAction *curr)
+
ModelAction
* ModelChecker::check_current_action(ModelAction *curr)
{
ASSERT(curr);
bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
{
ASSERT(curr);
bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
@@
-1203,13
+1207,17
@@
Thread * ModelChecker::check_current_action(ModelAction *curr)
if (!check_action_enabled(curr)) {
/* Make the execution look like we chose to run this action
* much later, when a lock/join can succeed */
if (!check_action_enabled(curr)) {
/* Make the execution look like we chose to run this action
* much later, when a lock/join can succeed */
- get_
current_thread(
)->set_pending(curr);
- scheduler->sleep(get_
current_thread(
));
- return
get_next_thread(NULL)
;
+ get_
thread(curr
)->set_pending(curr);
+ scheduler->sleep(get_
thread(curr
));
+ return
NULL
;
}
bool newly_explored = initialize_curr_action(&curr);
}
bool newly_explored = initialize_curr_action(&curr);
+ DBG();
+ if (DBG_ENABLED())
+ curr->print();
+
wake_up_sleeping_actions(curr);
/* Add the action to lists before any other model-checking tasks */
wake_up_sleeping_actions(curr);
/* Add the action to lists before any other model-checking tasks */
@@
-1287,7
+1295,7
@@
Thread * ModelChecker::check_current_action(ModelAction *curr)
check_curr_backtracking(curr);
set_backtracking(curr);
check_curr_backtracking(curr);
set_backtracking(curr);
- return
get_next_thread(curr)
;
+ return
curr
;
}
void ModelChecker::check_curr_backtracking(ModelAction *curr)
}
void ModelChecker::check_curr_backtracking(ModelAction *curr)
@@
-1295,7
+1303,7
@@
void ModelChecker::check_curr_backtracking(ModelAction *curr)
Node *currnode = curr->get_node();
Node *parnode = currnode->get_parent();
Node *currnode = curr->get_node();
Node *parnode = currnode->get_parent();
- if (
!parnode->backtrack_empty(
) ||
+ if (
(parnode && !parnode->backtrack_empty()
) ||
!currnode->misc_empty() ||
!currnode->read_from_empty() ||
!currnode->future_value_empty() ||
!currnode->misc_empty() ||
!currnode->read_from_empty() ||
!currnode->future_value_empty() ||
@@
-1427,7
+1435,7
@@
void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
action_list_t::reverse_iterator ritcopy = rit;
//See if we have enough reads from the same value
int count = 0;
action_list_t::reverse_iterator ritcopy = rit;
//See if we have enough reads from the same value
int count = 0;
- for (; count < params.maxreads; rit++,count++) {
+ for (; count < params.maxreads; rit++,
count++) {
if (rit == list->rend())
return;
ModelAction *act = *rit;
if (rit == list->rend())
return;
ModelAction *act = *rit;
@@
-1447,7
+1455,7
@@
void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
if (write == rf)
continue;
if (write == rf)
continue;
- /* Test to see whether this is a feasible write to read from*/
+ /* Test to see whether this is a feasible write to read from
*/
mo_graph->startChanges();
r_modification_order(curr, write);
bool feasiblereadfrom = !is_infeasible();
mo_graph->startChanges();
r_modification_order(curr, write);
bool feasiblereadfrom = !is_infeasible();
@@
-1460,10
+1468,10
@@
void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
bool feasiblewrite = true;
//new we need to see if this write works for everyone
bool feasiblewrite = true;
//new we need to see if this write works for everyone
- for (int loop = count; loop
>0; loop--,
rit++) {
+ for (int loop = count; loop
> 0; loop--,
rit++) {
ModelAction *act = *rit;
bool foundvalue = false;
ModelAction *act = *rit;
bool foundvalue = false;
- for (int j = 0; j
<
act->get_node()->get_read_from_size(); j++) {
+ for (int j = 0; j
<
act->get_node()->get_read_from_size(); j++) {
if (act->get_node()->get_read_from_at(j) == write) {
foundvalue = true;
break;
if (act->get_node()->get_read_from_at(j) == write) {
foundvalue = true;
break;
@@
-1619,7
+1627,7
@@
void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelActio
/* Include at most one act per-thread that "happens before" curr */
if (lastact != NULL) {
/* Include at most one act per-thread that "happens before" curr */
if (lastact != NULL) {
- if (lastact== curr) {
+ if (lastact
== curr) {
//Case 1: The resolved read is a RMW, and we need to make sure
//that the write portion of the RMW mod order after rf
//Case 1: The resolved read is a RMW, and we need to make sure
//that the write portion of the RMW mod order after rf
@@
-1765,7
+1773,7
@@
bool ModelChecker::w_modification_order(ModelAction *curr)
if (thin_air_constraint_may_allow(curr, act)) {
if (!is_infeasible() ||
(curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && !is_infeasible_ignoreRMW())) {
if (thin_air_constraint_may_allow(curr, act)) {
if (!is_infeasible() ||
(curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && !is_infeasible_ignoreRMW())) {
- struct PendingFutureValue pfv = {curr,act};
+ struct PendingFutureValue pfv = {curr,
act};
futurevalues->push_back(pfv);
}
}
futurevalues->push_back(pfv);
}
}
@@
-2408,14
+2416,14
@@
void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write)
const ModelAction *act = promise->get_action();
//Is this promise on the same location?
const ModelAction *act = promise->get_action();
//Is this promise on the same location?
- if (
act->get_location() != location
)
+ if (
act->get_location() != location
)
continue;
//same thread as the promise
continue;
//same thread as the promise
- if (
act->get_tid() == tid
) {
+ if (
act->get_tid() == tid
) {
//do we have a pwrite for the promise, if not, set it
//do we have a pwrite for the promise, if not, set it
- if (promise->get_write() == NULL
) {
+ if (promise->get_write() == NULL) {
promise->set_write(write);
//The pwrite cannot happen before the promise
if (write->happens_before(act) && (write != act)) {
promise->set_write(write);
//The pwrite cannot happen before the promise
if (write->happens_before(act) && (write != act)) {
@@
-2433,7
+2441,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 (promise->get_write()
&&
mo_graph->checkReachable(promise->get_write(), write)) {
+ if (promise->get_write()
&&
mo_graph->checkReachable(promise->get_write(), write)) {
if (promise->increment_threads(tid)) {
priv->failed_promise = true;
return;
if (promise->increment_threads(tid)) {
priv->failed_promise = true;
return;
@@
-2503,14
+2511,8
@@
void ModelChecker::build_reads_from_past(ModelAction *curr)
else if (curr->get_sleep_flag() && !curr->is_seqcst() && !sleep_can_read_from(curr, act))
allow_read = false;
else if (curr->get_sleep_flag() && !curr->is_seqcst() && !sleep_can_read_from(curr, act))
allow_read = false;
- if (allow_read) {
- DEBUG("Adding action to may_read_from:\n");
- if (DBG_ENABLED()) {
- act->print();
- curr->print();
- }
+ if (allow_read)
curr->get_node()->add_read_from(act);
curr->get_node()->add_read_from(act);
- }
/* Include at most one act per-thread that "happens before" curr */
if (act->happens_before(curr))
/* Include at most one act per-thread that "happens before" curr */
if (act->happens_before(curr))
@@
-2582,16
+2584,16
@@
static void print_list(action_list_t *list, int exec_num = -1)
void ModelChecker::dumpGraph(char *filename) const
{
char buffer[200];
void ModelChecker::dumpGraph(char *filename) const
{
char buffer[200];
- sprintf(buffer, "%s.dot",filename);
+ sprintf(buffer, "%s.dot",
filename);
FILE *file = fopen(buffer, "w");
FILE *file = fopen(buffer, "w");
- fprintf(file, "digraph %s {\n",filename);
+ fprintf(file, "digraph %s {\n",
filename);
mo_graph->dumpNodes(file);
mo_graph->dumpNodes(file);
- ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *)
*
get_num_threads());
+ ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *)
*
get_num_threads());
for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) {
ModelAction *action = *it;
if (action->is_read()) {
for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) {
ModelAction *action = *it;
if (action->is_read()) {
- fprintf(file, "N%u [label=\"%u, T%u\"];\n", action->get_seq_number(),action->get_seq_number(), action->get_tid());
+ fprintf(file, "N%u [label=\"%u, T%u\"];\n", action->get_seq_number(),
action->get_seq_number(), action->get_tid());
if (action->get_reads_from() != NULL)
fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
}
if (action->get_reads_from() != NULL)
fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
}
@@
-2601,7
+2603,7
@@
void ModelChecker::dumpGraph(char *filename) const
thread_array[action->get_tid()] = action;
}
thread_array[action->get_tid()] = action;
}
- fprintf(file,"}\n");
+ fprintf(file,
"}\n");
model_free(thread_array);
fclose(file);
}
model_free(thread_array);
fclose(file);
}
@@
-2722,12
+2724,7
@@
bool ModelChecker::take_step(ModelAction *curr)
Thread *curr_thrd = get_thread(curr);
ASSERT(curr_thrd->get_state() == THREAD_READY);
Thread *curr_thrd = get_thread(curr);
ASSERT(curr_thrd->get_state() == THREAD_READY);
- Thread *next_thrd = check_current_action(curr);
-
- if (curr_thrd->is_blocked() || curr_thrd->is_complete())
- scheduler->remove_thread(curr_thrd);
-
- next_thrd = scheduler->next_thread(next_thrd);
+ curr = check_current_action(curr);
/* Infeasible -> don't take any more steps */
if (is_infeasible())
/* Infeasible -> don't take any more steps */
if (is_infeasible())
@@
-2737,11
+2734,15
@@
bool ModelChecker::take_step(ModelAction *curr)
return false;
}
return false;
}
- if (params.bound != 0)
{
- if (priv->used_sequence_numbers > params.bound)
{
+ if (params.bound != 0)
+ if (priv->used_sequence_numbers > params.bound)
return false;
return false;
- }
- }
+
+ if (curr_thrd->is_blocked() || curr_thrd->is_complete())
+ scheduler->remove_thread(curr_thrd);
+
+ Thread *next_thrd = get_next_thread(curr);
+ next_thrd = scheduler->next_thread(next_thrd);
DEBUG("(%d, %d)\n", curr_thrd ? id_to_int(curr_thrd->get_id()) : -1,
next_thrd ? id_to_int(next_thrd->get_id()) : -1);
DEBUG("(%d, %d)\n", curr_thrd ? id_to_int(curr_thrd->get_id()) : -1,
next_thrd ? id_to_int(next_thrd->get_id()) : -1);