remove old release sequences
authorbdemsky <bdemsky@uci.edu>
Tue, 4 Jun 2019 04:53:31 +0000 (21:53 -0700)
committerbdemsky <bdemsky@uci.edu>
Tue, 4 Jun 2019 05:09:38 +0000 (22:09 -0700)
action.cc
action.h
execution.cc
execution.h
main.cc
model.cc
nodestack.cc
nodestack.h
params.h
pthread.cc
workqueue.h

index 8395c88..bd95850 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -46,7 +46,7 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc,
        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();
@@ -90,11 +90,6 @@ bool ModelAction::is_thread_join() const
        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;
@@ -535,7 +530,6 @@ bool ModelAction::happens_before(const ModelAction *act) const
 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";
index 06d76c2..ef93928 100644 (file)
--- a/action.h
+++ b/action.h
@@ -50,8 +50,6 @@ using std::memory_order_seq_cst;
 /** @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 */
@@ -128,7 +126,6 @@ public:
        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;
index 7a51bca..369498b 100644 (file)
@@ -745,9 +745,6 @@ bool ModelExecution::process_mutex(ModelAction *curr)
  */
 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);
 
@@ -885,61 +882,6 @@ bool ModelExecution::process_thread_action(ModelAction *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
@@ -995,9 +937,7 @@ bool ModelExecution::initialize_curr_action(ModelAction **curr)
                 * 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());
@@ -1129,45 +1069,30 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr)
                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)) {
@@ -1176,13 +1101,9 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr)
                                }
                        }
                        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:
@@ -1203,8 +1124,7 @@ void ModelExecution::check_curr_backtracking(ModelAction *curr)
 
        if ((parnode && !parnode->backtrack_empty()) ||
                         !currnode->misc_empty() ||
-                        !currnode->read_from_empty() ||
-                        !currnode->relseq_break_empty()) {
+           !currnode->read_from_empty()) {
                set_latest_backtrack(curr);
        }
 }
@@ -1216,7 +1136,7 @@ void ModelExecution::check_curr_backtracking(ModelAction *curr)
  */
 bool ModelExecution::isfeasibleprefix() const
 {
-       return pending_rel_seqs.size() == 0 && is_feasible_prefix_ignore_relseq();
+  return !is_infeasible();
 }
 
 /**
@@ -1242,16 +1162,6 @@ void ModelExecution::print_infeasibility(const char *prefix) const
                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
@@ -1852,8 +1762,6 @@ void ModelExecution::get_release_seq_heads(ModelAction *acquire,
  */
 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));
 
@@ -2101,29 +2009,6 @@ ClockVector * ModelExecution::get_cv(thread_id_t tid) const
        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.
@@ -2445,26 +2330,3 @@ Thread * ModelExecution::take_step(ModelAction *curr)
        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);
-       };
-}
index 579e9b7..bc7fb98 100644 (file)
@@ -71,7 +71,6 @@ public:
        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
@@ -110,7 +109,6 @@ public:
        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;
@@ -154,7 +152,6 @@ private:
        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);
 
@@ -168,7 +165,6 @@ private:
        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);
@@ -187,7 +183,6 @@ private:
        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;
diff --git a/main.cc b/main.cc
index 0d4a6ad..4d308a8 100644 (file)
--- a/main.cc
+++ b/main.cc
 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;
@@ -52,15 +49,6 @@ static void print_usage(const char *program_name, struct model_params *params)
 "-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"
@@ -89,16 +77,13 @@ static void print_usage(const char *program_name, struct model_params *params)
 " --                         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);
@@ -106,13 +91,10 @@ static void print_usage(const char *program_name, struct model_params *params)
 
 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'},
@@ -135,12 +117,6 @@ static void parse_options(struct model_params *params, int argc, char **argv)
                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;
@@ -153,9 +129,6 @@ static void parse_options(struct model_params *params, int argc, char **argv)
                case 'm':
                        params->maxreads = atoi(optarg);
                        break;
-               case 'M':
-                       params->maxfuturevalues = atoi(optarg);
-                       break;
                case 'v':
                        params->verbose = optarg ? atoi(optarg) : 1;
                        break;
index 6f6ba3e..6f28968 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -544,7 +544,6 @@ void ModelChecker::run()
                i++;
        } while (i<2); // while (has_next);
 
-       execution->fixup_release_sequences();
 
        model_print("******* Model-checking complete: *******\n");
        print_stats();
index e3bccc9..f676138 100644 (file)
@@ -42,8 +42,6 @@ Node::Node(const struct model_params *params, ModelAction *act, Node *par,
        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)
@@ -175,7 +173,6 @@ void Node::print() const
        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 **************************/
@@ -442,61 +439,6 @@ bool Node::increment_read_from_past()
 
 /************************** 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
@@ -510,9 +452,6 @@ bool Node::increment_behaviors()
        /* read from a different value */
        if (increment_read_from())
                return true;
-       /* resolve a release sequence differently */
-       if (increment_relseq_break())
-               return true;
        return false;
 }
 
index b7e630b..702c993 100644 (file)
@@ -98,11 +98,6 @@ public:
        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;
@@ -113,8 +108,6 @@ private:
        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; }
 
@@ -140,9 +133,6 @@ private:
        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;
index d5fd1cb..0b1c5bf 100644 (file)
--- a/params.h
+++ b/params.h
@@ -7,7 +7,6 @@
  */
 struct model_params {
        int maxreads;
-       int maxfuturedelay;
        bool yieldon;
        bool yieldblock;
        unsigned int fairwindow;
@@ -16,15 +15,6 @@ struct model_params {
        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;
 
index 723e60b..e5bc901 100644 (file)
 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;
index 9034788..be0188b 100644 (file)
@@ -27,12 +27,6 @@ class WorkQueueEntry {
        /** @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
@@ -55,31 +49,10 @@ class CheckCurrWorkEntry : public WorkQueueEntry {
         */
        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
  *
@@ -96,7 +69,6 @@ class MOEdgeWorkEntry : public WorkQueueEntry {
         */
        MOEdgeWorkEntry(ModelAction *updated) {
                type = WORK_CHECK_MO_EDGES;
-               location = NULL;
                action = updated;
        }
 };