#include <cstddef>
#include <ucontext.h>
-#include "schedule.h"
#include "mymemory.h"
-#include "libthreads.h"
-#include "threads.h"
#include "action.h"
-#include "clockvector.h"
#include "hashtable.h"
#include "workqueue.h"
#include "config.h"
+#include "modeltypes.h"
/* Forward declaration */
class NodeStack;
class CycleGraph;
class Promise;
+class Scheduler;
+class Thread;
/** @brief Shorthand for a list of release sequence heads */
-typedef std::vector< const ModelAction *, MyAlloc<const ModelAction *> > rel_heads_list_t;
+typedef std::vector< const ModelAction *, ModelAlloc<const ModelAction *> > rel_heads_list_t;
/**
* Model checker parameter structure. Holds run-time configuration options for
*/
struct model_snapshot_members {
ModelAction *current_action;
- int next_thread_id;
+ unsigned int next_thread_id;
modelclock_t used_sequence_numbers;
Thread *nextThread;
ModelAction *next_backtrack;
};
+/** @brief Records information regarding a single pending release sequence */
+struct release_seq {
+ /** @brief The acquire operation */
+ ModelAction *acquire;
+ /** @brief The head of the RMW chain from which 'acquire' 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 */
+ std::vector<const ModelAction *> writes;
+};
+
/** @brief The central structure for model-checking */
class ModelChecker {
public:
void add_thread(Thread *t);
void remove_thread(Thread *t);
- Thread * get_thread(thread_id_t tid) { return thread_map->get(id_to_int(tid)); }
- Thread * get_thread(ModelAction *act) { return get_thread(act->get_tid()); }
+ Thread * get_thread(thread_id_t tid) const;
+ Thread * get_thread(ModelAction *act) const;
thread_id_t get_next_id();
- int get_num_threads();
- modelclock_t get_next_seq_num();
-
- /** @return The currently executing Thread. */
- Thread * get_current_thread() { return scheduler->get_current_thread(); }
+ unsigned int get_num_threads();
+ Thread * get_current_thread();
int switch_to_master(ModelAction *act);
ClockVector * get_cv(thread_id_t tid);
bool isfeasible();
bool isfeasibleotherthanRMW();
bool isfinalfeasible();
- void check_promises(ClockVector *old_cv, ClockVector * merge_cv);
+ void mo_check_promises(thread_id_t tid, const ModelAction *write);
+ void check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector * merge_cv);
void get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads);
void finish_execution();
bool isfeasibleprefix();
void set_bad_synchronization() { bad_synchronization = true; }
const model_params params;
+ Scheduler * get_scheduler() { return scheduler;}
MEMALLOC
private:
int num_feasible_executions;
bool promises_expired();
+ modelclock_t get_next_seq_num();
+
/**
* Stores the ModelAction for the current thread action. Call this
* immediately before switching from user- to system-context to pass
void post_r_modification_order(ModelAction *curr, const ModelAction *rf);
bool r_modification_order(ModelAction *curr, const ModelAction *rf);
bool w_modification_order(ModelAction *curr);
- bool release_seq_head(const ModelAction *rf, rel_heads_list_t *release_heads) const;
+ bool release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const;
bool resolve_release_sequences(void *location, work_queue_t *work_queue);
void do_complete_join(ModelAction *join);