#include "promise.h"
#include "datarace.h"
#include "mutex.h"
+#include "threads.h"
#define INITIAL_THREAD_ID 0
return priv->next_thread_id;
}
+/** @return The currently executing Thread. */
+Thread * ModelChecker::get_current_thread()
+{
+ return scheduler->get_current_thread();
+}
+
/** @return a sequence number for a new ModelAction */
modelclock_t ModelChecker::get_next_seq_num()
{
}
} else {
const ModelAction *prevreadfrom = act->get_reads_from();
- if (prevreadfrom != NULL && rf != prevreadfrom) {
+ //if the previous read is unresolved, keep going...
+ if (prevreadfrom == NULL)
+ continue;
+
+ if (rf != prevreadfrom) {
mo_graph->addEdge(prevreadfrom, rf);
added = true;
}
ModelAction *act = *rit;
if (act == curr) {
/*
- * If RMW, we already have all relevant edges,
- * so just skip to next thread.
- * If normal write, we need to look at earlier
- * actions, so continue processing list.
+ * 1) If RMW and it actually read from something, then we
+ * already have all relevant edges, so just skip to next
+ * thread.
+ *
+ * 2) If RMW and it didn't read from anything, we should
+ * whatever edge we can get to speed up convergence.
+ *
+ * 3) If normal write, we need to look at earlier actions, so
+ * continue processing list.
*/
- if (curr->is_rmw())
- break;
- else
+ if (curr->is_rmw()) {
+ if (curr->get_reads_from()!=NULL)
+ break;
+ else
+ continue;
+ } else
continue;
}
*/
if (act->is_write())
mo_graph->addEdge(act, curr);
- else if (act->is_read() && act->get_reads_from() != NULL)
+ else if (act->is_read()) {
+ //if previous read accessed a null, just keep going
+ if (act->get_reads_from() == NULL)
+ continue;
mo_graph->addEdge(act->get_reads_from(), curr);
+ }
added = true;
break;
} else if (act->is_read() && !act->is_synchronizing(curr) &&
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 -> 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());
}
if (thread_array[action->get_tid()] != NULL) {
fprintf(file, "N%u -> N%u[label=\"sb\", color=blue];\n", thread_array[action->get_tid()]->get_seq_number(), action->get_seq_number());
scheduler->remove_thread(t);
}
+/**
+ * @brief Get a Thread reference by its ID
+ * @param tid The Thread's ID
+ * @return A Thread reference
+ */
+Thread * ModelChecker::get_thread(thread_id_t tid)
+{
+ return thread_map->get(id_to_int(tid));
+}
+
+/**
+ * @brief Get a reference to the Thread in which a ModelAction was executed
+ * @param act The ModelAction
+ * @return A Thread reference
+ */
+Thread * ModelChecker::get_thread(ModelAction *act)
+{
+ return get_thread(act->get_tid());
+}
+
/**
* Switch from a user-context to the "master thread" context (a.k.a. system
* context). This switch is made with the intention of exploring a particular
* model-checking action (described by a ModelAction object). Must be called
* from a user-thread context.
- * @param act The current action that will be explored. Must not be NULL.
+ *
+ * @param act The current action that will be explored. May be NULL only if
+ * trace is exiting via an assertion (see ModelChecker::set_assert and
+ * ModelChecker::has_asserted).
* @return Return status from the 'swap' call (i.e., success/fail, 0/-1)
*/
int ModelChecker::switch_to_master(ModelAction *act)