Merge branch 'master' of /home/git/model-checker

diff --git a/action.cc b/action.cc
index f80de7b322aa4dd288a2c6f8959240028ea9e3a8..20777f96161cfa84c3130c07f11177258481eb5f 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
 
@@ -248,18 +249,27 @@ void ModelAction::set_try_lock(bool obtainedlock) {
                value=VALUE_TRYFAILED;
 }
 
-/** Update the model action's read_from action */
-void ModelAction::read_from(const ModelAction *act)
+/**
+ * Update the model action's read_from action
+ * @param act The action to read from; should be a write
+ * @return True if this read established synchronization
+ */
+bool ModelAction::read_from(const ModelAction *act)
 {
        ASSERT(cv);
        reads_from = act;
        if (act != NULL && this->is_acquire()) {
                rel_heads_list_t release_heads;
                model->get_release_seq_heads(this, &release_heads);
+               int num_heads = release_heads.size();
                for (unsigned int i = 0; i < release_heads.size(); i++)
-                       if (!synchronize_with(release_heads[i]))
+                       if (!synchronize_with(release_heads[i])) {
                                model->set_bad_synchronization();
+                               num_heads--;
+                       }
+               return num_heads > 0;
        }
+       return false;
 }
 
 /**
@@ -292,13 +302,8 @@ bool ModelAction::happens_before(const ModelAction *act) const
        return act->cv->synchronized_since(this);
 }
 
-/**
- * Print nicely-formatted info about this ModelAction
- *
- * @param print_cv True if we want to print clock vector data. Might be false,
- * for instance, in situations where the clock vector might be invalid
- */
-void ModelAction::print(bool print_cv) const
+/** @brief Print nicely-formatted info about this ModelAction */
+void ModelAction::print() const
 {
        const char *type_str, *mo_str;
        switch (this->type) {
@@ -382,7 +387,7 @@ void ModelAction::print(bool print_cv) const
                else
                        printf(" Rf: ?");
        }
-       if (cv && print_cv) {
+       if (cv) {
                printf("\t");
                cv->print();
        } else

diff --git a/action.h b/action.h
index f6fb06236fe0230eb942c38dcc177c081db341bd..d178976a2c8e0206128750b5eaddac1485a4b432 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;
@@ -64,7 +66,7 @@ class ModelAction {
 public:
        ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value = VALUE_NONE);
        ~ModelAction();
-       void print(bool print_cv = true) const;
+       void print() const;
 
        thread_id_t get_tid() const { return tid; }
        action_type get_type() const { return type; }
@@ -103,7 +105,7 @@ public:
 
        void create_cv(const ModelAction *parent = NULL);
        ClockVector * get_cv() const { return cv; }
-       void read_from(const ModelAction *act);
+       bool read_from(const ModelAction *act);
        bool synchronize_with(const ModelAction *act);
 
        bool has_synchronized_with(const ModelAction *act) const;

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..f5501fe07629d39cd588156c8f219495640a6ecc 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;
@@ -122,8 +123,8 @@ bool checkDataRaces() {
 void printRace(struct DataRace * race) {
        printf("Datarace detected\n");
        printf("Location %p\n", race->address);
-       printf("Initial access: thread %u clock %u, iswrite %u\n",race->oldthread,race->oldclock, race->isoldwrite);
-       printf("Second access: thread %u clock %u, iswrite %u\n", race->newaction->get_tid(), race->newaction->get_seq_number() , race->isnewwrite);
+       printf("Initial access: thread %u clock %u, iswrite %u\n", id_to_int(race->oldthread), race->oldclock, race->isoldwrite);
+       printf("Second access: thread %u clock %u, iswrite %u\n", id_to_int(race->newaction->get_tid()), race->newaction->get_seq_number(), race->isnewwrite);
 }
 
 /** This function does race detection for a write on an expanded record. */

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/libthreads.cc b/libthreads.cc
index 4d6a0243c53b7fe880952747236bd8327c04a108..f973176ba8344a497e687b8f452fdefed031fe5e 100644 (file)
--- a/libthreads.cc
+++ b/libthreads.cc
@@ -23,7 +23,7 @@ int thrd_create(thrd_t *t, thrd_start_t start_routine, void *arg)
 int thrd_join(thrd_t t)
 {
        Thread *th = model->get_thread(thrd_to_id(t));
-       model->switch_to_master(new ModelAction(THREAD_JOIN, std::memory_order_seq_cst, th, thrd_to_id(t)));
+       model->switch_to_master(new ModelAction(THREAD_JOIN, std::memory_order_seq_cst, th, id_to_int(thrd_to_id(t))));
        return 0;
 }
 

diff --git a/model.cc b/model.cc
index c9353db71c5bc15c77e802c32285f64f0c697681..e3d9203eea60ec53010d67bb87da20331cfbf642 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()
 {
@@ -171,7 +178,7 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
        } else {
                tid = next->get_tid();
        }
-       DEBUG("*** ModelChecker chose next thread = %d ***\n", tid);
+       DEBUG("*** ModelChecker chose next thread = %d ***\n", id_to_int(tid));
        ASSERT(tid != THREAD_ID_T_NONE);
        return thread_map->get(id_to_int(tid));
 }
@@ -192,7 +199,7 @@ bool ModelChecker::next_execution()
        if (isfinalfeasible()) {
                printf("Earliest divergence point since last feasible execution:\n");
                if (earliest_diverge)
-                       earliest_diverge->print(false);
+                       earliest_diverge->print();
                else
                        printf("(Not set)\n");
 
@@ -317,7 +324,8 @@ void ModelChecker::set_backtracking(ModelAction *act)
                if (!node->set_backtrack(tid))
                        continue;
                DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
-                                       prev->get_tid(), t->get_id());
+                                       id_to_int(prev->get_tid()),
+                                       id_to_int(t->get_id()));
                if (DBG_ENABLED()) {
                        prev->print();
                        act->print();
@@ -787,8 +795,7 @@ bool ModelChecker::isfinalfeasible() {
 
 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
 ModelAction * ModelChecker::process_rmw(ModelAction *act) {
-       int tid = id_to_int(act->get_tid());
-       ModelAction *lastread = get_last_action(tid);
+       ModelAction *lastread = get_last_action(act->get_tid());
        lastread->process_rmw(act);
        if (act->is_rmw() && lastread->get_reads_from()!=NULL) {
                mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
@@ -1169,7 +1176,7 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con
  * @return true, if the ModelChecker is certain that release_heads is complete;
  * false otherwise
  */
-bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *release_heads) const
+bool ModelChecker::release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const
 {
        /* Only check for release sequences if there are no cycles */
        if (mo_graph->checkForCycles())
@@ -1239,7 +1246,7 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel
 
                ModelAction *last = get_last_action(int_to_id(i));
                if (last && (rf->happens_before(last) ||
-                               last->get_type() == THREAD_FINISH))
+                               get_thread(int_to_id(i))->is_complete()))
                        future_ordered = true;
 
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
@@ -1291,13 +1298,13 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel
  * @param act The 'acquire' action that may read from a release sequence
  * @param release_heads A pass-by-reference return parameter. Will be filled
  * with the head(s) of the release sequence(s), if they exists with certainty.
- * @see ModelChecker::release_seq_head
+ * @see ModelChecker::release_seq_heads
  */
 void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads)
 {
        const ModelAction *rf = act->get_reads_from();
        bool complete;
-       complete = release_seq_head(rf, release_heads);
+       complete = release_seq_heads(rf, release_heads);
        if (!complete) {
                /* add act to 'lazy checking' list */
                pending_acq_rel_seq->push_back(act);
@@ -1333,7 +1340,7 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
                const ModelAction *rf = act->get_reads_from();
                rel_heads_list_t release_heads;
                bool complete;
-               complete = release_seq_head(rf, &release_heads);
+               complete = release_seq_heads(rf, &release_heads);
                for (unsigned int i = 0; i < release_heads.size(); i++) {
                        if (!act->has_synchronized_with(release_heads[i])) {
                                if (act->synchronize_with(release_heads[i]))
@@ -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) const
+{
+       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) const
+{
+       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)
@@ -1726,7 +1756,7 @@ bool ModelChecker::take_step() {
        if (has_asserted())
                return false;
 
-       Thread * curr = thread_current();
+       Thread *curr = thread_current();
        if (curr) {
                if (curr->get_state() == THREAD_READY) {
                        ASSERT(priv->current_action);
@@ -1740,22 +1770,23 @@ bool ModelChecker::take_step() {
                        ASSERT(false);
                }
        }
-       Thread * next = scheduler->next_thread(priv->nextThread);
+       Thread *next = scheduler->next_thread(priv->nextThread);
 
        /* Infeasible -> don't take any more steps */
        if (!isfeasible())
                return false;
 
-       if (next)
-               next->set_state(THREAD_RUNNING);
-       DEBUG("(%d, %d)\n", curr ? curr->get_id() : -1, next ? next->get_id() : -1);
+       DEBUG("(%d, %d)\n", curr ? id_to_int(curr->get_id()) : -1,
+                       next ? id_to_int(next->get_id()) : -1);
 
        /* next == NULL -> don't take any more steps */
        if (!next)
                return false;
 
-       if ( next->get_pending() != NULL ) {
-               //restart a pending action
+       next->set_state(THREAD_RUNNING);
+
+       if (next->get_pending() != NULL) {
+               /* restart a pending action */
                set_current_action(next->get_pending());
                next->set_pending(NULL);
                next->set_state(THREAD_READY);

diff --git a/model.h b/model.h
index 7241765d38c5270a33cf25a4986f5dd6fbd9a776..d8dce07cbdf56423e04e2378d2e0715d18025559 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) const;
+       Thread * get_thread(ModelAction *act) const;
 
        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);
@@ -151,7 +148,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_head(const ModelAction *rf, rel_heads_list_t *release_heads) const;
+       bool release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const;
        bool resolve_release_sequences(void *location, work_queue_t *work_queue);
        void do_complete_join(ModelAction *join);
 

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/schedule.cc b/schedule.cc
index b1b41c3d88d579a766d5cd45ccf26815bc551a1e..88200a81cc650617044b4b0449477fbed1afb4e9 100644 (file)
--- a/schedule.cc
+++ b/schedule.cc
@@ -36,7 +36,7 @@ void Scheduler::set_enabled(Thread *t, bool enabled_status) {
  */
 void Scheduler::add_thread(Thread *t)
 {
-       DEBUG("thread %d\n", t->get_id());
+       DEBUG("thread %d\n", id_to_int(t->get_id()));
        set_enabled(t, true);
 }
 
@@ -119,7 +119,7 @@ Thread * Scheduler::get_current_thread() const
 void Scheduler::print() const
 {
        if (current)
-               DEBUG("Current thread: %d\n", current->get_id());
+               DEBUG("Current thread: %d\n", id_to_int(current->get_id()));
        else
                DEBUG("No current thread\n");
 }

diff --git a/threads.cc b/threads.cc
index 09efcae619c06b78ed5c2668473c2b8143b9ea71..ca4b28b1bc850c9ea5bcab709e2d27a9e74e2581 100644 (file)
--- a/threads.cc
+++ b/threads.cc
@@ -105,7 +105,7 @@ int Thread::swap(ucontext_t *ctxt, Thread *t)
 void Thread::complete()
 {
        if (!is_complete()) {
-               DEBUG("completed thread %d\n", get_id());
+               DEBUG("completed thread %d\n", id_to_int(get_id()));
                state = THREAD_COMPLETED;
                if (stack)
                        stack_free(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 {