#include "threads-model.h"
#include "output.h"
#include "traceanalysis.h"
+#include "bugmessage.h"
#define INITIAL_THREAD_ID 0
ModelChecker *model;
-struct bug_message {
- bug_message(const char *str) {
- const char *fmt = " [BUG] %s\n";
- msg = (char *)snapshot_malloc(strlen(fmt) + strlen(str));
- sprintf(msg, fmt, str);
- }
- ~bug_message() { if (msg) snapshot_free(msg); }
-
- char *msg;
- void print() { model_print("%s", msg); }
-
- SNAPSHOTALLOC
-};
-
/**
* Structure for holding small ModelChecker members that should be snapshotted
*/
thrd_last_action(new SnapVector<ModelAction *>(1)),
thrd_last_fence_release(new SnapVector<ModelAction *>()),
node_stack(new NodeStack()),
- trace_analyses(new ModelVector<Trace_Analysis *>()),
+ trace_analyses(new ModelVector<TraceAnalysis *>()),
priv(new struct model_snapshot_members()),
mo_graph(new CycleGraph())
{
delete thrd_last_action;
delete thrd_last_fence_release;
delete node_stack;
- for (unsigned int i = 0; i <trace_analyses->size();i++)
+ for (unsigned int i = 0; i < trace_analyses->size(); i++)
delete (*trace_analyses)[i];
delete trace_analyses;
delete scheduler;
return true;
}
-/**
- * @brief Run trace analyses on complete trace. */
-
+/** @brief Run trace analyses on complete trace */
void ModelChecker::run_trace_analyses() {
- for(unsigned int i=0; i < trace_analyses->size(); i++) {
+ for (unsigned int i = 0; i < trace_analyses->size(); i++)
(*trace_analyses)[i]->analyze(action_trace);
- }
}
/**
ModelAction *unlock = get_last_unlock(curr);
//synchronize with the previous unlock statement
if (unlock != NULL) {
- curr->synchronize_with(unlock);
+ synchronize(unlock, curr);
return true;
}
break;
rel_heads_list_t release_heads;
get_release_seq_heads(curr, act, &release_heads);
for (unsigned int i = 0; i < release_heads.size(); i++)
- if (!curr->synchronize_with(release_heads[i]))
- set_bad_synchronization();
+ synchronize(release_heads[i], curr);
if (release_heads.size() != 0)
updated = true;
}
case THREAD_JOIN: {
Thread *blocking = curr->get_thread_operand();
ModelAction *act = get_last_action(blocking->get_id());
- curr->synchronize_with(act);
+ synchronize(act, curr);
updated = true; /* trigger rel-seq checks */
break;
}
*/
/* Must synchronize */
- if (!acquire->synchronize_with(release)) {
- set_bad_synchronization();
+ if (!synchronize(release, acquire))
return;
- }
/* Re-check all pending release sequences */
work_queue->push_back(CheckRelSeqWorkEntry(NULL));
/* Re-check act for mo_graph edges */
for (; (*rit) != acquire; rit++) {
ModelAction *propagate = *rit;
if (acquire->happens_before(propagate)) {
- propagate->synchronize_with(acquire);
+ synchronize(acquire, propagate);
/* Re-check 'propagate' for mo_graph edges */
work_queue->push_back(MOEdgeWorkEntry(propagate));
}
get_release_seq_heads(act, act, &release_heads);
int num_heads = release_heads.size();
for (unsigned int i = 0; i < release_heads.size(); i++)
- if (!act->synchronize_with(release_heads[i])) {
- set_bad_synchronization();
+ if (!synchronize(release_heads[i], act))
num_heads--;
- }
return num_heads > 0;
}
return false;
}
+/**
+ * @brief Synchronizes two actions
+ *
+ * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
+ * This function performs the synchronization as well as providing other hooks
+ * for other checks along with synchronization.
+ *
+ * @param first The left-hand side of the synchronizes-with relation
+ * @param second The right-hand side of the synchronizes-with relation
+ * @return True if the synchronization was successful (i.e., was consistent
+ * with the execution order); false otherwise
+ */
+bool ModelChecker::synchronize(const ModelAction *first, ModelAction *second)
+{
+ if (*second < *first) {
+ set_bad_synchronization();
+ return false;
+ }
+ check_promises(first->get_tid(), second->get_cv(), first->get_cv());
+ return second->synchronize_with(first);
+}
+
/**
* Check promises and eliminate potentially-satisfying threads when a thread is
* blocked (e.g., join, lock). A thread which is waiting on another thread can
rel_heads_list_t release_heads;
bool complete;
complete = release_seq_heads(rf, &release_heads, pending);
- for (unsigned int i = 0; i < release_heads.size(); i++) {
- if (!acquire->has_synchronized_with(release_heads[i])) {
- if (acquire->synchronize_with(release_heads[i]))
+ for (unsigned int i = 0; i < release_heads.size(); i++)
+ if (!acquire->has_synchronized_with(release_heads[i]))
+ if (synchronize(release_heads[i], acquire))
updated = true;
- else
- set_bad_synchronization();
- }
- }
if (updated) {
/* Re-check all pending release sequences */
for (; (*rit) != acquire; rit++) {
ModelAction *propagate = *rit;
if (acquire->happens_before(propagate)) {
- propagate->synchronize_with(acquire);
+ synchronize(acquire, propagate);
/* Re-check 'propagate' for mo_graph edges */
work_queue->push_back(MOEdgeWorkEntry(propagate));
}
user_main(model->params.argc, model->params.argv);
}
+/** @return True if the execution has taken too many steps */
+bool ModelChecker::too_many_steps() const
+{
+ return params.bound != 0 && priv->used_sequence_numbers > params.bound;
+}
+
bool ModelChecker::should_terminate_execution()
{
/* Infeasible -> don't take any more steps */
return true;
}
- if (params.bound != 0 && priv->used_sequence_numbers > params.bound)
+ if (too_many_steps())
return true;
return false;
}
projects / model-checker.git / blobdiff