snapshotObject->backTrackBeforeStep(0);
}
-/** @returns a thread ID for a new Thread */
+/** @return a thread ID for a new Thread */
thread_id_t ModelChecker::get_next_id()
{
return priv->next_thread_id++;
}
-/** @returns the number of user threads created during this execution */
+/** @return the number of user threads created during this execution */
int ModelChecker::get_num_threads()
{
return priv->next_thread_id;
}
-/** @returns a sequence number for a new ModelAction */
+/** @return a sequence number for a new ModelAction */
modelclock_t ModelChecker::get_next_seq_num()
{
return ++priv->used_sequence_numbers;
ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
{
- action_type type = act->get_type();
-
- if (type==ATOMIC_READ||type==ATOMIC_WRITE||type==ATOMIC_RMW) {
+ switch (act->get_type()) {
+ case ATOMIC_READ:
+ case ATOMIC_WRITE:
+ case ATOMIC_RMW: {
/* linear search: from most recent to oldest */
action_list_t *list = obj_map->get_safe_ptr(act->get_location());
action_list_t::reverse_iterator rit;
if (act->is_synchronizing(prev))
return prev;
}
- } else if (type==ATOMIC_LOCK||type==ATOMIC_TRYLOCK) {
+ break;
+ }
+ case ATOMIC_LOCK:
+ case ATOMIC_TRYLOCK: {
/* linear search: from most recent to oldest */
action_list_t *list = obj_map->get_safe_ptr(act->get_location());
action_list_t::reverse_iterator rit;
if (act->is_conflicting_lock(prev))
return prev;
}
- } else if (type==ATOMIC_UNLOCK) {
+ break;
+ }
+ case ATOMIC_UNLOCK: {
/* linear search: from most recent to oldest */
action_list_t *list = obj_map->get_safe_ptr(act->get_location());
action_list_t::reverse_iterator rit;
if (!act->same_thread(prev)&&prev->is_failed_trylock())
return prev;
}
+ break;
+ }
+ default:
+ break;
}
return NULL;
}
+/** This method find backtracking points where we should try to
+ * reorder the parameter ModelAction against.
+ *
+ * @param the ModelAction to find backtracking points for.
+ */
+
+
void ModelChecker::set_backtracking(ModelAction *act)
{
Thread *t = get_thread(act);
}
}
+/**
+ * Processes a lock, trylock, or unlock model action. @param curr is
+ * the read model action to process.
+ *
+ * The try lock operation checks whether the lock is taken. If not,
+ * it falls to the normal lock operation case. If so, it returns
+ * fail.
+ *
+ * The lock operation has already been checked that it is enabled, so
+ * it just grabs the lock and synchronizes with the previous unlock.
+ *
+ * The unlock operation has to re-enable all of the threads that are
+ * waiting on the lock.
+ */
+
void ModelChecker::process_mutex(ModelAction *curr) {
std::mutex * mutex=(std::mutex *) curr->get_location();
struct std::mutex_state * state=mutex->get_state();
action_list_t * waiters = lock_waiters_map->get_safe_ptr(curr->get_location());
//activate all the waiting threads
for(action_list_t::iterator rit = waiters->begin(); rit!=waiters->end(); rit++) {
- add_thread(get_thread((*rit)->get_tid()));
+ scheduler->add_thread(get_thread((*rit)->get_tid()));
}
waiters->clear();
break;
return newcurr;
}
+/**
+ * This method checks whether a model action is enabled at the given point.
+ * At this point, it checks whether a lock operation would be successful at this point.
+ * If not, it puts the thread in a waiter list.
+ * @param curr is the ModelAction to check whether it is enabled.
+ * @return a bool that indicates whether the action is enabled.
+ */
+
bool ModelChecker::check_action_enabled(ModelAction *curr) {
if (curr->is_lock()) {
std::mutex * lock=(std::mutex *) curr->get_location();
return false;
}
-/** @returns whether the current partial trace must be a prefix of a
+/** @return whether the current partial trace must be a prefix of a
* feasible trace. */
bool ModelChecker::isfeasibleprefix() {
return promises->size() == 0 && *lazy_sync_size == 0;
}
-/** @returns whether the current partial trace is feasible. */
+/** @return whether the current partial trace is feasible. */
bool ModelChecker::isfeasible() {
return !mo_graph->checkForRMWViolation() && isfeasibleotherthanRMW();
}
-/** @returns whether the current partial trace is feasible other than
+/** @return whether the current partial trace is feasible other than
* multiple RMW reading from the same store. */
bool ModelChecker::isfeasibleotherthanRMW() {
if (DBG_ENABLED()) {
return NULL;
}
+/**
+ * Gets the last unlock operation
+ * performed on a particular mutex (i.e., memory location).
+ * @param curr The current ModelAction; also denotes the object location to
+ * check
+ * @return The last unlock operation
+ */
+
ModelAction * ModelChecker::get_last_unlock(ModelAction *curr)
{
void *location = curr->get_location();
scheduler->add_thread(t);
}
+/**
+ * Removes a thread from the scheduler.
+ * @param the thread to remove.
+ */
+
void ModelChecker::remove_thread(Thread *t)
{
scheduler->remove_thread(t);
projects / model-checker.git / blobdiff