static void param_defaults(struct model_params * params) {
params->maxreads = 0;
params->maxfuturedelay = 100;
+ params->fairwindow = 0;
+ params->enabledcount = 1;
}
static void print_usage(struct model_params *params) {
"-s Maximum actions that the model checker will wait for\n"
" a write from the future past the expected number of\n"
" actions. Default: %d\n"
+"-f Specify a fairness window in which actions that are\n"
+" enabled sufficiently many times should receive\n"
+" priority for execution. Default: %d\n"
+"-e Enabled count. Default: %d\n"
"-- Program arguments follow.\n\n",
- params->maxreads, params->maxfuturedelay);
+params->maxreads, params->maxfuturedelay, params->fairwindow, params->enabledcount);
exit(EXIT_SUCCESS);
}
static void parse_options(struct model_params *params, int *argc, char ***argv) {
- const char *shortopts = "hm:s:";
+ const char *shortopts = "hm:s:f:e:";
int opt;
bool error = false;
while (!error && (opt = getopt(*argc, *argv, shortopts)) != -1) {
case 's':
params->maxfuturedelay = atoi(optarg);
break;
+ case 'f':
+ params->fairwindow = atoi(optarg);
+ break;
+ case 'e':
+ params->enabledcount = atoi(optarg);
+ break;
case 'm':
params->maxreads = atoi(optarg);
break;
/** @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;
struct model_params {
int maxreads;
int maxfuturedelay;
+ unsigned int fairwindow;
+ unsigned int enabledcount;
};
struct PendingFutureValue {
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
* @param nthreads The number of threads which exist at this point in the
* execution trace.
*/
-Node::Node(ModelAction *act, Node *par, int nthreads, bool *enabled)
+Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness)
: action(act),
parent(par),
num_threads(nthreads),
explored_children(num_threads),
backtrack(num_threads),
+ fairness(num_threads),
numBacktracks(0),
+ enabled_array(NULL),
may_read_from(),
read_from_index(0),
future_values(),
future_index(-1)
{
- if (act)
+ if (act) {
act->set_node(this);
- enabled_array=(bool *)MYMALLOC(sizeof(bool)*num_threads);
- if (enabled != NULL)
- memcpy(enabled_array, enabled, sizeof(bool)*num_threads);
- else {
- for(int i=0;i<num_threads;i++)
- enabled_array[i]=false;
+ int currtid=id_to_int(act->get_tid());
+ int prevtid=(prevfairness != NULL)?id_to_int(prevfairness->action->get_tid()):0;
+
+ if ( model->params.fairwindow != 0 ) {
+ for(int i=0;i<nthreads;i++) {
+ ASSERT(i<((int)fairness.size()));
+ struct fairness_info * fi=& fairness[i];
+ struct fairness_info * prevfi=(par!=NULL)&&(i<par->get_num_threads())?&par->fairness[i]:NULL;
+ if (prevfi) {
+ *fi=*prevfi;
+ }
+ if (parent->enabled_array[i]) {
+ fi->enabled_count++;
+ }
+ if (i==currtid) {
+ fi->turns++;
+ fi->priority = false;
+ }
+ //Do window processing
+ if (prevfairness != NULL) {
+ if (prevfairness -> parent->enabled_array[i])
+ fi->enabled_count--;
+ if (i==prevtid) {
+ fi->turns--;
+ }
+ //Need full window to start evaluating conditions
+ //If we meet the enabled count and have no turns, give us priority
+ if ((fi->enabled_count >= model->params.enabledcount) &&
+ (fi->turns == 0))
+ fi->priority = true;
+ }
+ }
+ }
}
}
{
if (action)
delete action;
- MYFREE(enabled_array);
+ if (enabled_array)
+ MYFREE(enabled_array);
}
/** Prints debugging info for the ModelAction associated with this Node */
* Mark the appropriate backtracking information for exploring a thread choice.
* @param act The ModelAction to explore
*/
-void Node::explore_child(ModelAction *act)
+void Node::explore_child(ModelAction *act, bool * is_enabled)
{
+ if ( ! enabled_array )
+ enabled_array=(bool *)MYMALLOC(sizeof(bool)*num_threads);
+ if (is_enabled != NULL)
+ memcpy(enabled_array, is_enabled, sizeof(bool)*num_threads);
+ else {
+ for(int i=0;i<num_threads;i++)
+ enabled_array[i]=false;
+ }
+
explore(act->get_tid());
}
explored_children[i] = true;
}
-static void clear_node_list(node_list_t *list, node_list_t::iterator start,
- node_list_t::iterator end)
-{
- node_list_t::iterator it;
-
- for (it = start; it != end; it++)
- delete (*it);
- list->erase(start, end);
-}
-
NodeStack::NodeStack()
: total_nodes(0)
{
node_list.push_back(new Node());
total_nodes++;
- iter = node_list.begin();
+ iter = 0;
}
NodeStack::~NodeStack()
{
- clear_node_list(&node_list, node_list.begin(), node_list.end());
}
void NodeStack::print()
{
- node_list_t::iterator it;
printf("............................................\n");
printf("NodeStack printing node_list:\n");
- for (it = node_list.begin(); it != node_list.end(); it++) {
+ for (unsigned int it = 0; it < node_list.size(); it++) {
if (it == this->iter)
printf("vvv following action is the current iterator vvv\n");
- (*it)->print();
+ node_list[it]->print();
}
printf("............................................\n");
}
+/** Note: The is_enabled set contains what actions were enabled when
+ * act was chosen. */
+
ModelAction * NodeStack::explore_action(ModelAction *act, bool * is_enabled)
{
DBG();
ASSERT(!node_list.empty());
- node_list_t::iterator it=iter;
- it++;
- if (it != node_list.end()) {
+ if ((iter+1) < node_list.size()) {
iter++;
- return (*iter)->get_action();
+ return node_list[iter]->get_action();
}
/* Record action */
- get_head()->explore_child(act);
- node_list.push_back(new Node(act, get_head(), model->get_num_threads(), is_enabled));
+ get_head()->explore_child(act, is_enabled);
+ Node *prevfairness = NULL;
+ if ( model->params.fairwindow != 0 && iter > model->params.fairwindow ) {
+ prevfairness = node_list[iter-model->params.fairwindow];
+ }
+ node_list.push_back(new Node(act, get_head(), model->get_num_threads(), prevfairness));
total_nodes++;
iter++;
return NULL;
void NodeStack::pop_restofstack(int numAhead)
{
/* Diverging from previous execution; clear out remainder of list */
- node_list_t::iterator it = iter;
- while (numAhead--)
- it++;
- clear_node_list(&node_list, it, node_list.end());
+ unsigned int it=iter+numAhead;
+ node_list.resize(it);
}
Node * NodeStack::get_head()
{
if (node_list.empty())
return NULL;
- return *iter;
+ return node_list[iter];
}
Node * NodeStack::get_next()
{
- node_list_t::iterator it = iter;
if (node_list.empty()) {
DEBUG("Empty\n");
return NULL;
}
- it++;
- if (it == node_list.end()) {
+ unsigned int it=iter+1;
+ if (it == node_list.size()) {
DEBUG("At end\n");
return NULL;
}
- return *it;
+ return node_list[it];
}
void NodeStack::reset_execution()
{
- iter = node_list.begin();
+ iter = 0;
}
modelclock_t expiration;
};
+struct fairness_info {
+ unsigned int enabled_count;
+ unsigned int turns;
+ bool priority;
+};
+
/**
* @brief A single node in a NodeStack
*/
class Node {
public:
- Node(ModelAction *act = NULL, Node *par = NULL, int nthreads = 1, bool *enabled_array = NULL);
+ Node(ModelAction *act = NULL, Node *par = NULL, int nthreads = 1, Node *prevfairness = NULL);
~Node();
/* return true = thread choice has already been explored */
bool has_been_explored(thread_id_t tid);
/* return true = backtrack set is empty */
bool backtrack_empty();
- void explore_child(ModelAction *act);
+ void explore_child(ModelAction *act, bool * is_enabled);
/* return false = thread was already in backtrack */
bool set_backtrack(thread_id_t id);
thread_id_t get_next_backtrack();
bool is_enabled(Thread *t);
bool is_enabled(thread_id_t tid);
ModelAction * get_action() { return action; }
-
+ bool has_priority(thread_id_t tid) {return fairness[id_to_int(tid)].priority;}
+ int get_num_threads() {return num_threads;}
/** @return the parent Node to this Node; that is, the action that
* occurred previously in the stack. */
Node * get_parent() const { return parent; }
int num_threads;
std::vector< bool, MyAlloc<bool> > explored_children;
std::vector< bool, MyAlloc<bool> > backtrack;
+ std::vector< struct fairness_info, MyAlloc< struct fairness_info> > fairness;
int numBacktracks;
bool *enabled_array;
unsigned int future_index;
};
-typedef std::list< Node *, MyAlloc< Node * > > node_list_t;
+typedef std::vector< Node *, MyAlloc< Node * > > node_list_t;
/**
* @brief A stack of nodes
MEMALLOC
private:
node_list_t node_list;
- node_list_t::iterator iter;
+ unsigned int iter;
int total_nodes;
};
}
/**
- * Remove one Thread from the scheduler. This implementation defaults to FIFO,
- * if a thread is not already provided.
+ * Select a Thread. This implementation defaults to round-robin, if a
+ * thread is not already provided.
*
* @param t Thread to run, if chosen by an external entity (e.g.,
* ModelChecker). May be NULL to indicate no external choice.
projects / model-checker.git / commitdiff