.*.swp
*.so
*~
+<<<<<<< HEAD
+=======
*.*~
+>>>>>>> subramanian
# files in this directory
/model
USER_O=userprog.o
USER_H=libthreads.h libatomic.h
-MODEL_CC=libthreads.cc schedule.cc libatomic.cc model.cc threads.cc tree.cc librace.cc action.cc main.cc snapshot-interface.cc
-MODEL_O=libthreads.o schedule.o libatomic.o model.o threads.o tree.o librace.o action.o main.o snapshot-interface.o
-MODEL_H=libthreads.h schedule.h common.h libatomic.h model.h threads.h tree.h librace.h action.h snapshot-interface.h
+MODEL_CC=libthreads.cc schedule.cc libatomic.cc model.cc malloc.c threads.cc tree.cc librace.cc action.cc nodestack.cc clockvector.cc main.cc snapshot-interface.cc
+MODEL_O=libthreads.o schedule.o libatomic.o model.o malloc.o threads.o tree.o librace.o action.o nodestack.o clockvector.o main.o snapshot-interface.o
+MODEL_H=libthreads.h schedule.h common.h libatomic.h model.h threads.h tree.h librace.h action.h nodestack.h clockvector.h snapshot-interface.h
SHMEM_CC=snapshot.cc malloc.c mymemory.cc
SHMEM_O=snapshot.o malloc.o mymemory.o
/* Forward declaration */
class TreeNode;
+class Node;
class ModelAction {
public:
action_type get_type() { return type; }
memory_order get_mo() { return order; }
void * get_location() { return location; }
- int get_seq_number() { return seq_number; }
+ int get_seq_number() const { return seq_number; }
- TreeNode * get_node() { return node; }
- void set_node(TreeNode *n) { node = n; }
+ TreeNode * get_treenode() { return treenode; }
+ void set_node(TreeNode *n) { treenode = n; }
+ Node * get_node() { return node; }
+ void set_node(Node *n) { node = n; }
bool is_read();
bool is_write();
bool same_var(ModelAction *act);
bool same_thread(ModelAction *act);
bool is_dependent(ModelAction *act);
+
+ inline bool operator <(const ModelAction& act) const {
+ return get_seq_number() < act.get_seq_number();
+ }
+ inline bool operator >(const ModelAction& act) const {
+ return get_seq_number() > act.get_seq_number();
+ }
MEMALLOC
private:
action_type type;
void *location;
thread_id_t tid;
int value;
- TreeNode *node;
+ TreeNode *treenode;
+ Node *node;
int seq_number;
};
--- /dev/null
+#include <algorithm>
+#include <cstring>
+
+#include "model.h"
+#include "action.h"
+#include "clockvector.h"
+#include "common.h"
+
+ClockVector::ClockVector(ClockVector *parent, ModelAction *act)
+{
+ num_threads = parent ? parent->num_threads : 1;
+ if (act && act->get_type() == THREAD_CREATE)
+ num_threads++;
+ clock = (int *)myMalloc(num_threads * sizeof(int));
+ if (parent)
+ std::memcpy(clock, parent->clock, parent->num_threads * sizeof(int));
+ else
+ clock[0] = 0;
+
+ if (act)
+ clock[id_to_int(act->get_tid())] = act->get_seq_number();
+}
+
+ClockVector::~ClockVector()
+{
+ myFree(clock);
+}
+
+void ClockVector::merge(ClockVector *cv)
+{
+ int *clk = clock;
+ bool resize = false;
+
+ ASSERT(cv != NULL);
+
+ if (cv->num_threads > num_threads) {
+ resize = true;
+ clk = (int *)myMalloc(cv->num_threads * sizeof(int));
+ }
+
+ /* Element-wise maximum */
+ for (int i = 0; i < num_threads; i++)
+ clk[i] = std::max(clock[i], cv->clock[i]);
+
+ if (resize) {
+ for (int i = num_threads; i < cv->num_threads; i++)
+ clk[i] = cv->clock[i];
+ num_threads = cv->num_threads;
+ myFree(clock);
+ }
+ clock = clk;
+}
+
+bool ClockVector::happens_before(ModelAction *act, thread_id_t id)
+{
+ int i = id_to_int(id);
+
+ if (i < num_threads)
+ return act->get_seq_number() < clock[i];
+ return false;
+}
--- /dev/null
+#ifndef __CLOCKVECTOR_H__
+#define __CLOCKVECTOR_H__
+
+#include "threads.h"
+
+/* Forward declaration */
+class ModelAction;
+
+class ClockVector {
+public:
+ ClockVector(ClockVector *parent = NULL, ModelAction *act = NULL);
+ ~ClockVector();
+ void merge(ClockVector *cv);
+ bool happens_before(ModelAction *act, thread_id_t id);
+private:
+ int *clock;
+ int num_threads;
+};
+
+#endif /* __CLOCKVECTOR_H__ */
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_NONE));
- return obj->value;
+ model->switch_to_master(new ModelAction(ATOMIC_READ, order, obj, value));
+ return value;
}
void atomic_init(struct atomic_object *obj, int value)
void store_8(void *addr, uint8_t val)
{
DEBUG("addr = %p, val = %" PRIu8 "\n", addr, val);
+ (*(uint8_t *)addr) = val;
}
void store_16(void *addr, uint16_t val)
{
DEBUG("addr = %p, val = %" PRIu16 "\n", addr, val);
+ (*(uint16_t *)addr) = val;
}
void store_32(void *addr, uint32_t val)
{
DEBUG("addr = %p, val = %" PRIu32 "\n", addr, val);
+ (*(uint32_t *)addr) = val;
}
void store_64(void *addr, uint64_t val)
{
DEBUG("addr = %p, val = %" PRIu64 "\n", addr, val);
+ (*(uint64_t *)addr) = val;
}
uint8_t load_8(void *addr)
{
DEBUG("addr = %p\n", addr);
- return 0;
+ return *((uint8_t *)addr);
}
uint16_t load_16(void *addr)
{
DEBUG("addr = %p\n", addr);
- return 0;
+ return *((uint16_t *)addr);
}
uint32_t load_32(void *addr)
{
DEBUG("addr = %p\n", addr);
- return 0;
+ return *((uint32_t *)addr);
}
uint64_t load_64(void *addr)
{
DEBUG("addr = %p\n", addr);
- return 0;
+ return *((uint64_t *)addr);
}
-#include <stdlib.h>
-
#include "libthreads.h"
-#include "schedule.h"
#include "common.h"
#include "threads.h"
}
ModelChecker::ModelChecker()
-{
- /* First thread created will have id INITIAL_THREAD_ID */
- this->next_thread_id = INITIAL_THREAD_ID;
- used_sequence_numbers = 0;
+ :
/* Initialize default scheduler */
- this->scheduler = new Scheduler();
-
- num_executions = 0;
- this->current_action = NULL;
- this->exploring = NULL;
- this->nextThread = THREAD_ID_T_NONE;
-
- rootNode = new TreeNode();
- currentNode = rootNode;
- action_trace = new action_list_t();
+ scheduler(new Scheduler()),
+ /* First thread created will have id INITIAL_THREAD_ID */
+ next_thread_id(INITIAL_THREAD_ID),
+ used_sequence_numbers(0),
+
+ num_executions(0),
+ current_action(NULL),
+ exploring(NULL),
+ nextThread(THREAD_ID_T_NONE),
+ action_trace(new action_list_t()),
+ rootNode(new TreeNode()),
+ currentNode(rootNode)
+{
}
ModelChecker::~ModelChecker()
free_action_list(action_trace);
- delete this->scheduler;
+ delete scheduler;
delete rootNode;
}
current_action = NULL;
next_thread_id = INITIAL_THREAD_ID;
used_sequence_numbers = 0;
+ nextThread = 0;
/* scheduler reset ? */
}
ModelAction *next;
thread_id_t tid;
+ /* Have we completed exploring the preselected path? */
+ if (exploring == NULL)
+ return THREAD_ID_T_NONE;
+
+ /* Else, we are trying to replay an execution */
+ exploring->advance_state();
+
+ ASSERT(exploring->get_state() != NULL);
+
next = exploring->get_state();
if (next == exploring->get_diverge()) {
- TreeNode *node = next->get_node();
+ TreeNode *node = next->get_treenode();
/* Reached divergence point; discard our current 'exploring' */
DEBUG("*** Discard 'Backtrack' object ***\n");
return tid;
}
-thread_id_t ModelChecker::advance_backtracking_state()
-{
- /* Have we completed exploring the preselected path? */
- if (exploring == NULL)
- return THREAD_ID_T_NONE;
-
- /* Else, we are trying to replay an execution */
- exploring->advance_state();
-
- ASSERT(exploring->get_state() != NULL);
-
- return get_next_replay_thread();
-}
-
bool ModelChecker::next_execution()
{
DBG();
}
model->reset_to_initial_state();
- nextThread = get_next_replay_thread();
return true;
}
if (prev == NULL)
return;
- node = prev->get_node();
+ node = prev->get_treenode();
while (t && !node->is_enabled(t))
t = t->get_parent();
void ModelChecker::check_current_action(void)
{
- ModelAction *next = this->current_action;
-
- if (!next) {
+ ModelAction *curr = this->current_action;
+ current_action = NULL;
+ if (!curr) {
DEBUG("trying to push NULL action...\n");
return;
}
- current_action = NULL;
- nextThread = advance_backtracking_state();
- next->set_node(currentNode);
- set_backtracking(next);
- currentNode = currentNode->explore_child(next);
- this->action_trace->push_back(next);
+
+ nextThread = get_next_replay_thread();
+ curr->set_node(currentNode);
+ set_backtracking(curr);
+ currentNode = currentNode->explore_child(curr);
+ this->action_trace->push_back(curr);
}
void ModelChecker::print_summary(void)
ModelAction * get_last_conflict(ModelAction *act);
void set_backtracking(ModelAction *act);
- thread_id_t advance_backtracking_state();
thread_id_t get_next_replay_thread();
Backtrack * get_next_backtrack();
void reset_to_initial_state();
--- /dev/null
+#include "nodestack.h"
+#include "action.h"
+#include "common.h"
+
+int Node::total_nodes = 0;
+
+Node::Node(ModelAction *act, Node *parent)
+ : action(act),
+ num_threads(parent ? parent->num_threads : 1),
+ explored_children(num_threads),
+ backtrack(num_threads)
+{
+ total_nodes++;
+ if (act && act->get_type() == THREAD_CREATE) {
+ num_threads++;
+ explored_children.resize(num_threads);
+ backtrack.resize(num_threads);
+ }
+}
+
+Node::~Node()
+{
+ if (action)
+ delete action;
+}
+
+void Node::print()
+{
+ if (action)
+ action->print();
+ else
+ printf("******** empty action ********\n");
+}
+
+bool Node::has_been_explored(thread_id_t tid)
+{
+ int id = id_to_int(tid);
+ return explored_children[id];
+}
+
+bool Node::backtrack_empty()
+{
+ unsigned int i;
+ for (i = 0; i < backtrack.size(); i++)
+ if (backtrack[i] == true)
+ return false;
+ return true;
+}
+
+void Node::explore_child(ModelAction *act)
+{
+ act->set_node(this);
+ explore(act->get_tid());
+}
+
+bool Node::set_backtrack(thread_id_t id)
+{
+ int i = id_to_int(id);
+ if (backtrack[i])
+ return false;
+ backtrack[i] = true;
+ return true;
+}
+
+thread_id_t Node::get_next_backtrack()
+{
+ /* TODO: find next backtrack */
+ unsigned int i;
+ for (i = 0; i < backtrack.size(); i++)
+ if (backtrack[i] == true)
+ break;
+ if (i >= backtrack.size())
+ return THREAD_ID_T_NONE;
+ backtrack[i] = false;
+ return int_to_id(i);
+}
+
+bool Node::is_enabled(Thread *t)
+{
+ return id_to_int(t->get_id()) < num_threads;
+}
+
+void Node::explore(thread_id_t tid)
+{
+ int i = id_to_int(tid);
+ backtrack[i] = false;
+ explored_children[i] = true;
+}
+
+static void clear_node_list(node_list_t *list, node_list_t::iterator start,
+ node_list_t::iterator end)
+{
+ node_list_t::iterator it;
+
+ for (it = start; it != end; it++)
+ delete (*it);
+ list->erase(start, end);
+}
+
+NodeStack::NodeStack()
+{
+ node_list.push_back(new Node());
+ iter = node_list.begin();
+}
+
+NodeStack::~NodeStack()
+{
+ clear_node_list(&node_list, node_list.begin(), node_list.end());
+}
+
+void NodeStack::print()
+{
+ node_list_t::iterator it;
+ printf("............................................\n");
+ printf("NodeStack printing node_list:\n");
+ for (it = node_list.begin(); it != node_list.end(); it++) {
+ if (it == this->iter)
+ printf("vvv following action is the current iterator vvv\n");
+ (*it)->print();
+ }
+ printf("............................................\n");
+}
+
+ModelAction * NodeStack::explore_action(ModelAction *act)
+{
+ DBG();
+
+ ASSERT(!node_list.empty());
+
+ if (get_head()->has_been_explored(act->get_tid())) {
+ /* Discard duplicate ModelAction */
+ delete act;
+ iter++;
+ } else { /* Diverging from previous execution */
+ /* Clear out remainder of list */
+ node_list_t::iterator it = iter;
+ it++;
+ clear_node_list(&node_list, it, node_list.end());
+
+ /* Record action */
+ get_head()->explore_child(act);
+ node_list.push_back(new Node(act, get_head()));
+ iter++;
+ }
+ return (*iter)->get_action();
+}
+
+Node * NodeStack::get_head()
+{
+ if (node_list.empty())
+ return NULL;
+ return *iter;
+}
+
+Node * NodeStack::get_next()
+{
+ node_list_t::iterator it = iter;
+ if (node_list.empty()) {
+ DEBUG("Empty\n");
+ return NULL;
+ }
+ it++;
+ if (it == node_list.end()) {
+ DEBUG("At end\n");
+ return NULL;
+ }
+ return *it;
+}
+
+void NodeStack::reset_execution()
+{
+ iter = node_list.begin();
+}
--- /dev/null
+#ifndef __NODESTACK_H__
+#define __NODESTACK_H__
+
+#include <list>
+#include <vector>
+#include <cstddef>
+#include "threads.h"
+
+class ModelAction;
+
+class Node {
+public:
+ Node(ModelAction *act = NULL, Node *parent = NULL);
+ ~Node();
+ /* return true = thread choice has already been explored */
+ bool has_been_explored(thread_id_t tid);
+ /* return true = backtrack set is empty */
+ bool backtrack_empty();
+ void explore_child(ModelAction *act);
+ /* return false = thread was already in backtrack */
+ bool set_backtrack(thread_id_t id);
+ thread_id_t get_next_backtrack();
+ bool is_enabled(Thread *t);
+ ModelAction * get_action() { return action; }
+
+ void print();
+
+ static int get_total_nodes() { return total_nodes; }
+private:
+ void explore(thread_id_t tid);
+
+ static int total_nodes;
+ ModelAction *action;
+ int num_threads;
+ std::vector<bool> explored_children;
+ std::vector<bool> backtrack;
+};
+
+typedef std::list<class Node *> node_list_t;
+
+class NodeStack {
+public:
+ NodeStack();
+ ~NodeStack();
+ ModelAction * explore_action(ModelAction *act);
+ Node * get_head();
+ Node * get_next();
+ void reset_execution();
+
+ void print();
+private:
+ node_list_t node_list;
+ node_list_t::iterator iter;
+};
+
+#endif /* __NODESTACK_H__ */
-#include <stdlib.h>
-
#include "libthreads.h"
-#include "schedule.h"
#include "common.h"
#include "threads.h"
#include "libthreads.h"
#include "libatomic.h"
+#include "librace.h"
static void a(atomic_int *obj)
{
int i;
int ret;
- for (i = 0; i < 7; i++) {
+ store_32(&i, 10);
+ printf("load 32 yields: %d\n", load_32(&i));
+
+ for (i = 0; i < 2; i++) {
printf("Thread %d, loop %d\n", thrd_current(), i);
switch (i ) {
case 1:
printf("Read value: %d\n", ret);
break;
case 0:
- atomic_store(obj, i);
- printf("Write value: %d\n", i);
+ atomic_store(obj, i + 1);
+ printf("Write value: %d\n", i + 1);
break;
}
}
projects / c11tester.git / commitdiff