X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.h;h=d5dc42266769004d542d72f472f6e1029c1a7e5c;hb=1af30302f46d984b38a02a3f21ec53a5a9de0f71;hp=d8dce07cbdf56423e04e2378d2e0715d18025559;hpb=f4d77c40b4029cdc18f4aaa5a4e01dfbcfca5f7b;p=model-checker.git

diff --git a/model.h b/model.h
index d8dce07..d5dc422 100644
--- a/model.h
+++ b/model.h
@@ -49,12 +49,25 @@ struct PendingFutureValue {
  */
 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:
@@ -76,7 +89,7 @@ public:
 	Thread * get_thread(ModelAction *act) const;
 
 	thread_id_t get_next_id();
-	int get_num_threads();
+	unsigned int get_num_threads();
 	Thread * get_current_thread();
 
 	int switch_to_master(ModelAction *act);
@@ -86,7 +99,8 @@ public:
 	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();
@@ -97,6 +111,7 @@ public:
 	void set_bad_synchronization() { bad_synchronization = true; }
 
 	const model_params params;
+	Scheduler * get_scheduler() { return scheduler;}
 
 	MEMALLOC
 private:
@@ -148,7 +163,7 @@ private:
 	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_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const;
+	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);
 	void do_complete_join(ModelAction *join);
 
@@ -172,12 +187,12 @@ private:
 	std::vector<struct PendingFutureValue> *futurevalues;
 
 	/**
-	 * List of acquire actions that might synchronize with one or more
-	 * release sequence. Release sequences might be determined lazily as
-	 * promises are fulfilled and modification orders are established. Each
-	 * ModelAction in this list must be an acquire operation.
+	 * List of pending release sequences. Release sequences might be
+	 * determined lazily as promises are fulfilled and modification orders
+	 * are established. Each entry in the list may only be partially
+	 * filled, depending on its pending status.
 	 */
-	std::vector<ModelAction *> *pending_acq_rel_seq;
+	std::vector<struct release_seq *> *pending_rel_seqs;
 
 	std::vector<ModelAction *> *thrd_last_action;
 	NodeStack *node_stack;