#define __MODEL_H__
#include <cstddef>
-#include <ucontext.h>
#include <inttypes.h>
#include "mymemory.h"
#include "config.h"
#include "modeltypes.h"
#include "stl-model.h"
+#include "context.h"
/* Forward declaration */
class Node;
void check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector *merge_cv);
bool isfeasibleprefix() const;
- bool assert_bug(const char *msg);
+ bool assert_bug(const char *msg, ...);
void assert_user_bug(const char *msg);
const model_params params;
bool check_action_enabled(ModelAction *curr);
Thread * take_step(ModelAction *curr);
+ bool should_terminate_execution();
template <typename T>
bool check_recency(ModelAction *curr, const T *rf) const;
* to a trace of all actions performed on the object. */
HashTable<const void *, action_list_t *, uintptr_t, 4> * const obj_map;
- /** Per-object list of actions. Maps an object (i.e., memory location)
- * to a trace of all actions performed on the object. */
- HashTable<const void *, action_list_t *, uintptr_t, 4> * const lock_waiters_map;
-
/** Per-object list of actions. Maps an object (i.e., memory location)
* to a trace of all actions performed on the object. */
HashTable<const void *, action_list_t *, uintptr_t, 4> * const condvar_waiters_map;