projects
/
c11tester.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
experiment with adding NULLITY predicate
[c11tester.git]
/
funcinst.h
diff --git
a/funcinst.h
b/funcinst.h
index 654ba653edce66af902541dc9198703176d5ed04..3b2890f0bdafa33ea9e041b23ddfa47987eb3fac 100644
(file)
--- a/
funcinst.h
+++ b/
funcinst.h
@@
-13,7
+13,6
@@
public:
FuncInst(ModelAction *act, FuncNode *func_node);
~FuncInst();
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; }
action_type get_type() const { return type; }
const char * get_position() const { return position; }
void * get_location() const { return location; }
action_type get_type() const { return type; }
@@
-23,30
+22,40
@@
public:
bool add_pred(FuncInst * other);
bool add_succ(FuncInst * other);
bool add_pred(FuncInst * other);
bool add_succ(FuncInst * other);
- FuncInst * search_in_collision(ModelAction *act);
+ //FuncInst * search_in_collision(ModelAction *act);
+ //func_inst_list_mt * get_collisions() { return &collisions; }
- 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;
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 print();
MEMALLOC
private:
void print();
MEMALLOC
private:
- //ModelAction * const action;
const char * position;
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;
action_type type;
memory_order order;
FuncNode * func_node;
void * location;
action_type type;
memory_order order;
FuncNode * func_node;
- /* collisions store a list of FuncInsts with the same position
+ bool single_location;
+
+ /* Currently not in use. May remove this field later
+ *
+ * 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 */
* but different action types. For example, CAS is broken down
* as three different atomic operations in cmodelint.cc */
- func_inst_list_mt collisions;
+
//
func_inst_list_mt collisions;
func_inst_list_mt predecessors;
func_inst_list_mt successors;
func_inst_list_mt predecessors;
func_inst_list_mt successors;