From: Brian Norris <banorris@uci.edu>
Date: Fri, 6 Jul 2012 00:31:30 +0000 (-0700)
Subject: clock: add modelclock_t typedef, use 'unsigned int'
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=75ecaf106e4fc0d2ad2f3d82d089cf8a9956e41a

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 e342e632..0200111d 100644
--- 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 1956b18a..5a7c5349 100644
--- 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 470914b1..f56d8d50 100644
--- 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 f12e4d27..4e2bb025 100644
--- 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 4635644b..22430378 100644
--- 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);