X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=funcinst.h;h=c4d41eec32fb69211e11a6c84f36299335857a84;hp=85b9c20ecce2d9b07d8b85168fc3f1bbe39701b4;hb=25d73096cfc14c655f94b01bb235cc5efd1d5696;hpb=080c029c02600d44ad7d797c8e373d4df899f9b0 diff --git a/funcinst.h b/funcinst.h index 85b9c20e..c4d41eec 100644 --- a/funcinst.h +++ b/funcinst.h @@ -1,7 +1,10 @@ +#ifndef __FUNCINST_H__ +#define __FUNCINST_H__ + #include "action.h" +#include "classlist.h" #include "hashtable.h" - -class ModelAction; +#include "threads-model.h" typedef ModelList func_inst_list_mt; @@ -10,36 +13,70 @@ public: FuncInst(ModelAction *act, FuncNode *func_node); ~FuncInst(); - //ModelAction * get_action() const { return action; } const char * get_position() const { return position; } + void * get_location() const { return location; } + void set_location(void * loc) { location = loc; } + action_type get_type() const { return type; } + memory_order get_mo() const { return order; } FuncNode * get_func_node() const { return func_node; } bool add_pred(FuncInst * other); bool add_succ(FuncInst * other); FuncInst * search_in_collision(ModelAction *act); + void add_to_collision(FuncInst * inst); - func_inst_list_mt * get_collisions() { return &collisions; } func_inst_list_mt * get_preds() { return &predecessors; } func_inst_list_mt * get_succs() { return &successors; } bool is_read() const; + bool is_write() const; + bool is_single_location() { return single_location; } + void not_single_location() { single_location = false; } + + void set_execution_number(int new_number) { execution_number = new_number; } + int get_execution_number() { return execution_number; } + + void set_associated_read(thread_id_t tid, int index, uint32_t marker, uint64_t read_val); + uint64_t get_associated_read(thread_id_t tid, int index, uint32_t marker); + + void print(); MEMALLOC private: - //ModelAction * const action; const char * position; + + /* Atomic operations with the same source line number may act at different + * memory locations, such as the next field of the head pointer in ms-queue. + * location only stores the memory location when this FuncInst was constructed. + */ void * location; + + /* NOTE: for rmw actions, func_inst and act may have different + * action types because of action type conversion in ModelExecution */ action_type type; + + memory_order order; FuncNode * func_node; - /* collisions store a list of FuncInsts with the same position - * but different action types. For example, CAS is broken down - * as three different atomic operations in cmodelint.cc */ + bool single_location; + int execution_number; + + ModelVector< ModelVector * > associated_reads; + ModelVector< ModelVector * > thrd_markers; + + /** + * Collisions store a list of FuncInsts with the same position + * but different action types. For example, + * volatile int x; x++; produces read and write + * actions with the same position. + */ func_inst_list_mt collisions; func_inst_list_mt predecessors; func_inst_list_mt successors; }; + +#endif /* __FUNCINST_H__ */