From f646d6a9d7c201e54a3f7eb1f026064d4136cf2e Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Tue, 10 Apr 2012 15:00:13 -0700
Subject: [PATCH] threads_internal: pass the current 'action' to the internal
 thread system

I build a ModelAction object to represent the properties of the current action
that are relevant to the model checker. This action should be passed from the
basic action (atomic_load, atomic_store, thread_yield, etc.) into our thread
library and eventually to the model checker.

I don't use these actions yet, but they will be shortly.
---
 libatomic.cc       | 5 +++--
 libthreads.cc      | 9 ++++++---
 model.cc           | 2 ++
 model.h            | 3 +++
 threads_internal.h | 3 ++-
 5 files changed, 16 insertions(+), 6 deletions(-)

diff --git a/libatomic.cc b/libatomic.cc
index daf058a..dc715b2 100644
--- a/libatomic.cc
+++ b/libatomic.cc
@@ -1,13 +1,14 @@
 #include "libatomic.h"
+#include "model.h"
 #include "threads_internal.h"
 
 void atomic_store_explicit(struct atomic_object *obj, int value, memory_order order)
 {
-	thread_switch_to_master();
+	thread_switch_to_master(new ModelAction(ATOMIC_WRITE, order, obj, value));
 }
 
 int atomic_load_explicit(struct atomic_object *obj, memory_order order)
 {
-	thread_switch_to_master();
+	thread_switch_to_master(new ModelAction(ATOMIC_READ, order, obj, VALUE_NONE));
 	return 0;
 }
diff --git a/libthreads.cc b/libthreads.cc
index 42e9198..fb828b1 100644
--- a/libthreads.cc
+++ b/libthreads.cc
@@ -98,11 +98,12 @@ static void thread_wait_finish(void)
 	while (!thread_system_next());
 }
 
-int thread_switch_to_master()
+int thread_switch_to_master(ModelAction *act)
 {
 	struct thread *old, *next;
 
 	DBG();
+	model->set_current_action(act);
 	old = thread_current();
 	old->state = THREAD_READY;
 	next = model->system_thread;
@@ -140,12 +141,14 @@ void thread_join(struct thread *t)
 {
 	int ret = 0;
 	while (t->state != THREAD_COMPLETED && !ret)
-		ret = thread_switch_to_master();
+		/* seq_cst is just a 'don't care' parameter */
+		ret = thread_switch_to_master(new ModelAction(THREAD_JOIN, memory_order_seq_cst, NULL, VALUE_NONE));
 }
 
 int thread_yield(void)
 {
-	return thread_switch_to_master();
+	/* seq_cst is just a 'don't care' parameter */
+	return thread_switch_to_master(new ModelAction(THREAD_YIELD, memory_order_seq_cst, NULL, VALUE_NONE));
 }
 
 struct thread *thread_current(void)
diff --git a/model.cc b/model.cc
index 19194cd..88d5ce3 100644
--- a/model.cc
+++ b/model.cc
@@ -11,6 +11,8 @@ ModelChecker::ModelChecker()
 	this->used_thread_id = 0;
 	/* Initialize default scheduler */
 	this->scheduler = new DefaultScheduler();
+
+	this->current_action = NULL;
 }
 
 ModelChecker::~ModelChecker()
diff --git a/model.h b/model.h
index d3229b2..205b8d0 100644
--- a/model.h
+++ b/model.h
@@ -37,8 +37,11 @@ public:
 	void add_system_thread(struct thread *t);
 	void assign_id(struct thread *t);
 
+	void set_current_action(ModelAction *act) { current_action = act; }
+
 private:
 	int used_thread_id;
+	class ModelAction *current_action;
 };
 
 extern ModelChecker *model;
diff --git a/threads_internal.h b/threads_internal.h
index 37b446c..0fde64b 100644
--- a/threads_internal.h
+++ b/threads_internal.h
@@ -1,8 +1,9 @@
 #ifndef __THREADS_INTERNAL_H__
 #define __THREADS_INTERNAL_H__
 
+#include "model.h"
 #include "libthreads.h"
 
-int thread_switch_to_master();
+int thread_switch_to_master(ModelAction *act);
 
 #endif /* __THREADS_INTERNAL_H__ */
-- 
2.34.1