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())
cv = new ClockVector(NULL, this);
}
+
+/** Update the model action's read_from action */
void ModelAction::read_from(const ModelAction *act)
{
ASSERT(cv);
#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));
}
+/** @file cmodelint.h
+ * @brief C interface to the model checker.
+ */
+
#ifndef CMODELINT_H
#define CMODELINT_H
#include <inttypes.h>
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);
}
}
-//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);
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;
+/** @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
+/** @file datarace.h
+ * @brief Data race detection code.
+ */
+
#ifndef DATARACE_H
#include "config.h"
#include <stdint.h>
-/** Encoding idea:
+/** Basic encoding idea:
* (void *) Either:
* (1) points to a full record or
*
+/** @file hashtable.h
+ * @brief Hashtable. Standard chained bucket variety.
+ */
+
#ifndef HASHTABLE_H
#define HASHTABLE_H
free(table);
}
+ /** Reset the table to its initial state. */
void reset() {
for(int i=0;i<capacity;i++) {
struct hashlistnode<_Key,_Val> * bin = table[i];
size=0;
}
+ /** Put a key value pair into the table. */
void put(_Key key, _Val val) {
if(size > threshold) {
//Resize
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];
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];
return false;
}
+ /** Resize the table. */
void resize(unsigned int newsize) {
struct hashlistnode<_Key,_Val> ** oldtable = table;
struct hashlistnode<_Key,_Val> ** newtable;
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());
}
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<may_read_from.size());
* destructor for each. This function is provided an offset which determines
* how many nodes (relative to the current replay state) to save before popping
* the stack.
- * @param numAhead The number of nodes to skip forward before popping the stack.
+ * @param numAhead gives the number of Nodes (including this Node) to skip over
+ * before removing nodes.
*/
void NodeStack::pop_restofstack(int numAhead)
{
projects / model-checker.git / commitdiff