From: Brian Norris Date: Mon, 21 May 2012 18:07:44 +0000 (-0700) Subject: Merge commit: branch 'work' X-Git-Tag: pldi2013~409 X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=10de861d3a9908e75b6f94283cc67b3f1b4d93ab;hp=-c;p=model-checker.git Merge commit: branch 'work' tree.{cc,h} were replaced with NodeStack. (Will need to update them) Other trivial conflicts in Makefile and model.h Conflicts: Makefile model.h tree.cc tree.h --- 10de861d3a9908e75b6f94283cc67b3f1b4d93ab diff --combined Makefile index f91f4fd,22a1c64..ef89c5a --- a/Makefile +++ b/Makefile @@@ -8,35 -8,22 +8,35 @@@ LIB_SO=lib$(LIB_NAME).s 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 nodestack.cc clockvector.cc main.cc snapshot-interface.cc - MODEL_O=libthreads.o schedule.o libatomic.o model.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 -MODEL_CC=libthreads.cc schedule.cc libatomic.cc model.cc malloc.c threads.cc librace.cc action.cc nodestack.cc clockvector.cc main.cc -MODEL_O=libthreads.o schedule.o libatomic.o model.o malloc.o threads.o librace.o action.o nodestack.o clockvector.o main.o -MODEL_H=libthreads.h schedule.h common.h libatomic.h model.h threads.h librace.h action.h nodestack.h clockvector.h ++MODEL_CC=libthreads.cc schedule.cc libatomic.cc model.cc threads.cc librace.cc action.cc nodestack.cc clockvector.cc main.cc snapshot-interface.cc ++MODEL_O=libthreads.o schedule.o libatomic.o model.o threads.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 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 +SHMEM_H=snapshot.h snapshotimp.h mymemory.h CPPFLAGS=-Wall -g -LDFLAGS=-ldl +LDFLAGS=-ldl -lrt all: $(BIN) $(BIN): $(USER_O) $(LIB_SO) - $(CXX) -o $(BIN) $(USER_O) -L. -l$(LIB_NAME) $(CPPFLAGS) + $(CXX) -o $(BIN) $(USER_O) -L. -l$(LIB_NAME) # note: implicit rule for generating $(USER_O) (i.e., userprog.c -> userprog.o) -$(LIB_SO): $(MODEL_O) $(MODEL_H) - $(CXX) -shared -Wl,-soname,$(LIB_SO) -o $(LIB_SO) $(MODEL_O) $(LDFLAGS) $(CPPFLAGS) +$(LIB_SO): $(MODEL_O) $(MODEL_H) $(SHMEM_O) $(SHMEM_H) + $(CXX) -shared -o $(LIB_SO) $(MODEL_O) $(SHMEM_O) $(LDFLAGS) + +malloc.o: malloc.c + $(CC) -fPIC -c malloc.c -DMSPACES -DONLY_MSPACES $(CPPFLAGS) + +mymemory.o: mymemory.h snapshotimp.h mymemory.cc + $(CXX) -fPIC -c mymemory.cc $(CPPFLAGS) + +snapshot.o: mymemory.h snapshot.h snapshotimp.h snapshot.cc + $(CXX) -fPIC -c snapshot.cc $(CPPFLAGS) $(MODEL_O): $(MODEL_CC) $(MODEL_H) $(CXX) -fPIC -c $(MODEL_CC) $(CPPFLAGS) diff --combined action.h index 2f856e9,b30b650..4cc6847 --- a/action.h +++ b/action.h @@@ -2,9 -2,10 +2,9 @@@ #define __ACTION_H__ #include - #include "threads.h" #include "libatomic.h" - +#include "mymemory.h" #define VALUE_NONE -1 typedef enum action_type { @@@ -16,7 -17,6 +16,6 @@@ } action_type_t; /* Forward declaration */ - class TreeNode; class Node; class ModelAction { @@@ -30,8 -30,6 +29,6 @@@ public void * get_location() { return location; } int get_seq_number() const { return seq_number; } - TreeNode * get_treenode() { return treenode; } - void set_node(TreeNode *n) { treenode = n; } Node * get_node() { return node; } void set_node(Node *n) { node = n; } @@@ -49,18 -47,16 +46,17 @@@ inline bool operator >(const ModelAction& act) const { return get_seq_number() > act.get_seq_number(); } + MEMALLOC private: action_type type; memory_order order; void *location; thread_id_t tid; int value; - TreeNode *treenode; Node *node; int seq_number; }; -typedef std::list action_list_t; +typedef std::list > action_list_t; #endif /* __ACTION_H__ */ diff --combined model.cc index e068a08,90dcdc7..8da05aa --- a/model.cc +++ b/model.cc @@@ -2,44 -2,14 +2,16 @@@ #include "model.h" #include "action.h" - #include "tree.h" + #include "nodestack.h" #include "schedule.h" +#include "snapshot-interface.h" +#undef DEBUG #include "common.h" #define INITIAL_THREAD_ID 0 - class Backtrack { - public: - Backtrack(ModelAction *d, action_list_t *t) { - diverge = d; - actionTrace = t; - iter = actionTrace->begin(); - } - ModelAction * get_diverge() { return diverge; } - action_list_t * get_trace() { return actionTrace; } - void advance_state() { iter++; } - ModelAction * get_state() { - return iter == actionTrace->end() ? NULL : *iter; - } - private: - ModelAction *diverge; - action_list_t *actionTrace; - /* points to position in actionTrace as we replay */ - action_list_t::iterator iter; - }; - ModelChecker *model; - void free_action_list(action_list_t *list) - { - action_list_t::iterator it; - for (it = list->begin(); it != list->end(); it++) - delete (*it); - delete list; - } - ModelChecker::ModelChecker() : /* Initialize default scheduler */ @@@ -50,40 -20,42 +22,42 @@@ num_executions(0), current_action(NULL), - exploring(NULL), + diverge(NULL), nextThread(THREAD_ID_T_NONE), action_trace(new action_list_t()), - rootNode(new TreeNode()), - currentNode(rootNode) + node_stack(new NodeStack()), + next_backtrack(NULL) { } ModelChecker::~ModelChecker() { - std::map::iterator it; + std::map, MyAlloc< std::pair< int, class Thread * > > >::iterator it; for (it = thread_map.begin(); it != thread_map.end(); it++) delete (*it).second; thread_map.clear(); - free_action_list(action_trace); + delete action_trace; + delete node_stack; delete scheduler; - delete rootNode; } void ModelChecker::reset_to_initial_state() { DEBUG("+++ Resetting to initial state +++\n"); - std::map::iterator it; + std::map, MyAlloc< std::pair< int, class Thread * > > >::iterator it; for (it = thread_map.begin(); it != thread_map.end(); it++) delete (*it).second; thread_map.clear(); + delete action_trace; action_trace = new action_list_t(); - currentNode = rootNode; + node_stack->reset_execution(); current_action = NULL; next_thread_id = INITIAL_THREAD_ID; used_sequence_numbers = 0; nextThread = 0; + next_backtrack = NULL; /* scheduler reset ? */ } @@@ -122,24 -94,19 +96,19 @@@ thread_id_t ModelChecker::get_next_repl thread_id_t tid; /* Have we completed exploring the preselected path? */ - if (exploring == NULL) + if (diverge == NULL) return THREAD_ID_T_NONE; /* Else, we are trying to replay an execution */ - exploring->advance_state(); - - ASSERT(exploring->get_state() != NULL); + next = node_stack->get_next()->get_action(); - next = exploring->get_state(); + if (next == diverge) { + Node *node = next->get_node(); - if (next == exploring->get_diverge()) { - TreeNode *node = next->get_treenode(); - - /* Reached divergence point; discard our current 'exploring' */ - DEBUG("*** Discard 'Backtrack' object ***\n"); - tid = node->getNextBacktrack(); - delete exploring; - exploring = NULL; + /* Reached divergence point */ + DEBUG("*** Divergence point ***\n"); + tid = node->get_next_backtrack(); + diverge = NULL; } else { tid = next->get_tid(); } @@@ -153,13 -120,12 +122,12 @@@ bool ModelChecker::next_execution( num_executions++; print_summary(); - if ((exploring = model->get_next_backtrack()) == NULL) + if ((diverge = model->get_next_backtrack()) == NULL) return false; if (DBG_ENABLED()) { printf("Next execution will diverge at:\n"); - exploring->get_diverge()->print(); - print_list(exploring->get_trace()); + diverge->print(); } model->reset_to_initial_state(); @@@ -193,48 -159,47 +161,47 @@@ ModelAction * ModelChecker::get_last_co void ModelChecker::set_backtracking(ModelAction *act) { ModelAction *prev; - TreeNode *node; + Node *node; Thread *t = get_thread(act->get_tid()); prev = get_last_conflict(act); if (prev == NULL) return; - node = prev->get_treenode(); + node = prev->get_node(); - while (t && !node->is_enabled(t)) + while (!node->is_enabled(t)) t = t->get_parent(); /* Check if this has been explored already */ - if (node->hasBeenExplored(t->get_id())) + if (node->has_been_explored(t->get_id())) return; + + if (!next_backtrack || *prev > *next_backtrack) + next_backtrack = prev; + /* If this is a new backtracking point, mark the tree */ - if (node->setBacktrack(t->get_id()) != 0) + if (!node->set_backtrack(t->get_id())) return; - DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n", prev->get_tid(), t->get_id()); if (DBG_ENABLED()) { prev->print(); act->print(); } - - Backtrack *back = new Backtrack(prev, action_trace); - backtrack_list.push_back(back); } - Backtrack * ModelChecker::get_next_backtrack() + ModelAction * ModelChecker::get_next_backtrack() { - Backtrack *next; - if (backtrack_list.empty()) - return NULL; - next = backtrack_list.back(); - backtrack_list.pop_back(); + ModelAction *next = next_backtrack; + next_backtrack = NULL; return next; } void ModelChecker::check_current_action(void) { + Node *currnode; + ModelAction *curr = this->current_action; current_action = NULL; if (!curr) { @@@ -242,10 -207,16 +209,16 @@@ return; } + curr = node_stack->explore_action(curr); nextThread = get_next_replay_thread(); - curr->set_node(currentNode); + + currnode = curr->get_node(); + + if (!currnode->backtrack_empty()) + if (!next_backtrack || *curr > *next_backtrack) + next_backtrack = curr; + set_backtracking(curr); - currentNode = currentNode->explore_child(curr); this->action_trace->push_back(curr); } @@@ -253,13 -224,12 +226,12 @@@ void ModelChecker::print_summary(void { printf("\n"); printf("Number of executions: %d\n", num_executions); - printf("Total nodes created: %d\n", TreeNode::getTotalNodes()); + printf("Total nodes created: %d\n", Node::get_total_nodes()); scheduler->print(); print_list(action_trace); printf("\n"); - } void ModelChecker::print_list(action_list_t *list) diff --combined model.h index 1dc6a15,e8a8c5e..4718c50 --- a/model.h +++ b/model.h @@@ -3,21 -3,17 +3,20 @@@ #include #include +#include #include #include #include "schedule.h" +#include "mymemory.h" +#include #include "libthreads.h" #include "libatomic.h" #include "threads.h" #include "action.h" /* Forward declaration */ - class TreeNode; - class Backtrack; + class NodeStack; class ModelChecker { public: @@@ -43,7 -39,6 +42,7 @@@ int switch_to_master(ModelAction *act); bool next_execution(); + MEMALLOC private: int next_thread_id; int used_sequence_numbers; @@@ -52,20 -47,20 +51,20 @@@ ModelAction * get_last_conflict(ModelAction *act); void set_backtracking(ModelAction *act); thread_id_t get_next_replay_thread(); - Backtrack * get_next_backtrack(); + ModelAction * get_next_backtrack(); void reset_to_initial_state(); void print_list(action_list_t *list); - class ModelAction *current_action; - Backtrack *exploring; + ModelAction *current_action; + ModelAction *diverge; thread_id_t nextThread; ucontext_t *system_context; action_list_t *action_trace; - std::map thread_map; + std::map, MyAlloc< std::pair< const int, class Thread * > > > thread_map; - class TreeNode *rootNode, *currentNode; - std::list > backtrack_list; + class NodeStack *node_stack; + ModelAction *next_backtrack; }; extern ModelChecker *model;