/** @brief Constructor */
ModelChecker::ModelChecker(struct model_params params) :
/* Initialize default scheduler */
+ params(params),
scheduler(new Scheduler()),
num_executions(0),
num_feasible_executions(0),
- params(params),
diverge(NULL),
action_trace(new action_list_t()),
thread_map(new HashTable<int, Thread *, int>()),
obj_thrd_map(new HashTable<void *, std::vector<action_list_t>, uintptr_t, 4 >()),
promises(new std::vector<Promise *>()),
futurevalues(new std::vector<struct PendingFutureValue>()),
- lazy_sync_with_release(new HashTable<void *, action_list_t, uintptr_t, 4>()),
+ pending_acq_rel_seq(new std::vector<ModelAction *>()),
thrd_last_action(new std::vector<ModelAction *>(1)),
node_stack(new NodeStack()),
mo_graph(new CycleGraph()),
priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv));
/* First thread created will have id INITIAL_THREAD_ID */
priv->next_thread_id = INITIAL_THREAD_ID;
-
- lazy_sync_size = &priv->lazy_sync_size;
}
/** @brief Destructor */
delete (*promises)[i];
delete promises;
- delete lazy_sync_with_release;
+ delete pending_acq_rel_seq;
delete thrd_last_action;
delete node_stack;
if (node->has_been_explored(tid))
continue;
+ /* See if fairness allows */
+ if (model->params.fairwindow != 0 && !node->has_priority(tid)) {
+ bool unfair=false;
+ for(int t=0;t<node->get_num_threads();t++) {
+ thread_id_t tother=int_to_id(t);
+ if (node->is_enabled(tother) && node->has_priority(tother)) {
+ unfair=true;
+ break;
+ }
+ }
+ if (unfair)
+ continue;
+ }
+
/* Cache the latest backtracking point */
if (!priv->next_backtrack || *prev > *priv->next_backtrack)
priv->next_backtrack = prev;
/** @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;
+ return promises->size() == 0 && pending_acq_rel_seq->size() == 0;
}
/** @return whether the current partial trace is feasible. */
*/
bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *release_heads) const
{
- if (!rf) {
- /* read from future: need to settle this later */
- return false; /* incomplete */
- }
+ while (rf) {
+ ASSERT(rf->is_write());
- ASSERT(rf->is_write());
+ if (rf->is_release())
+ release_heads->push_back(rf);
+ if (!rf->is_rmw())
+ break; /* End of RMW chain */
- if (rf->is_release())
- release_heads->push_back(rf);
- if (rf->is_rmw()) {
- /* We need a RMW action that is both an acquire and release to stop */
/** @todo Need to be smarter here... In the linux lock
* example, this will run to the beginning of the program for
* every acquire. */
+ /** @todo The way to be smarter here is to keep going until 1
+ * thread has a release preceded by an acquire and you've seen
+ * both. */
+
+ /* acq_rel RMW is a sufficient stopping condition */
if (rf->is_acquire() && rf->is_release())
return true; /* complete */
- return release_seq_head(rf->get_reads_from(), release_heads);
+
+ rf = rf->get_reads_from();
+ };
+ if (!rf) {
+ /* read from future: need to settle this later */
+ return false; /* incomplete */
}
+
if (rf->is_release())
return true; /* complete */
complete = release_seq_head(rf, release_heads);
if (!complete) {
/* add act to 'lazy checking' list */
- action_list_t *list;
- list = lazy_sync_with_release->get_safe_ptr(act->get_location());
- list->push_back(act);
- (*lazy_sync_size)++;
+ pending_acq_rel_seq->push_back(act);
}
}
* modification order information is present at the time an action occurs.
*
* @param location The location/object that should be checked for release
- * sequence resolutions
+ * sequence resolutions. A NULL value means to check all locations.
* @param work_queue The work queue to which to add work items as they are
* generated
* @return True if any updates occurred (new synchronization, new mo_graph
*/
bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_queue)
{
- action_list_t *list;
- list = lazy_sync_with_release->getptr(location);
- if (!list)
- return false;
-
bool updated = false;
- action_list_t::iterator it = list->begin();
- while (it != list->end()) {
+ std::vector<ModelAction *>::iterator it = pending_acq_rel_seq->begin();
+ while (it != pending_acq_rel_seq->end()) {
ModelAction *act = *it;
+
+ /* Only resolve sequences on the given location, if provided */
+ if (location && act->get_location() != location) {
+ it++;
+ continue;
+ }
+
const ModelAction *rf = act->get_reads_from();
rel_heads_list_t release_heads;
bool complete;
}
}
}
- if (complete) {
- it = list->erase(it);
- (*lazy_sync_size)--;
- } else
+ if (complete)
+ it = pending_acq_rel_seq->erase(it);
+ else
it++;
}
struct model_params {
int maxreads;
int maxfuturedelay;
+ unsigned int fairwindow;
+ unsigned int enabledcount;
};
struct PendingFutureValue {
modelclock_t used_sequence_numbers;
Thread *nextThread;
ModelAction *next_backtrack;
-
- /** @see ModelChecker::lazy_sync_size */
- unsigned int lazy_sync_size;
};
/** @brief The central structure for model-checking */
void finish_execution();
bool isfeasibleprefix();
void set_assert() {asserted=true;}
+ const model_params params;
MEMALLOC
private:
int num_executions;
int num_feasible_executions;
bool promises_expired();
- const model_params params;
/**
* Stores the ModelAction for the current thread action. Call this
std::vector<struct PendingFutureValue> *futurevalues;
/**
- * Collection of lists of objects that might synchronize with one or
- * more release sequence. Release sequences might be determined lazily
- * as promises are fulfilled and modification orders are established.
- * This structure maps its lists by object location. Each ModelAction
- * in the lists should be an acquire operation.
- */
- HashTable<void *, action_list_t, uintptr_t, 4> *lazy_sync_with_release;
-
- /**
- * Represents the total size of the
- * ModelChecker::lazy_sync_with_release lists. This count should be
- * snapshotted, so it is actually a pointer to a location within
- * ModelChecker::priv
+ * List of acquire actions that might synchronize with one or more
+ * release sequence. Release sequences might be determined lazily as
+ * promises are fulfilled and modification orders are established. Each
+ * ModelAction in this list must be an acquire operation.
*/
- unsigned int *lazy_sync_size;
+ std::vector<ModelAction *> *pending_acq_rel_seq;
std::vector<ModelAction *> *thrd_last_action;
NodeStack *node_stack;
projects / model-checker.git / commitdiff