From: weiyu Date: Sat, 27 Jul 2019 01:23:50 +0000 (-0700) Subject: planning to build a predicate generator based on values that have been written to... X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=729acbffd2562f10dd1864b010c3623faa485513 planning to build a predicate generator based on values that have been written to memory locations historically --- diff --git a/funcinst.cc b/funcinst.cc index 7e0446ff..92890d58 100644 --- 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 85b9c20e..efdb43b4 100644 --- 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 281e0f05..208bc3be 100644 --- a/funcnode.cc +++ b/funcnode.cc @@ -1,4 +1,5 @@ #include "funcnode.h" +#include "predicate.h" FuncNode::FuncNode() : func_inst_map(), @@ -164,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 f80e9266..08e07fb1 100644 --- 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 func_inst_list_mt; typedef HashTable read_map_t; @@ -29,6 +30,9 @@ public: 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 thrd_read_map; ModelList read_locations; }; + +#endif /* __FUNCNODE_H__ */ diff --git a/history.cc b/history.cc index 267205db..7b6e3c87 100644 --- a/history.cc +++ b/history.cc @@ -13,7 +13,8 @@ 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) @@ -118,6 +119,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); @@ -150,6 +154,15 @@ uint64_t ModelHistory::query_last_read(void * location, thread_id_t 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 184646c6..5709ab6c 100644 --- 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 write_set_t; + class ModelHistory { public: ModelHistory(); @@ -24,6 +30,8 @@ public: 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(); MEMALLOC @@ -36,4 +44,7 @@ private: ModelVector func_map_rev; ModelVector func_nodes; + HashTable write_history; }; + +#endif /* __HISTORY_H__ */ diff --git a/predicate.cc b/predicate.cc new file mode 100644 index 00000000..9f4246e9 --- /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::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 index 00000000..e2412d18 --- /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 * get_predicates() { return &predicates; } + void add_predicate(predicate_expr predicate); + + MEMALLOC +private: + FuncInst * func_inst; + /* may have multiple precicates */ + ModelList predicates; +};