Merge branch 'branch-weiyu' of /home/git/random-fuzzer into new_fuzzer

diff --git a/execution.cc b/execution.cc
index 290a2624666f905dc8bac06c5178aafc2fe5dda0..de2cace8cecbe61116e74c13837d3dcaedac8c8c 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -277,7 +277,6 @@ ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
        return act;
 }
 
-
 /**
  * Processes a read model action.
  * @param curr is the read model action to process.
@@ -1632,7 +1631,7 @@ Thread * ModelExecution::take_step(ModelAction *curr)
        ASSERT(curr);
 
        /* Process this action in ModelHistory for records*/
-       model->get_history()->process_action( curr, curr_thrd->get_id() );
+       model->get_history()->process_action( curr, curr->get_tid() );
 
        if (curr_thrd->is_blocked() || curr_thrd->is_complete())
                scheduler->remove_thread(curr_thrd);

diff --git a/execution.h b/execution.h
index f1d3dc56f0085408fc3ffb2c49f55dad2d26e38c..e958148fc92651c4abe2ce768dc37f9ba61fe912 100644 (file)
--- a/execution.h
+++ b/execution.h
@@ -89,7 +89,7 @@ public:
        HashTable<pthread_mutex_t *, cdsc::snapmutex *, uintptr_t, 4> * getMutexMap() {return &mutex_map;}
        ModelAction * check_current_action(ModelAction *curr);
 
-       SnapVector<func_id_list_t *> * get_thrd_func_list() { return &thrd_func_list; }
+       SnapVector<func_id_list_t> * get_thrd_func_list() { return &thrd_func_list; }
        SnapVector< SnapList<func_inst_list_t *> *> * get_thrd_func_inst_lists() { return &thrd_func_inst_lists; }
 
        SNAPSHOTALLOC
@@ -203,7 +203,7 @@ private:
         *
         * This data structure is handled by ModelHistory
         */
-       SnapVector< func_id_list_t * > thrd_func_list;
+       SnapVector<func_id_list_t> thrd_func_list;
 
        /* Keeps track of atomic actions that thread i has performed in some
         * function. Index of SnapVector is thread id. SnapList simulates

diff --git a/funcinst.cc b/funcinst.cc
index 7e0446ffec149e9c778345c6ca2790ca48916cec..92890d58ce07b296daa0b7bb1c0c17e717d4bb78 100644 (file)
--- a/funcinst.cc
+++ b/funcinst.cc
@@ -58,5 +58,11 @@ FuncInst * FuncInst::search_in_collision(ModelAction *act)
 
 bool FuncInst::is_read() const
 {
-       return type == ATOMIC_READ || type == ATOMIC_RMWR || type == ATOMIC_RMWRCAS;
+       return type == ATOMIC_READ || type == ATOMIC_RMWR || type == ATOMIC_RMWRCAS; /* type == ATOMIC_RMW ? */
 }
+
+bool FuncInst::is_write() const
+{
+        return type == ATOMIC_WRITE || type == ATOMIC_RMW || type == ATOMIC_INIT || type == ATOMIC_UNINIT || type == NONATOMIC_WRITE;
+}
+

diff --git a/funcinst.h b/funcinst.h
index 85b9c20ecce2d9b07d8b85168fc3f1bbe39701b4..efdb43b4dbe88c9250cb62ecaca8848bbfce1f95 100644 (file)
--- a/funcinst.h
+++ b/funcinst.h
@@ -1,3 +1,6 @@
+#ifndef __FUNCINST_H__
+#define __FUNCINST_H__
+
 #include "action.h"
 #include "hashtable.h"
 
@@ -26,6 +29,7 @@ public:
        func_inst_list_mt * get_succs() { return &successors; }
 
        bool is_read() const;
+       bool is_write() const;
 
        MEMALLOC
 private:
@@ -43,3 +47,6 @@ private:
        func_inst_list_mt predecessors;
        func_inst_list_mt successors;
 };
+
+#endif /* __FUNCINST_H__ */
+

diff --git a/funcnode.cc b/funcnode.cc
index 8e76ebc674bf8e6d7339b45768b6a8b87c0a961d..208bc3beb2666520d20ac30f873234b1e9775e00 100644 (file)
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -1,4 +1,5 @@
 #include "funcnode.h"
+#include "predicate.h"
 
 FuncNode::FuncNode() :
        func_inst_map(),
@@ -112,15 +113,15 @@ void FuncNode::store_read(ModelAction * act, uint32_t tid)
        void * location = act->get_location();
        uint64_t read_from_val = act->get_reads_from_value();
 
-       if (thrd_read_map.size() <= tid)
+       /* resize and initialize */
+       uint32_t old_size = thrd_read_map.size();
+       if (old_size <= tid) {
                thrd_read_map.resize(tid + 1);
-
-       read_map_t * read_map = thrd_read_map[tid];
-       if (read_map == NULL) {
-               read_map = new read_map_t();
-               thrd_read_map[tid] = read_map;
+               for (uint32_t i = old_size; i < tid + 1; i++)
+                       thrd_read_map[i] = new read_map_t();
        }
 
+       read_map_t * read_map = thrd_read_map[tid];
        read_map->put(location, read_from_val);
 
        /* Store the memory locations where atomic reads happen */
@@ -137,13 +138,12 @@ void FuncNode::store_read(ModelAction * act, uint32_t tid)
                read_locations.push_back(location);
 }
 
-uint64_t FuncNode::query_last_read(ModelAction * act, uint32_t tid)
+uint64_t FuncNode::query_last_read(void * location, uint32_t tid)
 {
        if (thrd_read_map.size() <= tid)
                return 0xdeadbeef;
 
        read_map_t * read_map = thrd_read_map[tid];
-       void * location = act->get_location();
 
        /* last read value not found */
        if ( !read_map->contains(location) )
@@ -165,6 +165,11 @@ void FuncNode::clear_read_map(uint32_t tid)
        thrd_read_map[tid]->reset();
 }
 
+void FuncNode::generate_predicate(FuncInst *func_inst)
+{
+       
+}
+
 /* @param tid thread id
  * Print the values read by the last read actions for each memory location
  */

diff --git a/funcnode.h b/funcnode.h
index be6f406a4e3453b029247e8e23550deb9186cd99..08e07fb188ffcbd009f2ee6b160f0b674fd97935 100644 (file)
--- a/funcnode.h
+++ b/funcnode.h
@@ -1,9 +1,10 @@
+#ifndef __FUNCNODE_H__
+#define __FUNCNODE_H__
+
 #include "action.h"
 #include "funcinst.h"
 #include "hashtable.h"
 
-class ModelAction;
-
 typedef ModelList<FuncInst *> func_inst_list_mt;
 typedef HashTable<void *, uint64_t, uintptr_t, 4, model_malloc, model_calloc, model_free> read_map_t;
 
@@ -26,9 +27,12 @@ public:
        void link_insts(func_inst_list_t * inst_list);
 
        void store_read(ModelAction * act, uint32_t tid);
-       uint64_t query_last_read(ModelAction * act, uint32_t tid);
+       uint64_t query_last_read(void * location, uint32_t tid);
        void clear_read_map(uint32_t tid);
 
+       /* TODO: generate EQUALITY or NULLITY predicate based on write_history in history.cc */
+       void generate_predicate(FuncInst * func_inst);
+
        void print_last_read(uint32_t tid);
 
        MEMALLOC
@@ -51,3 +55,5 @@ private:
        ModelVector<read_map_t *> thrd_read_map;
        ModelList<void *> read_locations;
 };
+
+#endif /* __FUNCNODE_H__ */

diff --git a/history.cc b/history.cc
index ca176b1900759e71ec8b8c25aa2c979749c88f1a..3c000e7de06c20f2054610a96f7138db78d92745 100644 (file)
--- a/history.cc
+++ b/history.cc
@@ -13,14 +13,15 @@ ModelHistory::ModelHistory() :
        func_counter(1),        /* function id starts with 1 */
        func_map(),
        func_map_rev(),
-       func_nodes()
+       func_nodes(),
+       write_history()
 {}
 
 void ModelHistory::enter_function(const uint32_t func_id, thread_id_t tid)
 {
        //model_print("thread %d entering func %d\n", tid, func_id);
        uint32_t id = id_to_int(tid);
-       SnapVector<func_id_list_t *> * thrd_func_list = model->get_execution()->get_thrd_func_list();
+       SnapVector<func_id_list_t> * thrd_func_list = model->get_execution()->get_thrd_func_list();
        SnapVector< SnapList<func_inst_list_t *> *> *
                thrd_func_inst_lists = model->get_execution()->get_thrd_func_inst_lists();
 
@@ -29,20 +30,14 @@ void ModelHistory::enter_function(const uint32_t func_id, thread_id_t tid)
                thrd_func_inst_lists->resize( id + 1 );
        }
 
-       func_id_list_t * func_list = thrd_func_list->at(id);
        SnapList<func_inst_list_t *> * func_inst_lists = thrd_func_inst_lists->at(id);
 
-       if (func_list == NULL) {
-               func_list = new func_id_list_t();
-               thrd_func_list->at(id) = func_list;
-       }
-
        if (func_inst_lists == NULL) {
                func_inst_lists = new SnapList< func_inst_list_t *>();
                thrd_func_inst_lists->at(id) = func_inst_lists;
        }
 
-       func_list->push_back(func_id);
+       (*thrd_func_list)[id].push_back(func_id);
        func_inst_lists->push_back( new func_inst_list_t() );
 
        if ( func_nodes.size() <= func_id )
@@ -53,14 +48,12 @@ void ModelHistory::enter_function(const uint32_t func_id, thread_id_t tid)
 void ModelHistory::exit_function(const uint32_t func_id, thread_id_t tid)
 {
        uint32_t id = id_to_int(tid);
-       SnapVector<func_id_list_t *> * thrd_func_list = model->get_execution()->get_thrd_func_list();
+       SnapVector<func_id_list_t> * thrd_func_list = model->get_execution()->get_thrd_func_list();
        SnapVector< SnapList<func_inst_list_t *> *> *
                thrd_func_inst_lists = model->get_execution()->get_thrd_func_inst_lists();
 
-       func_id_list_t * func_list = thrd_func_list->at(id);
        SnapList<func_inst_list_t *> * func_inst_lists = thrd_func_inst_lists->at(id);
-
-       uint32_t last_func_id = func_list->back();
+       uint32_t last_func_id = (*thrd_func_list)[id].back();
 
        if (last_func_id == func_id) {
                FuncNode * func_node = func_nodes[func_id];
@@ -69,7 +62,7 @@ void ModelHistory::exit_function(const uint32_t func_id, thread_id_t tid)
                func_inst_list_t * curr_inst_list = func_inst_lists->back();
                func_node->link_insts(curr_inst_list);
 
-               func_list->pop_back();
+               (*thrd_func_list)[id].pop_back();
                func_inst_lists->pop_back();
        } else {
                model_print("trying to exit with a wrong function id\n");
@@ -98,22 +91,18 @@ void ModelHistory::process_action(ModelAction *act, thread_id_t tid)
 {
        /* return if thread i has not entered any function or has exited
           from all functions */
-       SnapVector<func_id_list_t *> * thrd_func_list = model->get_execution()->get_thrd_func_list();
+       SnapVector<func_id_list_t> * thrd_func_list = model->get_execution()->get_thrd_func_list();
        SnapVector< SnapList<func_inst_list_t *> *> *
                thrd_func_inst_lists = model->get_execution()->get_thrd_func_inst_lists();
 
        uint32_t id = id_to_int(tid);
        if ( thrd_func_list->size() <= id )
                return;
-       else if (thrd_func_list->at(id) == NULL)
-               return;
 
        /* get the function id that thread i is currently in */
-       func_id_list_t * func_list = thrd_func_list->at(id);
+       uint32_t func_id = (*thrd_func_list)[id].back();
        SnapList<func_inst_list_t *> * func_inst_lists = thrd_func_inst_lists->at(id);
 
-       uint32_t func_id = func_list->back();
-
        if ( func_nodes.size() <= func_id )
                resize_func_nodes( func_id + 1 );
 
@@ -129,6 +118,9 @@ void ModelHistory::process_action(ModelAction *act, thread_id_t tid)
        //      if (inst->is_read())
        //      func_node->store_read(act, tid);
 
+       if (inst->is_write())
+               add_to_write_history(act->get_location(), act->get_write_value());
+
        /* add to curr_inst_list */
        func_inst_list_t * curr_inst_list = func_inst_lists->back();
        ASSERT(curr_inst_list != NULL);
@@ -144,6 +136,32 @@ FuncNode * ModelHistory::get_func_node(uint32_t func_id)
        return func_nodes[func_id];
 }
 
+uint64_t ModelHistory::query_last_read(void * location, thread_id_t tid)
+{
+       SnapVector<func_id_list_t> * thrd_func_list = model->get_execution()->get_thrd_func_list();
+       uint32_t id = id_to_int(tid);
+
+       ASSERT( thrd_func_list->size() > id );
+       uint32_t func_id = (*thrd_func_list)[id].back();
+       FuncNode * func_node = func_nodes[func_id];
+
+       uint64_t last_read_val = 0xdeadbeef;
+       if (func_node != NULL) {
+               last_read_val = func_node->query_last_read(location, tid);
+       }
+
+       return last_read_val;
+}
+
+void ModelHistory::add_to_write_history(void * location, uint64_t write_val)
+{
+       if ( !write_history.contains(location) )
+               write_history.put(location, new write_set_t() );
+
+       write_set_t * write_set = write_history.get(location);
+       write_set->add(write_val);
+}
+
 void ModelHistory::print()
 {
        /* function id starts with 1 */

diff --git a/history.h b/history.h
index 0984e03ae129e4efc58fc517b8281bdf58ad9fff..5709ab6cc9baa405dc2f5febc00b3910b639c4bf 100644 (file)
--- a/history.h
+++ b/history.h
@@ -1,8 +1,14 @@
+#ifndef __HISTORY_H__
+#define __HISTORY_H__
+
 #include "stl-model.h"
 #include "common.h"
 #include "hashtable.h"
+#include "hashset.h"
 #include "threads-model.h"
 
+typedef HashSet<uint64_t, uint64_t, 4, model_malloc, model_calloc, model_free> write_set_t;
+
 class ModelHistory {
 public:
        ModelHistory();
@@ -22,6 +28,9 @@ public:
 
        ModelVector<FuncNode *> * getFuncNodes() { return &func_nodes; }
        FuncNode * get_func_node(uint32_t func_id);
+       uint64_t query_last_read(void * location, thread_id_t tid);
+
+       void add_to_write_history(void * location, uint64_t write_val);
 
        void print();
 
@@ -35,4 +44,7 @@ private:
        ModelVector<const char *> func_map_rev;
 
        ModelVector<FuncNode *> func_nodes;
+       HashTable<void *, write_set_t *, uintptr_t, 4, model_malloc, model_calloc, model_free> write_history;
 };
+
+#endif /* __HISTORY_H__ */

diff --git a/predicate.cc b/predicate.cc
new file mode 100644 (file)
index 0000000..9f4246e
--- /dev/null
+++ b/predicate.cc
@@ -0,0 +1,26 @@
+#include "predicate.h"
+
+inline bool operator==(const predicate_expr& expr_A, const predicate_expr& expr_B)
+{
+       if (expr_A.token != expr_B.token)
+               return false;
+
+       if (expr_A.token == EQUALITY && expr_A.location != expr_B.location)
+               return false;
+
+       if (expr_A.value != expr_B.value)
+               return false;
+
+       return true;
+}
+
+void Predicate::add_predicate(predicate_expr predicate)
+{
+       ModelList<predicate_expr>::iterator it;
+       for (it = predicates.begin(); it != predicates.end(); it++) {
+               if (predicate == *it)
+                       return;
+       }
+
+       predicates.push_back(predicate);
+}

diff --git a/predicate.h b/predicate.h
new file mode 100644 (file)
index 0000000..e2412d1
--- /dev/null
+++ b/predicate.h
@@ -0,0 +1,31 @@
+#include "funcinst.h"
+
+typedef enum predicate_token {
+       EQUALITY, NULLITY
+} token_t;
+
+/* If token is EQUALITY, then the predicate asserts whether
+ * this load should read the same value as the last value 
+ * read at memory location specified in predicate_expr.
+ */
+struct predicate_expr {
+       token_t token;
+       void * location;
+       bool value;
+};
+
+class Predicate {
+public:
+       Predicate();
+       ~Predicate();
+
+       FuncInst * get_func_inst() { return func_inst; }
+       ModelList<predicate_expr> * get_predicates() { return &predicates; }
+       void add_predicate(predicate_expr predicate);
+
+       MEMALLOC
+private:
+       FuncInst * func_inst;
+       /* may have multiple precicates */
+       ModelList<predicate_expr> predicates;
+};