From: Brian Demsky <bdemsky@uci.edu>
Date: Fri, 18 May 2012 23:32:38 +0000 (-0700)
Subject: merging stuff...made need to clean up some stuff...but need to push it somewhere... 
X-Git-Tag: pldi2013~435
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=810306cb85accaaace9a50f174264f105991230b;p=model-checker.git

merging stuff...made need to clean up some stuff...but need to push it somewhere else for now
Merge branch 'subramanian'

Conflicts:
	.gitignore
	Makefile
	action.h
	userprog.c
---

810306cb85accaaace9a50f174264f105991230b
diff --cc .gitignore
index ab5a84a,6223e7e..f9a2676
--- a/.gitignore
+++ b/.gitignore
@@@ -3,6 -3,7 +3,10 @@@
  .*.swp
  *.so
  *~
++<<<<<<< HEAD
++=======
+ *.*~
++>>>>>>> subramanian
  
  # files in this directory
  /model
diff --cc Makefile
index e61de2a,8344eff..b67d994
--- a/Makefile
+++ b/Makefile
@@@ -8,17 -10,22 +10,22 @@@ LIB_MEM_SO=lib$(LIB_MEM).s
  USER_O=userprog.o
  USER_H=libthreads.h libatomic.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
- 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
- MODEL_H=libthreads.h schedule.h common.h libatomic.h model.h threads.h tree.h librace.h action.h nodestack.h clockvector.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
+ SHMEM_H=snapshot.h snapshotimp.h mymemory.h
  
  CPPFLAGS=-Wall -g
- LDFLAGS=-ldl
+ LDFLAGS=-ldl -lrt
  
+ MEMCPPFLAGS=-fPIC -g -c -Wall
  all: $(BIN)
  
- $(BIN): $(USER_O) $(LIB_SO)
- 	$(CXX) -o $(BIN) $(USER_O) -L. -l$(LIB_NAME) $(CPPFLAGS)
+ $(BIN): $(USER_O) $(LIB_SO) $(LIB_MEM_SO)
+ 	$(CXX) -o $(BIN) $(USER_O) -L. -l$(LIB_NAME) -l$(LIB_MEM) $(CPPFLAGS)
  
  # note: implicit rule for generating $(USER_O) (i.e., userprog.c -> userprog.o)
  
diff --cc action.h
index cfe1f34,c069cab..2f856e9
--- a/action.h
+++ b/action.h
@@@ -43,13 -39,7 +42,14 @@@ public
  	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;
  	memory_order order;
diff --cc userprog.c
index 402cb0d,5598bfb..0948f0b
--- a/userprog.c
+++ b/userprog.c
@@@ -9,12 -8,9 +9,12 @@@ 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 % 4) {
+ 		switch (i  ) {
  		case 1:
  			ret = atomic_load(obj);
  			printf("Read value: %d\n", ret);