action_type get_type() { return type; }
memory_order get_mo() { return order; }
void * get_location() { return location; }
+ int get_seq_number() { return seq_number; }
TreeNode * get_node() { return node; }
void set_node(TreeNode *n) { node = n; }
thread_id_t tid;
int value;
TreeNode *node;
+ int seq_number;
};
typedef std::list<class ModelAction *> action_list_t;
{
/* First thread created will have id (INITIAL_THREAD_ID + 1) */
this->used_thread_id = INITIAL_THREAD_ID;
+ used_sequence_numbers = 0;
/* Initialize default scheduler */
this->scheduler = new Scheduler();
currentNode = rootNode;
current_action = NULL;
used_thread_id = INITIAL_THREAD_ID;
+ used_sequence_numbers = 0;
/* scheduler reset ? */
}
return ++used_thread_id;
}
+int ModelChecker::get_next_seq_num()
+{
+ return ++used_sequence_numbers;
+}
+
Thread * ModelChecker::schedule_next_thread()
{
Thread *t;
act->location = loc;
act->tid = t->get_id();
act->value = value;
+ act->seq_number = model->get_next_seq_num();
}
bool ModelAction::is_read()
type_str = "unknown type";
}
- printf("Thread: %d\tAction: %s\tMO: %d\tLoc: %14p\tValue: %d\n",
- id_to_int(tid), type_str, order, location, value);
+ printf("(%4d) Thread: %d\tAction: %s\tMO: %d\tLoc: %14p\tValue: %d\n",
+ seq_number, id_to_int(tid), type_str, order, location, value);
}
Thread * get_thread(thread_id_t tid) { return thread_map[id_to_int(tid)]; }
thread_id_t get_next_id();
+ int get_next_seq_num();
int switch_to_master(ModelAction *act);
bool next_execution();
private:
int used_thread_id;
+ int used_sequence_numbers;
int num_executions;
ModelAction * get_last_conflict(ModelAction *act);