X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.h;h=3f4ca001aa8c85d85564cf012d10bf37b6182614;hp=9e0b34ba18b25cf642a92dea56321763c23b48ba;hb=745b71256a4b96ddf4843c7f66b11d0cb3daa3cb;hpb=61d1e3ae29b690f69cf77c5a6f836fb36507a694

diff --git a/model.h b/model.h
index 9e0b34ba..3f4ca001 100644
--- a/model.h
+++ b/model.h
@@ -113,6 +113,7 @@ public:
 	void remove_thread(Thread *t);
 	Thread * get_thread(thread_id_t tid) const;
 	Thread * get_thread(const ModelAction *act) const;
+	int get_promise_number(const Promise *promise) const;
 
 	bool is_enabled(Thread *t) const;
 	bool is_enabled(thread_id_t tid) const;
@@ -166,7 +167,11 @@ private:
 
 	Thread * take_step(ModelAction *curr);
 
-	void check_recency(ModelAction *curr, const ModelAction *rf);
+	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;
+
 	ModelAction * get_last_fence_conflict(ModelAction *act) const;
 	ModelAction * get_last_conflict(ModelAction *act) const;
 	void set_backtracking(ModelAction *act);
@@ -174,7 +179,8 @@ private:
 	bool set_latest_backtrack(ModelAction *act);
 	ModelAction * get_next_backtrack();
 	void reset_to_initial_state();
-	bool resolve_promises(ModelAction *curr);
+	int get_promise_to_resolve(const ModelAction *curr) const;
+	bool resolve_promise(ModelAction *curr, unsigned int promise_idx);
 	void compute_promises(ModelAction *curr);
 	void compute_relseq_breakwrites(ModelAction *curr);
 
@@ -194,7 +200,7 @@ private:
 	template <typename rf_type>
 	bool r_modification_order(ModelAction *curr, const rf_type *rf);
 
-	bool w_modification_order(ModelAction *curr);
+	bool w_modification_order(ModelAction *curr, std::vector< ModelAction *, ModelAlloc<ModelAction *> > *send_fv);
 	void get_release_seq_heads(ModelAction *acquire, ModelAction *read, rel_heads_list_t *release_heads);
 	bool release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads, struct release_seq *pending) const;
 	bool resolve_release_sequences(void *location, work_queue_t *work_queue);