unsigned int next_thread_id;
modelclock_t used_sequence_numbers;
ModelAction *next_backtrack;
- std::vector< bug_message *, SnapshotAlloc<bug_message *> > bugs;
+ SnapVector<bug_message *> bugs;
struct execution_stats stats;
bool failed_promise;
bool too_many_reads;
obj_map(new HashTable<const void *, action_list_t *, uintptr_t, 4>()),
lock_waiters_map(new HashTable<const void *, action_list_t *, uintptr_t, 4>()),
condvar_waiters_map(new HashTable<const void *, action_list_t *, uintptr_t, 4>()),
- obj_thrd_map(new HashTable<void *,
snap_vector<action_list_t> *, uintptr_t, 4 >()),
- promises(new snap_vector< Promise * >()),
- futurevalues(new snap_vector< struct PendingFutureValue >()),
- pending_rel_seqs(new snap_vector< struct release_seq * >()),
- thrd_last_action(new snap_vector< ModelAction * >(1)),
- thrd_last_fence_release(new snap_vector< ModelAction * >()),
+ obj_thrd_map(new HashTable<void *,
SnapVector<action_list_t> *, uintptr_t, 4 >()),
+ promises(new SnapVector<Promise *>()),
+ futurevalues(new SnapVector<struct PendingFutureValue>()),
+ pending_rel_seqs(new SnapVector<struct release_seq *>()),
+ thrd_last_action(new SnapVector<ModelAction *>(1)),
+ thrd_last_fence_release(new SnapVector<ModelAction *>()),
node_stack(new NodeStack()),
priv(new struct model_snapshot_members()),
mo_graph(new CycleGraph())
return tmp;
}
-static
snap_vector<action_list_t> * get_safe_ptr_vect_action(HashTable<void *, snap_vector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
+static
SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<void *, SnapVector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
{
-
snap_vector<action_list_t> *tmp = hash->get(ptr);
+
SnapVector<action_list_t> *tmp = hash->get(ptr);
if (tmp == NULL) {
- tmp = new
snap_vector<action_list_t>();
+ tmp = new
SnapVector<action_list_t>();
hash->put(ptr, tmp);
}
return tmp;
* load-acquire
* or
* load --sb-> fence-acquire */
- std::vector< ModelAction *, ModelAlloc<ModelAction *> > acquire_fences(get_num_threads(), NULL);
- std::vector< ModelAction *, ModelAlloc<ModelAction *> > prior_loads(get_num_threads(), NULL);
+ ModelVector<ModelAction *> acquire_fences(get_num_threads(), NULL);
+ ModelVector<ModelAction *> prior_loads(get_num_threads(), NULL);
bool found_acquire_fences = false;
for ( ; rit != list->rend(); rit++) {
ModelAction *prev = *rit;
bool ModelChecker::process_write(ModelAction *curr)
{
/* Readers to which we may send our future value */
- std::vector< ModelAction *, ModelAlloc<ModelAction *> > send_fv;
+ ModelVector<ModelAction *> send_fv;
bool updated_mod_order = w_modification_order(curr, &send_fv);
int promise_idx = get_promise_to_resolve(curr);
if (!mo_graph->checkReachable(rf, other_rf))
return false;
-
snap_vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
+
SnapVector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
action_list_t *list = &(*thrd_lists)[id_to_int(curr->get_tid())];
action_list_t::reverse_iterator rit = list->rbegin();
ASSERT((*rit) == curr);
curr->get_node()->get_read_from_promise_size() <= 1)
return true;
-
snap_vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
+
SnapVector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
int tid = id_to_int(curr->get_tid());
ASSERT(tid < (int)thrd_lists->size());
action_list_t *list = &(*thrd_lists)[tid];
template <typename rf_type>
bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
{
-
snap_vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
+
SnapVector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
unsigned int i;
bool added = false;
ASSERT(curr->is_read());
/* Last SC fence in the current thread */
ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
+ ModelAction *last_sc_write = NULL;
+ if (curr->is_seqcst())
+ last_sc_write = get_last_seq_cst_write(curr);
/* Iterate over all threads */
for (i = 0; i < thrd_lists->size(); i++) {
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *act = *rit;
- if (act->is_write() && !act->equals(rf) && act != curr) {
+ /* Skip curr */
+ if (act == curr)
+ continue;
+ /* Don't want to add reflexive edges on 'rf' */
+ if (act->equals(rf)) {
+ if (act->happens_before(curr))
+ break;
+ else
+ continue;
+ }
+
+ if (act->is_write()) {
/* C++, Section 29.3 statement 5 */
if (curr->is_seqcst() && last_sc_fence_thread_local &&
*act < *last_sc_fence_thread_local) {
}
}
+ /* C++, Section 29.3 statement 3 (second subpoint) */
+ if (curr->is_seqcst() && last_sc_write && act == last_sc_write) {
+ added = mo_graph->addEdge(act, rf) || added;
+ break;
+ }
+
/*
* Include at most one act per-thread that "happens
- * before" curr. Don't consider reflexively.
+ * before" curr
*/
- if (act->happens_before(curr) && act != curr) {
+ if (act->happens_before(curr)) {
if (act->is_write()) {
- if (!act->equals(rf)) {
- added = mo_graph->addEdge(act, rf) || added;
- }
+ added = mo_graph->addEdge(act, rf) || added;
} else {
const ModelAction *prevrf = act->get_reads_from();
const Promise *prevrf_promise = act->get_reads_from_promise();
* value. If NULL, then don't record any future values.
* @return True if modification order edges were added; false otherwise
*/
-bool ModelChecker::w_modification_order(ModelAction *curr, std::vector< ModelAction *, ModelAlloc<ModelAction *> > *send_fv)
+bool ModelChecker::w_modification_order(ModelAction *curr, ModelVector<ModelAction *> *send_fv)
{
-
snap_vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
+
SnapVector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
unsigned int i;
bool added = false;
ASSERT(curr->is_write());
*/
bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
{
-
snap_vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, reader->get_location());
+
SnapVector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, reader->get_location());
unsigned int i;
/* Iterate over all threads */
for (i = 0; i < thrd_lists->size(); i++) {
release_heads->push_back(fence_release);
int tid = id_to_int(rf->get_tid());
-
snap_vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, rf->get_location());
+
SnapVector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, rf->get_location());
action_list_t *list = &(*thrd_lists)[tid];
action_list_t::const_reverse_iterator rit;
bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_queue)
{
bool updated = false;
- snap_vector< struct release_seq * >::iterator it = pending_rel_seqs->begin();
+ SnapVector<struct release_seq *>::iterator it = pending_rel_seqs->begin();
while (it != pending_rel_seqs->end()) {
struct release_seq *pending = *it;
ModelAction *acquire = pending->acquire;
if (uninit)
action_trace->push_front(uninit);
-
snap_vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, act->get_location());
+
SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, act->get_location());
if (tid >= (int)vec->size())
vec->resize(priv->next_thread_id);
(*vec)[tid].push_back(act);
void *mutex_loc = (void *) act->get_value();
get_safe_ptr_action(obj_map, mutex_loc)->push_back(act);
-
snap_vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, mutex_loc);
+
SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, mutex_loc);
if (tid >= (int)vec->size())
vec->resize(priv->next_thread_id);
(*vec)[tid].push_back(act);
action_list_t *list = get_safe_ptr_action(obj_map, location);
/* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
action_list_t::reverse_iterator rit;
- for (rit = list->rbegin(); rit != list->rend(); rit++)
- if ((*rit)->is_write() && (*rit)->is_seqcst() && (*rit) != curr)
+ for (rit = list->rbegin(); (*rit) != curr; rit++)
+ ;
+ rit++; /* Skip past curr */
+ for ( ; rit != list->rend(); rit++)
+ if ((*rit)->is_write() && (*rit)->is_seqcst())
return *rit;
return NULL;
}
*/
bool ModelChecker::resolve_promise(ModelAction *write, unsigned int promise_idx)
{
- std::vector< ModelAction *, ModelAlloc<ModelAction *> > actions_to_check;
+ ModelVector<ModelAction *> actions_to_check;
Promise *promise = (*promises)[promise_idx];
for (unsigned int i = 0; i < promise->get_num_readers(); i++) {
*/
void ModelChecker::build_may_read_from(ModelAction *curr)
{
-
snap_vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
+
SnapVector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
unsigned int i;
ASSERT(curr->is_read());
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);
-}
-
/**
* @brief Get a Thread reference by its ID
* @param tid The Thread's ID
{
DBG();
Thread *old = thread_current();
+ scheduler->set_current_thread(NULL);
ASSERT(!old->get_pending());
old->set_pending(act);
if (Thread::swap(old, &system_context) < 0) {
projects / model-checker.git / blobdiff