clock: add modelclock_t typedef, use 'unsigned int'

Clocks should be unsigned and documented as their own 'modelclock_t' type.

diff --git a/action.h b/action.h
index e342e63271d223417e55393d4d8bc941b1d2a0ba..0200111df387e586c4346c1858c0f139a6c6f4ce 100644 (file)
--- a/action.h
+++ b/action.h
@@ -11,6 +11,8 @@
 #include "threads.h"
 #include "libatomic.h"
 #include "mymemory.h"
+#include "clockvector.h"
+
 #define VALUE_NONE -1
 
 typedef enum action_type {
@@ -39,7 +41,7 @@ public:
        action_type get_type() const { return type; }
        memory_order get_mo() const { return order; }
        void * get_location() const { return location; }
-       int get_seq_number() const { return seq_number; }
+       modelclock_t get_seq_number() const { return seq_number; }
        int get_value() const { return value; }
 
        Node * get_node() const { return node; }
@@ -92,7 +94,7 @@ private:
         * saved on the NodeStack. */
        Node *node;
        
-       int seq_number;
+       modelclock_t seq_number;
 
        /** The clock vector stored with this action; only needed if this
         * action is a store release? */

diff --git a/clockvector.cc b/clockvector.cc
index 1956b18a127742a3584b0abfa74233fb92332c3c..5a7c5349b3cd98ad446e0eb90189cd4b695dbbfa 100644 (file)
--- a/clockvector.cc
+++ b/clockvector.cc
@@ -18,10 +18,10 @@
 ClockVector::ClockVector(ClockVector *parent, ModelAction *act)
 {
        num_threads = model->get_num_threads();
-       clock = (int *)MYMALLOC(num_threads * sizeof(int));
+       clock = (modelclock_t *)MYMALLOC(num_threads * sizeof(int));
        memset(clock, 0, num_threads * sizeof(int));
        if (parent)
-               std::memcpy(clock, parent->clock, parent->num_threads * sizeof(int));
+               std::memcpy(clock, parent->clock, parent->num_threads * sizeof(modelclock_t));
 
        if (act)
                clock[id_to_int(act->get_tid())] = act->get_seq_number();
@@ -40,14 +40,14 @@ ClockVector::~ClockVector()
  */
 void ClockVector::merge(ClockVector *cv)
 {
-       int *clk = clock;
+       modelclock_t *clk = clock;
        bool resize = false;
 
        ASSERT(cv != NULL);
 
        if (cv->num_threads > num_threads) {
                resize = true;
-               clk = (int *)MYMALLOC(cv->num_threads * sizeof(int));
+               clk = (modelclock_t *)MYMALLOC(cv->num_threads * sizeof(modelclock_t));
        }
 
        /* Element-wise maximum */
@@ -103,5 +103,5 @@ void ClockVector::print() const
        int i;
        printf("CV: (");
        for (i = 0; i < num_threads; i++)
-               printf("%2d%s", clock[i], (i == num_threads - 1) ? ")\n" : ", ");
+               printf("%2u%s", clock[i], (i == num_threads - 1) ? ")\n" : ", ");
 }

diff --git a/clockvector.h b/clockvector.h
index 470914b1ae2b08b19248b5aba29142c990232b4f..f56d8d5089b28a86b368214b9b68ae5cf1feed59 100644 (file)
--- a/clockvector.h
+++ b/clockvector.h
@@ -8,6 +8,7 @@
 #include "threads.h"
 #include "mymemory.h"
 
+typedef unsigned int modelclock_t;
 /* Forward declaration */
 class ModelAction;
 
@@ -24,7 +25,7 @@ public:
        MEMALLOC
 private:
        /** @brief Holds the actual clock data, as an array. */
-       int *clock;
+       modelclock_t *clock;
 
        /** @brief The number of threads recorded in clock (i.e., its length).  */
        int num_threads;

diff --git a/model.cc b/model.cc
index f12e4d27db44af7b3593067c806c539ce930ced9..4e2bb0250f05480ca3ccde1f6b99c26afe344a8b 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -78,7 +78,7 @@ int ModelChecker::get_num_threads()
 }
 
 /** @returns a sequence number for a new ModelAction */
-int ModelChecker::get_next_seq_num()
+modelclock_t ModelChecker::get_next_seq_num()
 {
        return ++used_sequence_numbers;
 }

diff --git a/model.h b/model.h
index 4635644b6b40b6bf1cfda8d08fc587b3a0fe67bb..22430378298aaa60c7755e40be665fe68d1bd275 100644 (file)
--- a/model.h
+++ b/model.h
@@ -18,6 +18,7 @@
 #include "libatomic.h"
 #include "threads.h"
 #include "action.h"
+#include "clockvector.h"
 
 /* Forward declaration */
 class NodeStack;
@@ -57,7 +58,7 @@ public:
 
        thread_id_t get_next_id();
        int get_num_threads();
-       int get_next_seq_num();
+       modelclock_t get_next_seq_num();
 
        int switch_to_master(ModelAction *act);
 
@@ -66,7 +67,7 @@ public:
        MEMALLOC
 private:
        int next_thread_id;
-       int used_sequence_numbers;
+       modelclock_t used_sequence_numbers;
        int num_executions;
 
        ModelAction * get_last_conflict(ModelAction *act);