From: Brian Norris Date: Thu, 13 Sep 2012 16:21:08 +0000 (-0700) Subject: Merge remote-tracking branch 'origin/makefile' X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=76205f5d9b62f73ea01f7e55765a043a8333a455;hp=59b62a130c9615c9ccd23c4354c7bc827d5eda3b;p=c11tester.git Merge remote-tracking branch 'origin/makefile' --- diff --git a/Makefile b/Makefile index 2acdbc7d..91acd7e8 100644 --- a/Makefile +++ b/Makefile @@ -6,10 +6,17 @@ OBJECTS = libthreads.o schedule.o model.o threads.o librace.o action.o \ snapshot.o malloc.o mymemory.o CPPFLAGS += -Iinclude -I. -LDFLAGS=-ldl -lrt -SHARED=-shared +LDFLAGS = -ldl -lrt +SHARED = -shared -TESTS=test +# Mac OSX options +ifeq ($(UNAME), Darwin) +CPPFLAGS += -D_XOPEN_SOURCE -DMAC +LDFLAGS = -ldl +SHARED = -Wl,-undefined,dynamic_lookup -dynamiclib +endif + +TESTS_DIR = test program_H_SRCS := $(wildcard *.h) $(wildcard include/*.h) program_C_SRCS := $(wildcard *.c) $(wildcard *.cc) @@ -18,18 +25,13 @@ DEPS = make.deps all: $(LIB_SO) $(DEPS) tests $(DEPS): $(program_C_SRCS) $(program_H_SRCS) - $(CXX) $(CPPFLAGS) -MM $(program_C_SRCS) > $(DEPS) + $(CXX) -MM $(program_C_SRCS) $(CPPFLAGS) > $(DEPS) include $(DEPS) debug: CPPFLAGS += -DCONFIG_DEBUG debug: all -mac: CPPFLAGS += -D_XOPEN_SOURCE -DMAC -mac: LDFLAGS=-ldl -mac: SHARED=-Wl,-undefined,dynamic_lookup -dynamiclib -mac: all - docs: *.c *.cc *.h doxygen @@ -44,7 +46,7 @@ malloc.o: malloc.c clean: rm -f *.o *.so - $(MAKE) -C $(TESTS) clean + $(MAKE) -C $(TESTS_DIR) clean mrclean: clean rm -rf docs @@ -53,4 +55,4 @@ tags:: ctags -R tests:: $(LIB_SO) - $(MAKE) -C $(TESTS) + $(MAKE) -C $(TESTS_DIR) diff --git a/common.mk b/common.mk index 378a6597..e9e40600 100644 --- a/common.mk +++ b/common.mk @@ -1,9 +1,11 @@ # A few common Makefile items -CC=gcc -CXX=g++ +CC = gcc +CXX = g++ -LIB_NAME=model -LIB_SO=lib$(LIB_NAME).so +UNAME = $(shell uname) -CPPFLAGS=-Wall -g -O0 +LIB_NAME = model +LIB_SO = lib$(LIB_NAME).so + +CPPFLAGS += -Wall -g -O0 diff --git a/cyclegraph.cc b/cyclegraph.cc index 0a3d8858..26235d65 100644 --- a/cyclegraph.cc +++ b/cyclegraph.cc @@ -89,10 +89,10 @@ void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw) { } /* Transfer all outgoing edges from the from node to the rmw node */ - /* This process should not add a cycle because either: + /* This process should not add a cycle because either: * (1) The rmw should not have any incoming edges yet if it is the * new node or - * (2) the fromnode is the new node and therefore it should not + * (2) the fromnode is the new node and therefore it should not * have any outgoing edges. */ std::vector * edges=fromnode->getEdges(); diff --git a/model.cc b/model.cc index 50317d07..fb2423f3 100644 --- a/model.cc +++ b/model.cc @@ -259,7 +259,6 @@ ModelAction * ModelChecker::get_next_backtrack() return next; } - /** * Processes a read or rmw model action. * @param curr is the read model action to process. @@ -267,7 +266,6 @@ ModelAction * ModelChecker::get_next_backtrack() * @param second_part_of_rmw is boolean that is true is this is the second action of a rmw. * @return True if processing this read updates the mo_graph. */ - bool ModelChecker::process_read(ModelAction *curr, Thread * th, bool second_part_of_rmw) { uint64_t value; bool updated=false; @@ -428,7 +426,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) add_action_to_lists(curr); check_curr_backtracking(curr); - + set_backtracking(curr); return get_next_thread(curr); @@ -437,7 +435,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) void ModelChecker::check_curr_backtracking(ModelAction * curr) { Node *currnode = curr->get_node(); Node *parnode = currnode->get_parent(); - + if ((!parnode->backtrack_empty() || !currnode->read_from_empty() || !currnode->future_value_empty() || @@ -448,7 +446,6 @@ void ModelChecker::check_curr_backtracking(ModelAction * curr) { } } - bool ModelChecker::promises_expired() { for (unsigned int promise_index = 0; promise_index < promises->size(); promise_index++) { Promise *promise = (*promises)[promise_index]; @@ -762,7 +759,6 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con return true; } - /** * Finds the head(s) of the release sequence(s) containing a given ModelAction. * The ModelAction under consideration is expected to be taking part in @@ -1056,8 +1052,6 @@ bool ModelChecker::resolve_promises(ModelAction *write) return resolved; } - - /** * Compute the set of promises that could potentially be satisfied by this * action. Note that the set computation actually appears in the Node, not in diff --git a/model.h b/model.h index 9afe642a..cf03f091 100644 --- a/model.h +++ b/model.h @@ -94,7 +94,7 @@ public: private: /** The scheduler to use: tracks the running/ready Threads */ Scheduler *scheduler; - + bool thin_air_constraint_may_allow(const ModelAction * writer, const ModelAction *reader); bool has_asserted() {return asserted;} void reset_asserted() {asserted=false;} @@ -123,7 +123,6 @@ private: bool resolve_promises(ModelAction *curr); void compute_promises(ModelAction *curr); - void check_curr_backtracking(ModelAction * curr); void add_action_to_lists(ModelAction *act); ModelAction * get_last_action(thread_id_t tid); diff --git a/test/linuxrwlocks.c b/test/linuxrwlocks.c index dcf323ca..3862ed49 100644 --- a/test/linuxrwlocks.c +++ b/test/linuxrwlocks.c @@ -4,14 +4,12 @@ #include "librace.h" #include "stdatomic.h" - #define RW_LOCK_BIAS 0x00100000 #define WRITE_LOCK_CMP RW_LOCK_BIAS /** Example implementation of linux rw lock along with 2 thread test * driver... */ - typedef union { atomic_int lock; } rwlock_t; @@ -55,7 +53,7 @@ static inline int read_trylock(rwlock_t *rw) int priorvalue=atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire); if (priorvalue>0) return 1; - + atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed); return 0; } @@ -65,7 +63,7 @@ static inline int write_trylock(rwlock_t *rw) int priorvalue=atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire); if (priorvalue==RW_LOCK_BIAS) return 1; - + atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed); return 0; } @@ -106,7 +104,7 @@ void user_main() thrd_create(&t1, (thrd_start_t)&a, NULL); thrd_create(&t2, (thrd_start_t)&a, NULL); - + thrd_join(t1); thrd_join(t2); }