From bdef0741b8a01e16946d261bc2a657af5a683b3e Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Wed, 25 Jul 2012 16:11:51 -0700 Subject: [PATCH] some changes towards reading from future writes --- Makefile | 6 +++--- model.cc | 2 ++ model.h | 3 +++ nodestack.cc | 49 +++++++++++++++++++++++++++++++++++++++++++++++-- nodestack.h | 8 ++++++++ promise.cc | 8 ++++++++ promise.h | 23 +++++++++++++++++++++++ 7 files changed, 94 insertions(+), 5 deletions(-) create mode 100644 promise.cc create mode 100644 promise.h diff --git a/Makefile b/Makefile index 2d31611..4526ed7 100644 --- a/Makefile +++ b/Makefile @@ -8,9 +8,9 @@ LIB_SO=lib$(LIB_NAME).so USER_O=userprog.o USER_H=libthreads.h -MODEL_CC=libthreads.cc schedule.cc model.cc threads.cc librace.cc action.cc nodestack.cc clockvector.cc main.cc snapshot-interface.cc cyclegraph.cc datarace.cc impatomic.cc cmodelint.cc -MODEL_O=libthreads.o schedule.o model.o threads.o librace.o action.o nodestack.o clockvector.o main.o snapshot-interface.o cyclegraph.o datarace.o impatomic.o cmodelint.o -MODEL_H=libthreads.h schedule.h common.h model.h threads.h librace.h action.h nodestack.h clockvector.h snapshot-interface.h cyclegraph.h hashtable.h datarace.h config.h include/impatomic.h include/cstdatomic include/stdatomic.h cmodelint.h +MODEL_CC=libthreads.cc schedule.cc model.cc threads.cc librace.cc action.cc nodestack.cc clockvector.cc main.cc snapshot-interface.cc cyclegraph.cc datarace.cc impatomic.cc cmodelint.cc promise.cc +MODEL_O=libthreads.o schedule.o model.o threads.o librace.o action.o nodestack.o clockvector.o main.o snapshot-interface.o cyclegraph.o datarace.o impatomic.o cmodelint.o promise.o +MODEL_H=libthreads.h schedule.h common.h model.h threads.h librace.h action.h nodestack.h clockvector.h snapshot-interface.h cyclegraph.h hashtable.h datarace.h config.h include/impatomic.h include/cstdatomic include/stdatomic.h cmodelint.h promise.h SHMEM_CC=snapshot.cc malloc.c mymemory.cc SHMEM_O=snapshot.o malloc.o mymemory.o diff --git a/model.cc b/model.cc index a9d76c6..bfa3e02 100644 --- a/model.cc +++ b/model.cc @@ -8,6 +8,7 @@ #include "common.h" #include "clockvector.h" #include "cyclegraph.h" +#include "promise.h" #define INITIAL_THREAD_ID 0 @@ -30,6 +31,7 @@ ModelChecker::ModelChecker() thread_map(new HashTable()), obj_map(new HashTable()), obj_thrd_map(new HashTable, uintptr_t, 4 >()), + promises(new std::vector(1)), thrd_last_action(new std::vector(1)), node_stack(new NodeStack()), next_backtrack(NULL), diff --git a/model.h b/model.h index b6099c6..41ec97b 100644 --- a/model.h +++ b/model.h @@ -16,10 +16,12 @@ #include "threads.h" #include "action.h" #include "clockvector.h" +#include "hashtable.h" /* Forward declaration */ class NodeStack; class CycleGraph; +class Promise; /** @brief The central structure for model-checking */ class ModelChecker { @@ -99,6 +101,7 @@ private: HashTable *obj_map; HashTable, uintptr_t, 4 > *obj_thrd_map; + std::vector * promises; std::vector *thrd_last_action; NodeStack *node_stack; ModelAction *next_backtrack; diff --git a/nodestack.cc b/nodestack.cc index 409c4e1..6295442 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -25,7 +25,9 @@ Node::Node(ModelAction *act, Node *par, int nthreads) backtrack(num_threads), numBacktracks(0), may_read_from(), - read_from_index(0) + read_from_index(0), + future_values(), + future_index(0) { if (act) act->set_node(this); @@ -55,6 +57,19 @@ void Node::print_may_read_from() (*it)->print(); } +/** + * Adds a value from a weakly ordered future write to backtrack to. + * @param value is the value to backtrack to. + */ + +void Node::add_future_value(uint64_t value) { + for(int i=0;i=may_read_from.size()); } +/** + * Checks whether the future_values set for this node is empty. + * @return true if the future_values set is empty. + */ + +bool Node::futurevalues_empty() { + return ((future_index+1)>=future_values.size()); +} + /** - * Mark the appropriate backtracking infromation for exploring a thread choice. + * Mark the appropriate backtracking information for exploring a thread choice. * @param act The ModelAction to explore */ void Node::explore_child(ModelAction *act) @@ -141,6 +165,17 @@ void Node::add_read_from(const ModelAction *act) may_read_from.push_back(act); } +/** + * Gets the next 'future_value' value from this Node. Only valid for a node + * where this->action is a 'read'. + * @return The first element in future_values + */ + +uint64_t Node::get_future_value() { + ASSERT(future_indexaction is a 'read'. @@ -162,6 +197,16 @@ bool Node::increment_read_from() { return (read_from_index > readfrom_set_t; +typedef std::vector< uint64_t, MyAlloc< uint64_t > > futurevalues_t; /** * @brief A single node in a NodeStack @@ -33,6 +34,7 @@ public: /* return true = backtrack set is empty */ bool backtrack_empty(); bool readsfrom_empty(); + bool futurevalues_empty(); void explore_child(ModelAction *act); /* return false = thread was already in backtrack */ bool set_backtrack(thread_id_t id); @@ -44,9 +46,12 @@ public: * occurred previously in the stack. */ Node * get_parent() const { return parent; } + void add_future_value(uint64_t value); void add_read_from(const ModelAction *act); const ModelAction * get_read_from(); + uint64_t get_future_value(); bool increment_read_from(); + bool increment_future_values(); void print(); void print_may_read_from(); @@ -66,6 +71,9 @@ private: * from. Only meaningful if this Node represents a 'read' action. */ readfrom_set_t may_read_from; unsigned int read_from_index; + + futurevalues_t future_values; + unsigned int future_index; }; typedef std::list< Node *, MyAlloc< Node * > > node_list_t; diff --git a/promise.cc b/promise.cc new file mode 100644 index 0000000..b051ef0 --- /dev/null +++ b/promise.cc @@ -0,0 +1,8 @@ +#include "promise.h" + +Promise::Promise(ModelAction *act, uint64_t value) { + this->value=value; + this->read=act; + this->numthreads=1; +} + diff --git a/promise.h b/promise.h new file mode 100644 index 0000000..a47982d --- /dev/null +++ b/promise.h @@ -0,0 +1,23 @@ +/** @file promise.h + * + * @brief Promise class --- tracks future obligations for execution + * related to weakly ordered writes. + */ + +#ifndef __PROMISE_H__ +#define __PROMISE_H__ +#include + + +class ModelAction; + +class Promise { + public: + Promise(ModelAction * act, uint64_t value); + private: + uint64_t value; + ModelAction *read; + unsigned int numthreads; +}; + +#endif -- 2.34.1