Merge remote-tracking branch 'origin/master'

diff --git a/action.cc b/action.cc
index f80de7b322aa4dd288a2c6f8959240028ea9e3a8..c5912ff2ef51d5ac5dd0371f96caf7519a5dd2a0 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -7,6 +7,7 @@
 #include "action.h"
 #include "clockvector.h"
 #include "common.h"
+#include "threads.h"
 
 #define ACTION_INITIAL_CLOCK 0
 

diff --git a/action.h b/action.h
index f6fb06236fe0230eb942c38dcc177c081db341bd..8dc88430f2b093969c00ed9f4cff18163072d776 100644 (file)
--- a/action.h
+++ b/action.h
@@ -7,11 +7,13 @@
 
 #include <list>
 #include <cstddef>
+#include <inttypes.h>
 
-#include "threads.h"
 #include "mymemory.h"
-#include "clockvector.h"
 #include "memoryorder.h"
+#include "modeltypes.h"
+
+class ClockVector;
 
 using std::memory_order;
 using std::memory_order_relaxed;

diff --git a/clockvector.cc b/clockvector.cc
index c5bf07709b718f775f0337f6b360f273081c3e08..2b6a4cc6822c6f202decc866c0d25956908dff85 100644 (file)
--- a/clockvector.cc
+++ b/clockvector.cc
@@ -6,6 +6,7 @@
 #include "action.h"
 #include "clockvector.h"
 #include "common.h"
+#include "threads.h"
 
 /**
  * Constructs a new ClockVector, given a parent ClockVector and a first

diff --git a/clockvector.h b/clockvector.h
index 739a336e1adc6c81178686c10da60d411cd903b8..6a902c5215342bae0313d56b3e6cfa8267bd79cf 100644 (file)
--- a/clockvector.h
+++ b/clockvector.h
@@ -5,10 +5,9 @@
 #ifndef __CLOCKVECTOR_H__
 #define __CLOCKVECTOR_H__
 
-#include "threads.h"
 #include "mymemory.h"
+#include "modeltypes.h"
 
-typedef unsigned int modelclock_t;
 /* Forward declaration */
 class ModelAction;
 

diff --git a/cmodelint.cc b/cmodelint.cc
index 228c40f9ec8d02b1a7b9c599a6cf69fc1c4ebf78..6b20c2cc9c800378de4b2255fc94e7a7646516d7 100644 (file)
--- a/cmodelint.cc
+++ b/cmodelint.cc
@@ -1,5 +1,6 @@
 #include "model.h"
 #include "cmodelint.h"
+#include "threads.h"
 
 /** Performs a read action.*/
 uint64_t model_read_action(void * obj, memory_order ord) {

diff --git a/datarace.cc b/datarace.cc
index 293743052858c8029fb685ff246ac071f38b821e..d6e0875c1a5562315b26367a3582452d5c41b07d 100644 (file)
--- a/datarace.cc
+++ b/datarace.cc
@@ -4,6 +4,7 @@
 #include <stdio.h>
 #include <cstring>
 #include "mymemory.h"
+#include "clockvector.h"
 
 struct ShadowTable *root;
 std::vector<struct DataRace *> unrealizedraces;

diff --git a/datarace.h b/datarace.h
index 5bfcb8ad48cc98d007612805c2cc48567dedf984..627b8cc88c7016b27cc2660bdebdf4693e674c40 100644 (file)
--- a/datarace.h
+++ b/datarace.h
@@ -5,8 +5,12 @@
 #ifndef DATARACE_H
 #include "config.h"
 #include <stdint.h>
-#include "clockvector.h"
 #include <vector>
+#include "modeltypes.h"
+
+/* Forward declaration */
+class ClockVector;
+class ModelAction;
 
 struct ShadowTable {
        void * array[65536];

diff --git a/impatomic.cc b/impatomic.cc
index df11202d8ade74f9e677bd8ebb46b2fc1bf062cd..0a35b4b65d0513da09bdc47d81614c7d14f7ab88 100644 (file)
--- a/impatomic.cc
+++ b/impatomic.cc
@@ -1,6 +1,7 @@
 #include "impatomic.h"
 #include "common.h"
 #include "model.h"
+#include "threads.h"
 
 namespace std {
 

diff --git a/librace.cc b/librace.cc
index 38434de70f44d4694ed2a268094e19370a2f87d1..bdd6093a6b6d4ea1f8c9665219a660dc23d1a813 100644 (file)
--- a/librace.cc
+++ b/librace.cc
@@ -5,6 +5,7 @@
 #include "common.h"
 #include "datarace.h"
 #include "model.h"
+#include "threads.h"
 
 void store_8(void *addr, uint8_t val)
 {

diff --git a/model.cc b/model.cc
index c9353db71c5bc15c77e802c32285f64f0c697681..39a7c2170f59fb0ac9b3a7d2160ecb80027283ff 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -12,6 +12,7 @@
 #include "promise.h"
 #include "datarace.h"
 #include "mutex.h"
+#include "threads.h"
 
 #define INITIAL_THREAD_ID      0
 
@@ -99,6 +100,12 @@ int ModelChecker::get_num_threads()
        return priv->next_thread_id;
 }
 
+/** @return The currently executing Thread. */
+Thread * ModelChecker::get_current_thread()
+{
+       return scheduler->get_current_thread();
+}
+
 /** @return a sequence number for a new ModelAction */
 modelclock_t ModelChecker::get_next_seq_num()
 {
@@ -1701,12 +1708,35 @@ void ModelChecker::remove_thread(Thread *t)
        scheduler->remove_thread(t);
 }
 
+/**
+ * @brief Get a Thread reference by its ID
+ * @param tid The Thread's ID
+ * @return A Thread reference
+ */
+Thread * ModelChecker::get_thread(thread_id_t tid)
+{
+       return thread_map->get(id_to_int(tid));
+}
+
+/**
+ * @brief Get a reference to the Thread in which a ModelAction was executed
+ * @param act The ModelAction
+ * @return A Thread reference
+ */
+Thread * ModelChecker::get_thread(ModelAction *act)
+{
+       return get_thread(act->get_tid());
+}
+
 /**
  * Switch from a user-context to the "master thread" context (a.k.a. system
  * context). This switch is made with the intention of exploring a particular
  * model-checking action (described by a ModelAction object). Must be called
  * from a user-thread context.
- * @param act The current action that will be explored. Must not be NULL.
+ *
+ * @param act The current action that will be explored. May be NULL only if
+ * trace is exiting via an assertion (see ModelChecker::set_assert and
+ * ModelChecker::has_asserted).
  * @return Return status from the 'swap' call (i.e., success/fail, 0/-1)
  */
 int ModelChecker::switch_to_master(ModelAction *act)

diff --git a/model.h b/model.h
index 7241765d38c5270a33cf25a4986f5dd6fbd9a776..62c762711bcb8300765483ee075ec9747d412d5f 100644 (file)
--- a/model.h
+++ b/model.h
@@ -10,20 +10,19 @@
 #include <cstddef>
 #include <ucontext.h>
 
-#include "schedule.h"
 #include "mymemory.h"
-#include "libthreads.h"
-#include "threads.h"
 #include "action.h"
-#include "clockvector.h"
 #include "hashtable.h"
 #include "workqueue.h"
 #include "config.h"
+#include "modeltypes.h"
 
 /* Forward declaration */
 class NodeStack;
 class CycleGraph;
 class Promise;
+class Scheduler;
+class Thread;
 
 /** @brief Shorthand for a list of release sequence heads */
 typedef std::vector< const ModelAction *, ModelAlloc<const ModelAction *> > rel_heads_list_t;
@@ -73,14 +72,12 @@ public:
 
        void add_thread(Thread *t);
        void remove_thread(Thread *t);
-       Thread * get_thread(thread_id_t tid) { return thread_map->get(id_to_int(tid)); }
-       Thread * get_thread(ModelAction *act) { return get_thread(act->get_tid()); }
+       Thread * get_thread(thread_id_t tid);
+       Thread * get_thread(ModelAction *act);
 
        thread_id_t get_next_id();
        int get_num_threads();
-
-       /** @return The currently executing Thread. */
-       Thread * get_current_thread() { return scheduler->get_current_thread(); }
+       Thread * get_current_thread();
 
        int switch_to_master(ModelAction *act);
        ClockVector * get_cv(thread_id_t tid);

diff --git a/modeltypes.h b/modeltypes.h
new file mode 100644 (file)
index 0000000..22221cb
--- /dev/null
+++ b/modeltypes.h
@@ -0,0 +1,10 @@
+#ifndef __MODELTYPES_H__
+#define __MODELTYPES_H__
+
+typedef int thread_id_t;
+
+#define THREAD_ID_T_NONE       -1
+
+typedef unsigned int modelclock_t;
+
+#endif /* __MODELTYPES_H__ */

diff --git a/mutex.cc b/mutex.cc
index 51315d94bbf3081959c4c59d1d4c6af727f4a7ea..6ef297a594d6b897110e7663c1f3753f859e0c3a 100644 (file)
--- a/mutex.cc
+++ b/mutex.cc
@@ -1,5 +1,7 @@
 #include "mutex.h"
 #include "model.h"
+#include "threads.h"
+#include "clockvector.h"
 
 namespace std {
 mutex::mutex() {

diff --git a/mutex.h b/mutex.h
index 828aae53f9e1d273900b776ab657907c87e3cd08..53fccb2b89a8974fb26ed8d60f4f1262d3c23396 100644 (file)
--- a/mutex.h
+++ b/mutex.h
@@ -1,7 +1,7 @@
 #ifndef MUTEX_H
 #define MUTEX_H
-#include "threads.h"
-#include "clockvector.h"
+
+#include "modeltypes.h"
 
 namespace std {
        struct mutex_state {

diff --git a/nodestack.cc b/nodestack.cc
index d5425e335dad86614b4e09db71717e0b00dfe2d2..a73765320dac47e97428390fe37bc3b06ba10483 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -4,6 +4,7 @@
 #include "action.h"
 #include "common.h"
 #include "model.h"
+#include "threads.h"
 
 /**
  * @brief Node constructor
@@ -273,6 +274,11 @@ bool Node::is_enabled(thread_id_t tid)
        return thread_id < num_threads && enabled_array[thread_id];
 }
 
+bool Node::has_priority(thread_id_t tid)
+{
+       return fairness[id_to_int(tid)].priority;
+}
+
 /**
  * Add an action to the may_read_from set.
  * @param act is the action to add

diff --git a/nodestack.h b/nodestack.h
index 8df67838c87c362518bdd3100bddcd4663254475..fca063e7a4f86c2462f75a01f006d9c911487a26 100644 (file)
--- a/nodestack.h
+++ b/nodestack.h
@@ -8,11 +8,13 @@
 #include <list>
 #include <vector>
 #include <cstddef>
-#include "threads.h"
+#include <inttypes.h>
+
 #include "mymemory.h"
-#include "clockvector.h"
+#include "modeltypes.h"
 
 class ModelAction;
+class Thread;
 
 /**
  * A flag used for the promise counting/combination problem within a node,
@@ -64,7 +66,7 @@ public:
        bool is_enabled(Thread *t);
        bool is_enabled(thread_id_t tid);
        ModelAction * get_action() { return action; }
-       bool has_priority(thread_id_t tid) {return fairness[id_to_int(tid)].priority;}
+       bool has_priority(thread_id_t tid);
        int get_num_threads() {return num_threads;}
        /** @return the parent Node to this Node; that is, the action that
         * occurred previously in the stack. */

diff --git a/threads.h b/threads.h
index 9456a22f2fe4942b1004a87794fa3474eaeab26b..b69f4265618d1dd2eb4ef18c66aef2b4442a0496 100644 (file)
--- a/threads.h
+++ b/threads.h
@@ -11,10 +11,7 @@
 
 #include "mymemory.h"
 #include "libthreads.h"
-
-typedef int thread_id_t;
-
-#define THREAD_ID_T_NONE       -1
+#include "modeltypes.h"
 
 /** @brief Represents the state of a user Thread */
 typedef enum thread_state {