sleep_flag(false)
{
/* References to NULL atomic variables can end up here */
- ASSERT(loc || type == ATOMIC_FENCE || type == MODEL_FIXUP_RELSEQ);
+ ASSERT(loc || type == ATOMIC_FENCE);
Thread *t = thread ? thread : thread_current();
this->tid = t->get_id();
return type == THREAD_JOIN || type == PTHREAD_JOIN;
}
-bool ModelAction::is_relseq_fixup() const
-{
- return type == MODEL_FIXUP_RELSEQ;
-}
-
bool ModelAction::is_mutex_op() const
{
return type == ATOMIC_LOCK || type == ATOMIC_TRYLOCK || type == ATOMIC_UNLOCK || type == ATOMIC_WAIT || type == ATOMIC_NOTIFY_ONE || type == ATOMIC_NOTIFY_ALL;
const char * ModelAction::get_type_str() const
{
switch (this->type) {
- case MODEL_FIXUP_RELSEQ: return "relseq fixup";
case THREAD_CREATE: return "thread create";
case THREAD_START: return "thread start";
case THREAD_YIELD: return "thread yield";
/** @brief Represents an action type, identifying one of several types of
* ModelAction */
typedef enum action_type {
- MODEL_FIXUP_RELSEQ, /**< Special ModelAction: finalize a release
- * sequence */
THREAD_CREATE, /**< A thread creation action */
THREAD_START, /**< First action in each thread */
THREAD_YIELD, /**< A thread yield action */
void set_try_lock(bool obtainedlock);
bool is_thread_start() const;
bool is_thread_join() const;
- bool is_relseq_fixup() const;
bool is_mutex_op() const;
bool is_lock() const;
bool is_trylock() const;
*/
bool ModelExecution::process_write(ModelAction *curr, work_queue_t *work)
{
- /* Readers to which we may send our future value */
- ModelVector<ModelAction *> send_fv;
-
bool updated_mod_order = w_modification_order(curr);
return updated;
}
-/**
- * @brief Process the current action for release sequence fixup activity
- *
- * Performs model-checker release sequence fixups for the current action,
- * forcing a single pending release sequence to break (with a given, potential
- * "loose" write) or to complete (i.e., synchronize). If a pending release
- * sequence forms a complete release sequence, then we must perform the fixup
- * synchronization, mo_graph additions, etc.
- *
- * @param curr The current action; must be a release sequence fixup action
- * @param work_queue The work queue to which to add work items as they are
- * generated
- */
-void ModelExecution::process_relseq_fixup(ModelAction *curr, work_queue_t *work_queue)
-{
- const ModelAction *write = curr->get_node()->get_relseq_break();
- struct release_seq *sequence = pending_rel_seqs.back();
- pending_rel_seqs.pop_back();
- ASSERT(sequence);
- ModelAction *acquire = sequence->acquire;
- const ModelAction *rf = sequence->rf;
- const ModelAction *release = sequence->release;
- ASSERT(acquire);
- ASSERT(release);
- ASSERT(rf);
- ASSERT(release->same_thread(rf));
-
- if (write == NULL) {
- /**
- * @todo Forcing a synchronization requires that we set
- * modification order constraints. For instance, we can't allow
- * a fixup sequence in which two separate read-acquire
- * operations read from the same sequence, where the first one
- * synchronizes and the other doesn't. Essentially, we can't
- * allow any writes to insert themselves between 'release' and
- * 'rf'
- */
-
- /* Must synchronize */
- if (!synchronize(release, acquire))
- return;
-
- /* Propagate the changed clock vector */
- propagate_clockvector(acquire, work_queue);
- } else {
- /* Break release sequence with new edges:
- * release --mo--> write --mo--> rf */
- mo_graph->addEdge(release, write);
- mo_graph->addEdge(write, rf);
- }
-
- /* See if we have realized a data race */
- checkDataRaces();
-}
-
/**
* Initialize the current action by performing one or more of the following
* actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
* Perform one-time actions when pushing new ModelAction onto
* NodeStack
*/
- if (newcurr->is_relseq_fixup())
- compute_relseq_breakwrites(newcurr);
- else if (newcurr->is_wait())
+ if (newcurr->is_wait())
newcurr->get_node()->set_misc_max(2);
else if (newcurr->is_notify_one()) {
newcurr->get_node()->set_misc_max(get_safe_ptr_action(&condvar_waiters_map, newcurr->get_location())->size());
switch (work.type) {
case WORK_CHECK_CURR_ACTION: {
ModelAction *act = work.action;
- bool update = false; /* update this location's release seq's */
- bool update_all = false; /* update all release seq's */
- if (process_thread_action(curr))
- update_all = true;
+ process_thread_action(curr);
- if (act->is_read() && !second_part_of_rmw && process_read(act))
- update = true;
+ if (act->is_read() && !second_part_of_rmw)
+ process_read(act);
- if (act->is_write() && process_write(act, &work_queue))
- update = true;
+ if (act->is_write())
+ process_write(act, &work_queue);
+
+ if (act->is_fence())
+ process_fence(act);
+
+ if (act->is_mutex_op())
+ process_mutex(act);
- if (act->is_fence() && process_fence(act))
- update_all = true;
-
- if (act->is_mutex_op() && process_mutex(act))
- update_all = true;
-
- if (act->is_relseq_fixup())
- process_relseq_fixup(curr, &work_queue);
-
- if (update_all)
- work_queue.push_back(CheckRelSeqWorkEntry(NULL));
- else if (update)
- work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
break;
}
- case WORK_CHECK_RELEASE_SEQ:
- resolve_release_sequences(work.location, &work_queue);
- break;
case WORK_CHECK_MO_EDGES: {
/** @todo Complete verification of work_queue */
ModelAction *act = work.action;
- bool updated = false;
if (act->is_read()) {
const ModelAction *rf = act->get_reads_from();
- if (r_modification_order(act, rf))
- updated = true;
+ r_modification_order(act, rf);
if (act->is_seqcst()) {
ModelAction *last_sc_write = get_last_seq_cst_write(act);
if (last_sc_write != NULL && rf->happens_before(last_sc_write)) {
}
}
if (act->is_write()) {
- if (w_modification_order(act))
- updated = true;
+ w_modification_order(act);
}
mo_graph->commitChanges();
-
- if (updated)
- work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
break;
}
default:
if ((parnode && !parnode->backtrack_empty()) ||
!currnode->misc_empty() ||
- !currnode->read_from_empty() ||
- !currnode->relseq_break_empty()) {
+ !currnode->read_from_empty()) {
set_latest_backtrack(curr);
}
}
*/
bool ModelExecution::isfeasibleprefix() const
{
- return pending_rel_seqs.size() == 0 && is_feasible_prefix_ignore_relseq();
+ return !is_infeasible();
}
/**
model_print("%s: %s", prefix ? prefix : "Infeasible", buf);
}
-/**
- * Returns whether the current completed trace is feasible, except for pending
- * release sequences.
- */
-bool ModelExecution::is_feasible_prefix_ignore_relseq() const
-{
- return !is_infeasible() ;
-
-}
-
/**
* Check if the current partial trace is infeasible. Does not check any
* end-of-execution flags, which might rule out the execution. Thus, this is
*/
void ModelExecution::propagate_clockvector(ModelAction *acquire, work_queue_t *work)
{
- /* Re-check all pending release sequences */
- work->push_back(CheckRelSeqWorkEntry(NULL));
/* Re-check read-acquire for mo_graph edges */
work->push_back(MOEdgeWorkEntry(acquire));
return get_parent_action(tid)->get_cv();
}
-/**
- * Compute the set of writes that may break the current pending release
- * sequence. This information is extracted from previou release sequence
- * calculations.
- *
- * @param curr The current ModelAction. Must be a release sequence fixup
- * action.
- */
-void ModelExecution::compute_relseq_breakwrites(ModelAction *curr)
-{
- if (pending_rel_seqs.empty())
- return;
-
- struct release_seq *pending = pending_rel_seqs.back();
- for (unsigned int i = 0; i < pending->writes.size(); i++) {
- const ModelAction *write = pending->writes[i];
- curr->get_node()->add_relseq_break(write);
- }
-
- /* NULL means don't break the sequence; just synchronize */
- curr->get_node()->add_relseq_break(NULL);
-}
-
/**
* Build up an initial set of all past writes that this 'read' action may read
* from, as well as any previously-observed future values that must still be valid.
return action_select_next_thread(curr);
}
-/**
- * Launch end-of-execution release sequence fixups only when
- * the execution is otherwise feasible AND there are:
- *
- * (1) pending release sequences
- * (2) pending assertions that could be invalidated by a change
- * in clock vectors (i.e., data races)
- * (3) no pending promises
- */
-void ModelExecution::fixup_release_sequences()
-{
- while (!pending_rel_seqs.empty() &&
- is_feasible_prefix_ignore_relseq() &&
- haveUnrealizedRaces()) {
- model_print("*** WARNING: release sequence fixup action "
- "(%zu pending release seuqence(s)) ***\n",
- pending_rel_seqs.size());
- ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,
- std::memory_order_seq_cst, NULL, VALUE_NONE,
- model_thread);
- take_step(fixup);
- };
-}
const struct model_params * get_params() const { return params; }
Thread * take_step(ModelAction *curr);
- void fixup_release_sequences();
void print_summary() const;
#if SUPPORT_MOD_ORDER_DUMP
bool is_complete_execution() const;
void print_infeasibility(const char *prefix) const;
- bool is_feasible_prefix_ignore_relseq() const;
bool is_infeasible() const;
bool is_deadlocked() const;
bool is_yieldblocked() const;
bool process_mutex(ModelAction *curr);
bool process_thread_action(ModelAction *curr);
- void process_relseq_fixup(ModelAction *curr, work_queue_t *work_queue);
bool read_from(ModelAction *act, const ModelAction *rf);
bool synchronize(const ModelAction *first, ModelAction *second);
ModelAction * get_last_conflict(ModelAction *act) const;
void set_backtracking(ModelAction *act);
bool set_latest_backtrack(ModelAction *act);
- void compute_relseq_breakwrites(ModelAction *curr);
void check_curr_backtracking(ModelAction *curr);
void add_action_to_lists(ModelAction *act);
bool release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads, struct release_seq *pending) const;
void propagate_clockvector(ModelAction *acquire, work_queue_t *work);
bool resolve_release_sequences(void *location, work_queue_t *work_queue);
- void add_future_value(const ModelAction *writer, ModelAction *reader);
ModelAction * get_uninitialized_action(const ModelAction *curr) const;
action_list_t action_trace;
static void param_defaults(struct model_params *params)
{
params->maxreads = 0;
- params->maxfuturedelay = 6;
params->fairwindow = 0;
params->yieldon = false;
params->yieldblock = false;
params->enabledcount = 1;
params->bound = 0;
- params->maxfuturevalues = 0;
- params->expireslop = 4;
params->verbose = !!DBG_ENABLED();
params->uninitvalue = 0;
params->maxexecutions = 0;
"-m, --liveness=NUM Maximum times a thread can read from the same write\n"
" while other writes exist.\n"
" Default: %d\n"
-"-M, --maxfv=NUM Maximum number of future values that can be sent to\n"
-" the same read.\n"
-" Default: %d\n"
-"-s, --maxfvdelay=NUM Maximum actions that the model checker will wait for\n"
-" a write from the future past the expected number\n"
-" of actions.\n"
-" Default: %d\n"
-"-S, --fvslop=NUM Future value expiration sloppiness.\n"
-" Default: %u\n"
"-y, --yield Enable CHESS-like yield-based fairness support\n"
" (requires thrd_yield() in test program).\n"
" Default: %s\n"
" -- Program arguments follow.\n\n",
program_name,
params->maxreads,
- params->maxfuturevalues,
- params->maxfuturedelay,
- params->expireslop,
params->yieldon ? "enabled" : "disabled",
params->yieldblock ? "enabled" : "disabled",
params->fairwindow,
params->enabledcount,
params->bound,
params->verbose,
- params->uninitvalue,
+ params->uninitvalue,
params->maxexecutions);
exit(EXIT_SUCCESS);
static void parse_options(struct model_params *params, int argc, char **argv)
{
- const char *shortopts = "hyYt:o:m:M:s:S:f:e:b:u:x:v::";
+ const char *shortopts = "hyYt:o:m:f:e:b:u:x:v::";
const struct option longopts[] = {
{"help", no_argument, NULL, 'h'},
{"liveness", required_argument, NULL, 'm'},
- {"maxfv", required_argument, NULL, 'M'},
- {"maxfvdelay", required_argument, NULL, 's'},
- {"fvslop", required_argument, NULL, 'S'},
{"fairness", required_argument, NULL, 'f'},
{"yield", no_argument, NULL, 'y'},
{"yieldblock", no_argument, NULL, 'Y'},
case 'x':
params->maxexecutions = atoi(optarg);
break;
- case 's':
- params->maxfuturedelay = atoi(optarg);
- break;
- case 'S':
- params->expireslop = atoi(optarg);
- break;
case 'f':
params->fairwindow = atoi(optarg);
break;
case 'm':
params->maxreads = atoi(optarg);
break;
- case 'M':
- params->maxfuturevalues = atoi(optarg);
- break;
case 'v':
params->verbose = optarg ? atoi(optarg) : 1;
break;
i++;
} while (i<2); // while (has_next);
- execution->fixup_release_sequences();
model_print("******* Model-checking complete: *******\n");
print_stats();
enabled_array(NULL),
read_from_past(),
read_from_past_idx(0),
- relseq_break_writes(),
- relseq_break_index(0),
misc_index(0),
misc_max(0),
yield_data(NULL)
model_print("\n");
model_print(" misc: %s\n", misc_empty() ? "empty" : "non-empty");
- model_print(" rel seq break: %s\n", relseq_break_empty() ? "empty" : "non-empty");
}
/****************************** threads backtracking **************************/
/************************** end read from past ********************************/
-/*********************** breaking release sequences ***************************/
-
-/**
- * Add a write ModelAction to the set of writes that may break the release
- * sequence. This is used during replay exploration of pending release
- * sequences. This Node must correspond to a release sequence fixup action.
- *
- * @param write The write that may break the release sequence. NULL means we
- * allow the release sequence to synchronize.
- */
-void Node::add_relseq_break(const ModelAction *write)
-{
- relseq_break_writes.push_back(write);
-}
-
-/**
- * Get the write that may break the current pending release sequence,
- * according to the replay / divergence pattern.
- *
- * @return A write that may break the release sequence. If NULL, that means
- * the release sequence should not be broken.
- */
-const ModelAction * Node::get_relseq_break() const
-{
- if (relseq_break_index < (int)relseq_break_writes.size())
- return relseq_break_writes[relseq_break_index];
- else
- return NULL;
-}
-
-/**
- * Increments the index into the relseq_break_writes set to explore the next
- * item.
- * @return Returns false if we have explored all values.
- */
-bool Node::increment_relseq_break()
-{
- DBG();
- if (relseq_break_index < ((int)relseq_break_writes.size())) {
- relseq_break_index++;
- return (relseq_break_index < ((int)relseq_break_writes.size()));
- }
- return false;
-}
-
-/**
- * @return True if all writes that may break the release sequence have been
- * explored
- */
-bool Node::relseq_break_empty() const
-{
- return ((relseq_break_index + 1) >= ((int)relseq_break_writes.size()));
-}
-
-/******************* end breaking release sequences ***************************/
/**
* Increments some behavior's index, if a new behavior is available
/* read from a different value */
if (increment_read_from())
return true;
- /* resolve a release sequence differently */
- if (increment_relseq_break())
- return true;
return false;
}
bool increment_misc();
bool misc_empty() const;
- void add_relseq_break(const ModelAction *write);
- const ModelAction * get_relseq_break() const;
- bool increment_relseq_break();
- bool relseq_break_empty() const;
-
bool increment_behaviors();
void print() const;
int get_yield_data(int tid1, int tid2) const;
bool read_from_past_empty() const;
bool increment_read_from_past();
- bool future_value_empty() const;
- bool increment_future_value();
read_from_type_t read_from_status;
const struct model_params * get_params() const { return params; }
ModelVector<const ModelAction *> read_from_past;
unsigned int read_from_past_idx;
- ModelVector<const ModelAction *> relseq_break_writes;
- int relseq_break_index;
-
int misc_index;
int misc_max;
int * yield_data;
*/
struct model_params {
int maxreads;
- int maxfuturedelay;
bool yieldon;
bool yieldblock;
unsigned int fairwindow;
unsigned int uninitvalue;
int maxexecutions;
- /** @brief Maximum number of future values that can be sent to the same
- * read */
- int maxfuturevalues;
-
- /** @brief Only generate a new future value/expiration pair if the
- * expiration time exceeds the existing one by more than the slop
- * value */
- unsigned int expireslop;
-
/** @brief Verbosity (0 = quiet; 1 = noisy; 2 = noisier) */
int verbose;
static void param_defaults(struct model_params *params)
{
params->maxreads = 0;
- params->maxfuturedelay = 6;
params->fairwindow = 0;
params->yieldon = false;
params->yieldblock = false;
params->enabledcount = 1;
params->bound = 0;
- params->maxfuturevalues = 0;
- params->expireslop = 4;
params->verbose = !!DBG_ENABLED();
params->uninitvalue = 0;
params->maxexecutions = 0;
/** @brief Type of work queue entry */
model_work_t type;
- /**
- * @brief Object affected
- * @see CheckRelSeqWorkEntry
- */
- void *location;
-
/**
* @brief The ModelAction to work on
* @see MOEdgeWorkEntry
*/
CheckCurrWorkEntry(ModelAction *curr) {
type = WORK_CHECK_CURR_ACTION;
- location = NULL;
action = curr;
}
};
-/**
- * @brief Work: check an object location for resolved release sequences
- *
- * This WorkQueueEntry checks synchronization and the mo_graph for resolution
- * of any release sequences. The object @a location is the only relevant
- * parameter to this entry.
- */
-class CheckRelSeqWorkEntry : public WorkQueueEntry {
- public:
- /**
- * @brief Constructor for a "check release sequences" work entry
- * @param l The location which must be checked for release sequences
- */
- CheckRelSeqWorkEntry(void *l) {
- type = WORK_CHECK_RELEASE_SEQ;
- location = l;
- action = NULL;
- }
-};
-
/**
* @brief Work: check a ModelAction for new mo_graph edges
*
*/
MOEdgeWorkEntry(ModelAction *updated) {
type = WORK_CHECK_MO_EDGES;
- location = NULL;
action = updated;
}
};
projects / c11tester.git / commitdiff