X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=funcnode.h;h=4ba239856df8e468a7bf4f6b7518a7a95381bed7;hb=9a2ba97d13c76e9048ba7c499b3cbca0d02a84ca;hp=51f19f0cce65812a9771c60e796093357e024911;hpb=080c029c02600d44ad7d797c8e373d4df899f9b0;p=c11tester.git diff --git a/funcnode.h b/funcnode.h index 51f19f0c..4ba23985 100644 --- a/funcnode.h +++ b/funcnode.h @@ -1,10 +1,14 @@ +#ifndef __FUNCNODE_H__ +#define __FUNCNODE_H__ + #include "action.h" #include "funcinst.h" #include "hashtable.h" - -class ModelAction; +#include "hashset.h" +#include "predicate.h" typedef ModelList func_inst_list_mt; +typedef HashTable read_map_t; class FuncNode { public: @@ -16,25 +20,37 @@ public: void set_func_id(uint32_t id) { func_id = id; } void set_func_name(const char * name) { func_name = name; } - FuncInst * get_or_add_action(ModelAction *act); + void add_inst(ModelAction *act); + FuncInst * get_inst(ModelAction *act); HashTable * getFuncInstMap() { return &func_inst_map; } func_inst_list_mt * get_inst_list() { return &inst_list; } func_inst_list_mt * get_entry_insts() { return &entry_insts; } void add_entry_inst(FuncInst * inst); - void group_reads_by_loc(FuncInst * inst); + void update_tree(action_list_t * act_list); + void update_inst_tree(func_inst_list_t * inst_list); + + void store_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 update_predicate_tree(action_list_t * act_list); + bool follow_branch(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act, HashTable* loc_act_map); + void print_predicate_tree(); + + void print_last_read(uint32_t tid); MEMALLOC private: uint32_t func_id; const char * func_name; + bool predicate_tree_initialized; + Predicate * predicate_tree_entry; // a dummy node whose children are the real entries - /* Use source line number as the key of hashtable, to check if + /* Use source line number as the key of hashtable, to check if * atomic operation with this line number has been added or not - * - * To do: cds_atomic_compare_exchange contains three atomic operations - * that are feeded with the same source line number by llvm pass */ HashTable func_inst_map; @@ -44,6 +60,8 @@ private: /* possible entry atomic actions in this function */ func_inst_list_mt entry_insts; - /* group atomic read actions by memory location */ - HashTable reads_by_loc; + /* Store the values read by atomic read actions per memory location for each thread */ + ModelVector thrd_read_map; }; + +#endif /* __FUNCNODE_H__ */