Merge branch 'master' into brian

diff --git a/action.cc b/action.cc
index d9aae2d4958253977e9f0256fb87076174e94a67..39b0f7f6d4847207f0dc2a18da5b0edeffa5776a 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -10,6 +10,7 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, int
        order(order),
        location(loc),
        value(value),
+       reads_from(NULL),
        cv(NULL)
 {
        Thread *t = thread_current();
@@ -132,6 +133,7 @@ void ModelAction::read_from(const ModelAction *act)
        ASSERT(cv);
        if (act->is_release() && this->is_acquire())
                cv->merge(act->cv);
+       reads_from = act;
        value = act->value;
 }
 
@@ -178,8 +180,10 @@ void ModelAction::print(void) const
                type_str = "unknown type";
        }
 
-       printf("(%3d) Thread: %-2d    Action: %-13s    MO: %d    Loc: %14p    Value: %d",
+       printf("(%3d) Thread: %-2d    Action: %-13s    MO: %d    Loc: %14p    Value: %-4d",
                        seq_number, id_to_int(tid), type_str, order, location, value);
+       if (reads_from)
+               printf(" Rf: %d", reads_from->get_seq_number());
        if (cv) {
                printf("\t");
                cv->print();

diff --git a/action.h b/action.h
index 3e4480419c03941413307ebba6a6e27a77372109..30c8a35b80ed7681ce74bc5388c0667b9b4e4fec 100644 (file)
--- a/action.h
+++ b/action.h
@@ -48,10 +48,10 @@ public:
        void * get_location() const { return location; }
        modelclock_t get_seq_number() const { return seq_number; }
        int get_value() const { return value; }
+       const ModelAction * get_reads_from() const { return reads_from; }
 
        Node * get_node() const { return node; }
        void set_node(Node *n) { node = n; }
-       void set_value(int val) { value = val; }
 
        bool is_read() const;
        bool is_write() const;
@@ -96,6 +96,9 @@ private:
         * should probably be something longer. */
        int value;
 
+       /** The action that this action reads from. Only valid for reads */
+       const ModelAction *reads_from;
+
        /** A back reference to a Node in NodeStack, if this ModelAction is
         * saved on the NodeStack. */
        Node *node;

diff --git a/clockvector.cc b/clockvector.cc
index 162a7c2550db61c3845885349a01b76e6fd84838..190f9216a92b61ad68df0990775d4c978aaa53f9 100644 (file)
--- a/clockvector.cc
+++ b/clockvector.cc
@@ -34,11 +34,11 @@ ClockVector::~ClockVector()
 }
 
 /**
- * Merge a clock vector into this vector, using a pairwise vector. The
+ * Merge a clock vector into this vector, using a pairwise comparison. The
  * resulting vector length will be the maximum length of the two being merged.
  * @param cv is the ClockVector being merged into this vector.
  */
-void ClockVector::merge(ClockVector *cv)
+void ClockVector::merge(const ClockVector *cv)
 {
        modelclock_t *clk = clock;
        bool resize = false;

diff --git a/clockvector.h b/clockvector.h
index 1428886c80f692891a8103be8e721bc07644cdf7..56037eb6bfcd2f37a5110d12a7f733e79faad8b0 100644 (file)
--- a/clockvector.h
+++ b/clockvector.h
@@ -16,7 +16,7 @@ class ClockVector {
 public:
        ClockVector(ClockVector *parent = NULL, ModelAction *act = NULL);
        ~ClockVector();
-       void merge(ClockVector *cv);
+       void merge(const ClockVector *cv);
        bool synchronized_since(const ModelAction *act) const;
 
        void print() const;

diff --git a/libatomic.cc b/libatomic.cc
index a07653303c86348dfc5fe16fee790f137e478a11..531731966a862cacd2f704fa26163f6851cd6d52 100644 (file)
--- a/libatomic.cc
+++ b/libatomic.cc
@@ -11,10 +11,9 @@ void atomic_store_explicit(struct atomic_object *obj, int value, memory_order or
 
 int atomic_load_explicit(struct atomic_object *obj, memory_order order)
 {
-       int value = obj->value;
        DBG();
-       model->switch_to_master(new ModelAction(ATOMIC_READ, order, obj, value));
-       return value;
+       model->switch_to_master(new ModelAction(ATOMIC_READ, order, obj));
+       return thread_current()->get_return_value();
 }
 
 void atomic_init(struct atomic_object *obj, int value)

diff --git a/main.cc b/main.cc
index 19f12f182494685d718a963b23ee01d3ef3ffcb0..c9ac1d0663206feccb6d05d43803689e7214574e 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -53,7 +53,7 @@ static void thread_wait_finish(void) {
 
 /** The real_main function contains the main model checking loop. */
 
-void real_main() {
+static void real_main() {
        thrd_t user_thread;
        ucontext_t main_context;
 

diff --git a/model.cc b/model.cc
index cde6213ada34c0b3c6a9a5328474ddcf9371a726..d80d1d27be741c749d9f94db4e8c5c9f8c28e6d4 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -272,6 +272,19 @@ void ModelChecker::check_current_action(void)
        set_backtracking(curr);
 
        add_action_to_lists(curr);
+
+       /* Assign reads_from values */
+       /* TODO: perform release/acquire synchronization here; include
+        * reads_from as ModelAction member? */
+       Thread *th = get_thread(curr->get_tid());
+       int value = VALUE_NONE;
+       if (curr->is_read()) {
+               const ModelAction *reads_from = curr->get_node()->get_next_read_from();
+               value = reads_from->get_value();
+               /* Assign reads_from, perform release/acquire synchronization */
+               curr->read_from(reads_from);
+       }
+       th->set_return_value(value);
 }
 
 /**

diff --git a/nodestack.cc b/nodestack.cc
index 10f7a72b5ef3ff5705fdbe29771def18212ecf11..2416ed7c5b35d23deadd2f2681cd890a926e7f98 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -130,6 +130,22 @@ void Node::add_read_from(const ModelAction *act)
        may_read_from.push_back(act);
 }
 
+/**
+ * Gets the next 'may_read_from' action from this Node. Only valid for a node
+ * where this->action is a 'read'.
+ * @todo Perform reads_from backtracking/replay properly, so that this function
+ * may remove elements from may_read_from
+ * @return The first element in may_read_from
+ */
+const ModelAction * Node::get_next_read_from() {
+       const ModelAction *act;
+       ASSERT(!may_read_from.empty());
+       act = may_read_from.front();
+       /* TODO: perform reads_from replay properly */
+       /* may_read_from.pop_front(); */
+       return act;
+}
+
 void Node::explore(thread_id_t tid)
 {
        int i = id_to_int(tid);

diff --git a/nodestack.h b/nodestack.h
index c09b628b4ffc9a8f91a7997f628f3234c1e6b7df..11cbdfa801d772d70e210668db374fd71f718b71 100644 (file)
--- a/nodestack.h
+++ b/nodestack.h
@@ -44,6 +44,7 @@ public:
        Node * get_parent() const { return parent; }
 
        void add_read_from(const ModelAction *act);
+       const ModelAction * get_next_read_from();
 
        void print();
        void print_may_read_from();