X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=execution.h;h=ab4df362bcd89544402fafb701d2b982bb5c7be7;hb=741d3d1160343d8545a783a2d05d3d0562b1c737;hp=bb4ebb08f0b67cb3b30af855196c3b2b217b8013;hpb=dd1f275d3e8042282bad49cf85fddfc2a5735166;p=model-checker.git

diff --git a/execution.h b/execution.h
index bb4ebb0..ab4df36 100644
--- a/execution.h
+++ b/execution.h
@@ -141,7 +141,7 @@ private:
 	ModelAction * check_current_action(ModelAction *curr);
 	bool initialize_curr_action(ModelAction **curr);
 	bool process_read(ModelAction *curr);
-	bool process_write(ModelAction *curr);
+	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);
@@ -160,7 +160,8 @@ private:
 	void set_backtracking(ModelAction *act);
 	bool set_latest_backtrack(ModelAction *act);
 	Promise * pop_promise_to_resolve(const ModelAction *curr);
-	bool resolve_promise(ModelAction *curr, Promise *promise);
+	bool resolve_promise(ModelAction *curr, Promise *promise,
+			work_queue_t *work);
 	void compute_promises(ModelAction *curr);
 	void compute_relseq_breakwrites(ModelAction *curr);