-/**
- * Structure for holding small ModelChecker members that should be snapshotted
- */
-struct model_snapshot_members {
- ModelAction *current_action;
- int next_thread_id;
- modelclock_t used_sequence_numbers;
- Thread *nextThread;
- ModelAction *next_backtrack;
-
- /** @see ModelChecker::lazy_sync_size */
- unsigned int lazy_sync_size;
+/** @brief Model checker execution stats */
+struct execution_stats {
+ int num_total; /**< @brief Total number of executions */
+ int num_infeasible; /**< @brief Number of infeasible executions */
+ int num_buggy_executions; /** @brief Number of buggy executions */
+ int num_complete; /**< @brief Number of feasible, non-buggy, complete executions */
+ int num_redundant; /**< @brief Number of redundant, aborted executions */
+};
+
+struct PendingFutureValue {
+ PendingFutureValue(ModelAction *writer, ModelAction *act) : writer(writer), act(act) { }
+ const ModelAction *writer;
+ ModelAction *act;
+};
+
+/** @brief Records information regarding a single pending release sequence */
+struct release_seq {
+ /** @brief The acquire operation */
+ ModelAction *acquire;
+ /** @brief The read operation that may read from a release sequence;
+ * may be the same as acquire, or else an earlier action in the same
+ * thread (i.e., when 'acquire' is a fence-acquire) */
+ const ModelAction *read;
+ /** @brief The head of the RMW chain from which 'read' reads; may be
+ * equal to 'release' */
+ const ModelAction *rf;
+ /** @brief The head of the potential longest release sequence chain */
+ const ModelAction *release;
+ /** @brief The write(s) that may break the release sequence */
+ SnapVector<const ModelAction *> writes;