/** @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>()),
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;
/** @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. */
+
if (rf->is_acquire() && rf->is_release())
return true; /* complete */
+
+ /** @todo Might it be better to make this into a loop... */
+
return release_seq_head(rf->get_reads_from(), release_heads);
}
if (rf->is_release())