#ifndef __MODEL_H__
#define __MODEL_H__
-#include <vector>
+#include "stl_wrappers.h"
#include <cstddef>
#include <ucontext.h>
#include <inttypes.h>
struct model_snapshot_members;
/** @brief Shorthand for a list of release sequence heads */
-typedef std::vector< const ModelAction *, ModelAlloc<const ModelAction *> > rel_heads_list_t;
+typedef model_vector< const ModelAction * > rel_heads_list_t;
-typedef std::list< ModelAction *, SnapshotAlloc<ModelAction *> > action_list_t;
+typedef snap_list< ModelAction * > action_list_t;
/**
* Model checker parameter structure. Holds run-time configuration options for
struct model_params {
int maxreads;
int maxfuturedelay;
+ bool yieldon;
unsigned int fairwindow;
unsigned int enabledcount;
unsigned int bound;
+ unsigned int uninitvalue;
/** @brief Maximum number of future values that can be sent to the same
* read */
Thread * take_step(ModelAction *curr);
- bool check_recency(ModelAction *curr, const ModelAction *rf) const;
-
template <typename T>
- bool should_read_instead(const ModelAction *curr, const ModelAction *rf, const T *other_rf) const;
+ bool check_recency(ModelAction *curr, const T *rf) const;
+
+ template <typename T, typename U>
+ bool should_read_instead(const ModelAction *curr, const T *rf, const U *other_rf) const;
ModelAction * get_last_fence_conflict(ModelAction *act) const;
ModelAction * get_last_conflict(ModelAction *act) const;
void set_backtracking(ModelAction *act);
- Thread * get_next_thread(ModelAction *curr);
+ Thread * action_select_next_thread(const ModelAction *curr) const;
+ Thread * get_next_thread();
bool set_latest_backtrack(ModelAction *act);
ModelAction * get_next_backtrack();
void reset_to_initial_state();
bool resolve_release_sequences(void *location, work_queue_t *work_queue);
void add_future_value(const ModelAction *writer, ModelAction *reader);
- ModelAction * new_uninitialized_action(void *location) const;
+ ModelAction * get_uninitialized_action(const ModelAction *curr) const;
ModelAction *diverge;
ModelAction *earliest_diverge;
* to a trace of all actions performed on the object. */
HashTable<const void *, action_list_t *, uintptr_t, 4> * const condvar_waiters_map;
- HashTable<void *, std::vector<action_list_t> *, uintptr_t, 4 > * const obj_thrd_map;
- std::vector< Promise *, SnapshotAlloc<Promise *> > * const promises;
- std::vector< struct PendingFutureValue, SnapshotAlloc<struct PendingFutureValue> > * const futurevalues;
+ HashTable<void *, snap_vector<action_list_t> *, uintptr_t, 4 > * const obj_thrd_map;
+ snap_vector< Promise * > * const promises;
+ snap_vector< struct PendingFutureValue > * const futurevalues;
/**
* List of pending release sequences. Release sequences might be
* are established. Each entry in the list may only be partially
* filled, depending on its pending status.
*/
- std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> > * const pending_rel_seqs;
+ snap_vector< struct release_seq * > * const pending_rel_seqs;
- std::vector< ModelAction *, SnapshotAlloc<ModelAction *> > * const thrd_last_action;
- std::vector< ModelAction *, SnapshotAlloc<ModelAction *> > * const thrd_last_fence_release;
+ snap_vector< ModelAction * > * const thrd_last_action;
+ snap_vector< ModelAction * > * const thrd_last_fence_release;
NodeStack * const node_stack;
/** Private data members that should be snapshotted. They are grouped
bool is_feasible_prefix_ignore_relseq() const;
bool is_infeasible() const;
bool is_deadlocked() const;
+ bool is_circular_wait(const Thread *t) const;
bool is_complete_execution() const;
bool have_bug_reports() const;
void print_bugs() const;