#include "stl-model.h"
#include "params.h"
+#include "mutex.h"
+#include <condition_variable>
+
/* Forward declaration */
class Node;
class NodeStack;
void add_thread(Thread *t);
Thread * get_thread(thread_id_t tid) const;
Thread * get_thread(const ModelAction *act) const;
+
+ pthread_t get_pthread_counter() { return pthread_counter; }
+ void incr_pthread_counter() { pthread_counter++; }
+ Thread * get_pthread(pthread_t pid);
+
int get_promise_number(const Promise *promise) const;
bool is_enabled(Thread *t) const;
CycleGraph * const get_mo_graph() { return mo_graph; }
+ HashTable<pthread_mutex_t *, cdsc::mutex *, uintptr_t, 4> mutex_map;
+ HashTable<pthread_cond_t *, cdsc::condition_variable *, uintptr_t, 4> cond_map;
+
SNAPSHOTALLOC
private:
int get_execution_number() const;
+ pthread_t pthread_counter;
ModelChecker *model;
bool process_write(ModelAction *curr, work_queue_t *work);
bool process_fence(ModelAction *curr);
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);
action_list_t action_trace;
SnapVector<Thread *> thread_map;
+ SnapVector<Thread *> pthread_map;
/** Per-object list of actions. Maps an object (i.e., memory location)
* to a trace of all actions performed on the object. */
HashTable<void *, SnapVector<action_list_t> *, uintptr_t, 4> obj_thrd_map;
+// HashTable<pthread_mutex_t *, cdsc::mutex *, uintptr_t, 4> mutex_map;
+
/**
* @brief List of currently-pending promises
*