projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
datarace: don't export unrealized race vector
[model-checker.git]
/
execution.cc
diff --git
a/execution.cc
b/execution.cc
index e038961d211ca074c0b8deece5fe5fab7eccde51..c8c4b89ac2910abd7024b531ea1bed5e97187faa 100644
(file)
--- a/
execution.cc
+++ b/
execution.cc
@@
-64,9
+64,9
@@
ModelExecution::ModelExecution(ModelChecker *m,
model(m),
params(params),
scheduler(scheduler),
model(m),
params(params),
scheduler(scheduler),
- action_trace(
new action_list_t()
),
- thread_map(
),
- obj_map(
new HashTable<const void *, action_list_t *, uintptr_t, 4>()
),
+ action_trace(),
+ thread_map(
2), /* We'll always need at least 2 threads */
+ obj_map(),
condvar_waiters_map(),
obj_thrd_map(),
promises(),
condvar_waiters_map(),
obj_thrd_map(),
promises(),
@@
-80,18
+80,16
@@
ModelExecution::ModelExecution(ModelChecker *m,
{
/* Initialize a model-checker thread, for special ModelActions */
model_thread = new Thread(get_next_id());
{
/* Initialize a model-checker thread, for special ModelActions */
model_thread = new Thread(get_next_id());
-
thread_map.put(id_to_int(model_thread->get_id()),
model_thread);
+
add_thread(
model_thread);
scheduler->register_engine(this);
scheduler->register_engine(this);
+ node_stack->register_engine(this);
}
/** @brief Destructor */
ModelExecution::~ModelExecution()
{
for (unsigned int i = 0; i < get_num_threads(); i++)
}
/** @brief Destructor */
ModelExecution::~ModelExecution()
{
for (unsigned int i = 0; i < get_num_threads(); i++)
- delete thread_map.get(i);
-
- delete obj_map;
- delete action_trace;
+ delete get_thread(int_to_id(i));
for (unsigned int i = 0; i < promises.size(); i++)
delete promises[i];
for (unsigned int i = 0; i < promises.size(); i++)
delete promises[i];
@@
-309,8
+307,8
@@
ModelAction * ModelExecution::get_last_fence_conflict(ModelAction *act) const
return NULL;
/* Skip past the release */
return NULL;
/* Skip past the release */
-
action_list_t *list =
action_trace;
- action_list_t::reverse_iterator rit;
+
const action_list_t *list = &
action_trace;
+ action_list_t::
const_
reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++)
if (*rit == last_release)
break;
for (rit = list->rbegin(); rit != list->rend(); rit++)
if (*rit == last_release)
break;
@@
-368,17
+366,22
@@
ModelAction * ModelExecution::get_last_fence_conflict(ModelAction *act) const
ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const
{
switch (act->get_type()) {
ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const
{
switch (act->get_type()) {
- /* case ATOMIC_FENCE: fences don't directly cause backtracking */
+ case ATOMIC_FENCE:
+ /* Only seq-cst fences can (directly) cause backtracking */
+ if (!act->is_seqcst())
+ break;
case ATOMIC_READ:
case ATOMIC_WRITE:
case ATOMIC_RMW: {
ModelAction *ret = NULL;
/* linear search: from most recent to oldest */
case ATOMIC_READ:
case ATOMIC_WRITE:
case ATOMIC_RMW: {
ModelAction *ret = NULL;
/* linear search: from most recent to oldest */
- action_list_t *list =
get_safe_ptr_action(obj_map,
act->get_location());
+ action_list_t *list =
obj_map.get(
act->get_location());
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 (prev == act)
+ continue;
if (prev->could_synchronize_with(act)) {
ret = prev;
break;
if (prev->could_synchronize_with(act)) {
ret = prev;
break;
@@
-397,7
+400,7
@@
ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const
case ATOMIC_LOCK:
case ATOMIC_TRYLOCK: {
/* linear search: from most recent to oldest */
case ATOMIC_LOCK:
case ATOMIC_TRYLOCK: {
/* linear search: from most recent to oldest */
- action_list_t *list =
get_safe_ptr_action(obj_map,
act->get_location());
+ action_list_t *list =
obj_map.get(
act->get_location());
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;
@@
-408,7
+411,7
@@
ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const
}
case ATOMIC_UNLOCK: {
/* linear search: from most recent to oldest */
}
case ATOMIC_UNLOCK: {
/* linear search: from most recent to oldest */
- action_list_t *list =
get_safe_ptr_action(obj_map,
act->get_location());
+ action_list_t *list =
obj_map.get(
act->get_location());
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;
@@
-419,7
+422,7
@@
ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const
}
case ATOMIC_WAIT: {
/* linear search: from most recent to oldest */
}
case ATOMIC_WAIT: {
/* linear search: from most recent to oldest */
- action_list_t *list =
get_safe_ptr_action(obj_map,
act->get_location());
+ action_list_t *list =
obj_map.get(
act->get_location());
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;
@@
-434,7
+437,7
@@
ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const
case ATOMIC_NOTIFY_ALL:
case ATOMIC_NOTIFY_ONE: {
/* linear search: from most recent to oldest */
case ATOMIC_NOTIFY_ALL:
case ATOMIC_NOTIFY_ONE: {
/* linear search: from most recent to oldest */
- action_list_t *list =
get_safe_ptr_action(obj_map,
act->get_location());
+ action_list_t *list =
obj_map.get(
act->get_location());
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;
@@
-856,7
+859,7
@@
bool ModelExecution::process_fence(ModelAction *curr)
*/
bool updated = false;
if (curr->is_acquire()) {
*/
bool updated = false;
if (curr->is_acquire()) {
- action_list_t *list = action_trace;
+ action_list_t *list =
&
action_trace;
action_list_t::reverse_iterator rit;
/* Find X : is_read(X) && X --sb-> curr */
for (rit = list->rbegin(); rit != list->rend(); rit++) {
action_list_t::reverse_iterator rit;
/* Find X : is_read(X) && X --sb-> curr */
for (rit = list->rbegin(); rit != list->rend(); rit++) {
@@
-1004,7
+1007,7
@@
void ModelExecution::process_relseq_fixup(ModelAction *curr, work_queue_t *work_
work_queue->push_back(MOEdgeWorkEntry(acquire));
/* propagate synchronization to later actions */
work_queue->push_back(MOEdgeWorkEntry(acquire));
/* propagate synchronization to later actions */
- action_list_t::reverse_iterator rit = action_trace
->
rbegin();
+ action_list_t::reverse_iterator rit = action_trace
.
rbegin();
for (; (*rit) != acquire; rit++) {
ModelAction *propagate = *rit;
if (acquire->happens_before(propagate)) {
for (; (*rit) != acquire; rit++) {
ModelAction *propagate = *rit;
if (acquire->happens_before(propagate)) {
@@
-1211,7
+1214,7
@@
bool ModelExecution::check_action_enabled(ModelAction *curr) {
*
* @param curr The current action to process
* @return The ModelAction that is actually executed; may be different than
*
* @param curr The current action to process
* @return The ModelAction that is actually executed; may be different than
- * curr
; may be NULL, if the current action is not enabled to run
+ * curr
*/
ModelAction * ModelExecution::check_current_action(ModelAction *curr)
{
*/
ModelAction * ModelExecution::check_current_action(ModelAction *curr)
{
@@
-2077,7
+2080,7
@@
bool ModelExecution::resolve_release_sequences(void *location, work_queue_t *wor
work_queue->push_back(MOEdgeWorkEntry(acquire));
/* propagate synchronization to later actions */
work_queue->push_back(MOEdgeWorkEntry(acquire));
/* propagate synchronization to later actions */
- action_list_t::reverse_iterator rit = action_trace
->
rbegin();
+ action_list_t::reverse_iterator rit = action_trace
.
rbegin();
for (; (*rit) != acquire; rit++) {
ModelAction *propagate = *rit;
if (acquire->happens_before(propagate)) {
for (; (*rit) != acquire; rit++) {
ModelAction *propagate = *rit;
if (acquire->happens_before(propagate)) {
@@
-2113,7
+2116,7
@@
void ModelExecution::add_action_to_lists(ModelAction *act)
int tid = id_to_int(act->get_tid());
ModelAction *uninit = NULL;
int uninit_id = -1;
int tid = id_to_int(act->get_tid());
ModelAction *uninit = NULL;
int uninit_id = -1;
- action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
+ action_list_t *list = get_safe_ptr_action(
&
obj_map, act->get_location());
if (list->empty() && act->is_atomic_var()) {
uninit = get_uninitialized_action(act);
uninit_id = id_to_int(uninit->get_tid());
if (list->empty() && act->is_atomic_var()) {
uninit = get_uninitialized_action(act);
uninit_id = id_to_int(uninit->get_tid());
@@
-2121,9
+2124,9
@@
void ModelExecution::add_action_to_lists(ModelAction *act)
}
list->push_back(act);
}
list->push_back(act);
- action_trace
->
push_back(act);
+ action_trace
.
push_back(act);
if (uninit)
if (uninit)
- action_trace
->
push_front(uninit);
+ action_trace
.
push_front(uninit);
SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
if (tid >= (int)vec->size())
SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
if (tid >= (int)vec->size())
@@
-2146,7
+2149,7
@@
void ModelExecution::add_action_to_lists(ModelAction *act)
if (act->is_wait()) {
void *mutex_loc = (void *) act->get_value();
if (act->is_wait()) {
void *mutex_loc = (void *) act->get_value();
- get_safe_ptr_action(obj_map, mutex_loc)->push_back(act);
+ get_safe_ptr_action(
&
obj_map, mutex_loc)->push_back(act);
SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
if (tid >= (int)vec->size())
SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
if (tid >= (int)vec->size())
@@
-2194,7
+2197,7
@@
ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
{
void *location = curr->get_location();
ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
{
void *location = curr->get_location();
- action_list_t *list =
get_safe_ptr_action(obj_map,
location);
+ action_list_t *list =
obj_map.get(
location);
/* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); (*rit) != curr; rit++)
/* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); (*rit) != curr; rit++)
@@
-2216,8
+2219,12
@@
ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
*/
ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
{
*/
ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
{
- /* All fences should have NULL location */
- action_list_t *list = get_safe_ptr_action(obj_map, NULL);
+ /* All fences should have location FENCE_LOCATION */
+ action_list_t *list = obj_map.get(FENCE_LOCATION);
+
+ if (!list)
+ return NULL;
+
action_list_t::reverse_iterator rit = list->rbegin();
if (before_fence) {
action_list_t::reverse_iterator rit = list->rbegin();
if (before_fence) {
@@
-2246,7
+2253,7
@@
ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const Mode
ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
{
void *location = curr->get_location();
ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
{
void *location = curr->get_location();
- action_list_t *list =
get_safe_ptr_action(obj_map,
location);
+ action_list_t *list =
obj_map.get(
location);
/* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++)
/* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++)
@@
-2581,9
+2588,9
@@
ModelAction * ModelExecution::get_uninitialized_action(const ModelAction *curr)
return act;
}
return act;
}
-static void print_list(action_list_t *list)
+static void print_list(
const
action_list_t *list)
{
{
- action_list_t::iterator it;
+ action_list_t::
const_
iterator it;
model_print("---------------------------------------------------------------------\n");
model_print("---------------------------------------------------------------------\n");
@@
-2609,7
+2616,7
@@
void ModelExecution::dumpGraph(char *filename) const
mo_graph->dumpNodes(file);
ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
mo_graph->dumpNodes(file);
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++) {
+ for (action_list_t::iterator it = action_trace
.begin(); it != action_trace.
end(); it++) {
ModelAction *act = *it;
if (act->is_read()) {
mo_graph->dot_print_node(file, act);
ModelAction *act = *it;
if (act->is_read()) {
mo_graph->dot_print_node(file, act);
@@
-2657,7
+2664,7
@@
void ModelExecution::print_summary() const
model_print("\n");
} else
print_infeasibility(" INFEASIBLE");
model_print("\n");
} else
print_infeasibility(" INFEASIBLE");
- print_list(action_trace);
+ print_list(
&
action_trace);
model_print("\n");
if (!promises.empty()) {
model_print("Pending promises:\n");
model_print("\n");
if (!promises.empty()) {
model_print("Pending promises:\n");
@@
-2676,7
+2683,10
@@
void ModelExecution::print_summary() const
*/
void ModelExecution::add_thread(Thread *t)
{
*/
void ModelExecution::add_thread(Thread *t)
{
- thread_map.put(id_to_int(t->get_id()), t);
+ unsigned int i = id_to_int(t->get_id());
+ if (i >= thread_map.size())
+ thread_map.resize(i + 1);
+ thread_map[i] = t;
if (!t->is_model_thread())
scheduler->add_thread(t);
}
if (!t->is_model_thread())
scheduler->add_thread(t);
}
@@
-2688,7
+2698,10
@@
void ModelExecution::add_thread(Thread *t)
*/
Thread * ModelExecution::get_thread(thread_id_t tid) const
{
*/
Thread * ModelExecution::get_thread(thread_id_t tid) const
{
- return thread_map.get(id_to_int(tid));
+ unsigned int i = id_to_int(tid);
+ if (i < thread_map.size())
+ return thread_map[i];
+ return NULL;
}
/**
}
/**
@@
-2803,7
+2816,7
@@
void ModelExecution::fixup_release_sequences()
{
while (!pending_rel_seqs.empty() &&
is_feasible_prefix_ignore_relseq() &&
{
while (!pending_rel_seqs.empty() &&
is_feasible_prefix_ignore_relseq() &&
-
!unrealizedraces.empty
()) {
+
haveUnrealizedRaces
()) {
model_print("*** WARNING: release sequence fixup action "
"(%zu pending release seuqence(s)) ***\n",
pending_rel_seqs.size());
model_print("*** WARNING: release sequence fixup action "
"(%zu pending release seuqence(s)) ***\n",
pending_rel_seqs.size());