From 20926923f6de1790fdd368d5e7fa1738abe7b9a6 Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Fri, 20 Jul 2012 14:01:03 -0700 Subject: [PATCH] Add documentation [Split by Brian Norris] --- action.cc | 10 ++++++++++ cmodelint.cc | 10 ++++++++++ cmodelint.h | 4 ++++ cyclegraph.cc | 17 +++++++++++------ cyclegraph.h | 4 ++++ datarace.h | 6 +++++- hashtable.h | 9 +++++++++ nodestack.cc | 12 +++++++++++- 8 files changed, 64 insertions(+), 8 deletions(-) diff --git a/action.cc b/action.cc index 1fb3b76..f0ad48f 100644 --- a/action.cc +++ b/action.cc @@ -100,6 +100,14 @@ void ModelAction::copy_typeandorder(ModelAction * act) { this->order=act->order; } +/** This method changes an existing read part of an RMW action into either: + * (1) a full RMW action in case of the completed write or + * (2) a READ action in case a failed action. + */ + +//TODO: If the memory_order changes, we may potentially need to update our +//clock vector. + void ModelAction::process_rmw(ModelAction * act) { this->order=act->order; if (act->is_rmwc()) @@ -155,6 +163,8 @@ void ModelAction::create_cv(const ModelAction *parent) cv = new ClockVector(NULL, this); } + +/** Update the model action's read_from action */ void ModelAction::read_from(const ModelAction *act) { ASSERT(cv); diff --git a/cmodelint.cc b/cmodelint.cc index 4754a82..8919041 100644 --- a/cmodelint.cc +++ b/cmodelint.cc @@ -1,28 +1,38 @@ #include "model.h" #include "cmodelint.h" +/** Performs a read action.*/ uint64_t model_read_action(void * obj, memory_order ord) { model->switch_to_master(new ModelAction(ATOMIC_READ, ord, obj)); return thread_current()->get_return_value(); } +/** Performs a write action.*/ void model_write_action(void * obj, memory_order ord, uint64_t val) { model->switch_to_master(new ModelAction(ATOMIC_WRITE, ord, obj, val)); } +/** Performs an init action. */ void model_init_action(void * obj, uint64_t val) { model->switch_to_master(new ModelAction(ATOMIC_INIT, memory_order_relaxed, obj, val)); } +/** + * Performs the read part of a RMW action. The next action must either be the + * write part of the RMW action or an explicit close out of the RMW action w/o + * a write. + */ uint64_t model_rmwr_action(void *obj, memory_order ord) { model->switch_to_master(new ModelAction(ATOMIC_RMWR, ord, obj)); return thread_current()->get_return_value(); } +/** Performs the write part of a RMW action. */ void model_rmw_action(void *obj, memory_order ord, uint64_t val) { model->switch_to_master(new ModelAction(ATOMIC_RMW, ord, obj, val)); } +/** Closes out a RMW action without doing a write. */ void model_rmwc_action(void *obj, memory_order ord) { model->switch_to_master(new ModelAction(ATOMIC_RMWC, ord, obj)); } diff --git a/cmodelint.h b/cmodelint.h index 5e762f8..c23c061 100644 --- a/cmodelint.h +++ b/cmodelint.h @@ -1,3 +1,7 @@ +/** @file cmodelint.h + * @brief C interface to the model checker. + */ + #ifndef CMODELINT_H #define CMODELINT_H #include diff --git a/cyclegraph.cc b/cyclegraph.cc index c0e8e2a..f060a00 100644 --- a/cyclegraph.cc +++ b/cyclegraph.cc @@ -19,10 +19,10 @@ CycleNode * CycleGraph::getNode(const ModelAction * action) { return node; } -/** Adds an edge between two ModelActions. */ - -//the event to happens after the event from - +/** + * Adds an edge between two ModelActions. The ModelAction to happens after the + * ModelAction from. + */ void CycleGraph::addEdge(const ModelAction *to, const ModelAction *from) { CycleNode *fromnode=getNode(from); CycleNode *tonode=getNode(to); @@ -47,8 +47,11 @@ void CycleGraph::addEdge(const ModelAction *to, const ModelAction *from) { } } -//event rmw that reads from the node from - +/** Handles special case of a RMW action. The ModelAction rmw reads + * from the ModelAction from. The key differences are: (1) no write + * can occur in between the rmw and the from action. Only one RMW + * action can read from a given write. + */ void CycleGraph::addRMWEdge(const ModelAction *rmw, const ModelAction * from) { CycleNode *fromnode=getNode(from); CycleNode *rmwnode=getNode(rmw); @@ -116,10 +119,12 @@ void CycleNode::addEdge(CycleNode * node) { edges.push_back(node); } +/** Get the RMW CycleNode that reads from the current CycleNode. */ CycleNode* CycleNode::getRMW() { return hasRMW; } +/** Set a RMW action node that reads from the current CycleNode. */ bool CycleNode::setRMW(CycleNode * node) { CycleNode * oldhasRMW=hasRMW; hasRMW=node; diff --git a/cyclegraph.h b/cyclegraph.h index 3ed4e4a..5cf7093 100644 --- a/cyclegraph.h +++ b/cyclegraph.h @@ -1,3 +1,7 @@ +/** @file cyclegraph.h @brief Data structure to track ordering + * constraints on modification order. The idea is to see whether a + * total order exists that satisfies the ordering constriants.*/ + #ifndef CYCLEGRAPH_H #define CYCLEGRAPH_H diff --git a/datarace.h b/datarace.h index ef1ef8c..33a5c26 100644 --- a/datarace.h +++ b/datarace.h @@ -1,3 +1,7 @@ +/** @file datarace.h + * @brief Data race detection code. + */ + #ifndef DATARACE_H #include "config.h" #include @@ -19,7 +23,7 @@ void raceCheckRead(thread_id_t thread, void *location, ClockVector *currClock); -/** Encoding idea: +/** Basic encoding idea: * (void *) Either: * (1) points to a full record or * diff --git a/hashtable.h b/hashtable.h index b1cd327..c4cf290 100644 --- a/hashtable.h +++ b/hashtable.h @@ -1,3 +1,7 @@ +/** @file hashtable.h + * @brief Hashtable. Standard chained bucket variety. + */ + #ifndef HASHTABLE_H #define HASHTABLE_H @@ -36,6 +40,7 @@ template free(table); } + /** Reset the table to its initial state. */ void reset() { for(int i=0;i * bin = table[i]; @@ -49,6 +54,7 @@ template size=0; } + /** Put a key value pair into the table. */ void put(_Key key, _Val val) { if(size > threshold) { //Resize @@ -75,6 +81,7 @@ template table[(((_KeyInt)key)&mask)>>_Shift]=newptr; } + /** Lookup the corresponding value for the given key. */ _Val get(_Key key) { struct hashlistnode<_Key,_Val> *search = table[(((_KeyInt)key) & mask)>>_Shift]; @@ -87,6 +94,7 @@ template return (_Val)0; } + /** Check whether the table contains a value for the given key. */ bool contains(_Key key) { struct hashlistnode<_Key,_Val> *search = table[(((_KeyInt)key) & mask)>>_Shift]; @@ -99,6 +107,7 @@ template return false; } + /** Resize the table. */ void resize(unsigned int newsize) { struct hashlistnode<_Key,_Val> ** oldtable = table; struct hashlistnode<_Key,_Val> ** newtable; diff --git a/nodestack.cc b/nodestack.cc index 1de5169..e8f377b 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -77,6 +77,11 @@ bool Node::backtrack_empty() return (numBacktracks == 0); } + +/** + * Checks whether the readsfrom set for this node is empty. + * @return true if the readsfrom set is empty. + */ bool Node::readsfrom_empty() { return ((read_from_index+1)>=may_read_from.size()); } @@ -148,6 +153,10 @@ const ModelAction * Node::get_read_from() { return may_read_from[read_from_index]; } +/** + * Increments the index into the readsfrom set to explore the next item. + * @return Returns false if we have explored all items. + */ bool Node::increment_read_from() { read_from_index++; return (read_from_index