* the release seq? */
bool future_ordered = false;
+ ModelAction *last = get_last_action(int_to_id(i));
+ if (last && rf->happens_before(last))
+ future_ordered = true;
+
for (rit = list->rbegin(); rit != list->rend(); rit++) {
const ModelAction *act = *rit;
- if (!act->is_write())
- continue;
/* Reach synchronization -> this thread is complete */
if (act->happens_before(release))
break;
continue;
}
+ /* Only writes can break release sequences */
+ if (!act->is_write())
+ continue;
+
/* Check modification order */
if (mo_graph->checkReachable(rf, act)) {
/* rf --mo--> act */
(*thrd_last_action)[tid] = act;
}
-ModelAction * ModelChecker::get_last_action(thread_id_t tid)
+/**
+ * @brief Get the last action performed by a particular Thread
+ * @param tid The thread ID of the Thread in question
+ * @return The last action in the thread
+ */
+ModelAction * ModelChecker::get_last_action(thread_id_t tid) const
{
- int threadid=id_to_int(tid);
- if (threadid<(int)thrd_last_action->size())
+ int threadid = id_to_int(tid);
+ if (threadid < (int)thrd_last_action->size())
return (*thrd_last_action)[id_to_int(tid)];
else
return NULL;
* check
* @return The last seq_cst write
*/
-ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr)
+ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr) const
{
void *location = curr->get_location();
action_list_t *list = obj_map->get_safe_ptr(location);
}
/**
- * Gets the last unlock operation
- * performed on a particular mutex (i.e., memory location).
+ * Gets the last unlock operation performed on a particular mutex (i.e., memory
+ * location). This function identifies the mutex according to the current
+ * action, which is presumed to perform on the same mutex.
* @param curr The current ModelAction; also denotes the object location to
* check
* @return The last unlock operation
*/
-
-ModelAction * ModelChecker::get_last_unlock(ModelAction *curr)
+ModelAction * ModelChecker::get_last_unlock(ModelAction *curr) const
{
void *location = curr->get_location();
action_list_t *list = obj_map->get_safe_ptr(location);
- /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
+ /* 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++)
if ((*rit)->is_unlock())
#if SUPPORT_MOD_ORDER_DUMP
scheduler->print();
char buffername[100];
- sprintf(buffername, "exec%u",num_executions);
+ sprintf(buffername, "exec%04u", num_executions);
mo_graph->dumpGraphToFile(buffername);
#endif