action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *prev = *rit;
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *prev = *rit;
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *prev = *rit;
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *prev = *rit;
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *prev = *rit;
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *prev = *rit;
if (curr->is_trylock() || curr->is_lock() || curr->is_unlock()) {
mutex = (std::mutex *)curr->get_location();
state = mutex->get_state();
if (curr->is_trylock() || curr->is_lock() || curr->is_unlock()) {
mutex = (std::mutex *)curr->get_location();
state = mutex->get_state();
mo_graph->startChanges();
r_modification_order(curr, write);
bool feasiblereadfrom = !is_infeasible();
mo_graph->startChanges();
r_modification_order(curr, write);
bool feasiblereadfrom = !is_infeasible();
//Case 1: The resolved read is a RMW, and we need to make sure
//that the write portion of the RMW mod order after rf
//Case 1: The resolved read is a RMW, and we need to make sure
//that the write portion of the RMW mod order after rf
if (thin_air_constraint_may_allow(curr, act)) {
if (!is_infeasible() ||
(curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && !is_infeasible_ignoreRMW())) {
if (thin_air_constraint_may_allow(curr, act)) {
if (!is_infeasible() ||
(curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && !is_infeasible_ignoreRMW())) {
promise->set_write(write);
//The pwrite cannot happen before the promise
if (write->happens_before(act) && (write != act)) {
promise->set_write(write);
//The pwrite cannot happen before the promise
if (write->happens_before(act) && (write != act)) {
for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) {
ModelAction *action = *it;
if (action->is_read()) {
for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) {
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 [label=\"%u, T%u\"];\n", action->get_seq_number(), action->get_seq_number(), action->get_tid());
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 (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());
}