#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()
{
DBG();
num_executions++;
+
if (isfinalfeasible()) {
printf("Earliest divergence point since last feasible execution:\n");
if (earliest_diverge)
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();
//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
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)