return false;
}
-/**
- * Gets the clock corresponding to a given thread id from the clock
- * vector. */
-
+/** Gets the clock corresponding to a given thread id from the clock vector. */
modelclock_t ClockVector::getClock(thread_id_t thread) {
int threadid = id_to_int(thread);
#include "action.h"
/** Initializes a CycleGraph object. */
-
CycleGraph::CycleGraph() {
hasCycles=false;
}
/** Returns the CycleNode for a given ModelAction. */
-
CycleNode * CycleGraph::getNode(ModelAction * action) {
CycleNode *node=actionToNode.get(action);
if (node==NULL) {
}
/** Adds an edge between two ModelActions. */
-
void CycleGraph::addEdge(ModelAction *from, ModelAction *to) {
CycleNode *fromnode=getNode(from);
CycleNode *tonode=getNode(to);
}
/** Checks whether the first CycleNode can reach the second one. */
-
bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to) {
std::vector<CycleNode *> queue;
HashTable<CycleNode *, CycleNode *, uintptr_t, 4> discovered;
}
/** Constructor for a CycleNode. */
-
CycleNode::CycleNode(ModelAction *modelaction) {
action=modelaction;
}
/** Returns a vector of the edges from a CycleNode. */
-
std::vector<CycleNode *> * CycleNode::getEdges() {
return &edges;
}
/** Adds an edge to a CycleNode. */
-
void CycleNode::addEdge(CycleNode * node) {
edges.push_back(node);
}
struct ShadowTable *root;
/** This function initialized the data race detector. */
-
void initRaceDetector() {
root=(struct ShadowTable *) calloc(sizeof(struct ShadowTable),1);
}
-/** This function looks up the entry in the shadow table corresponding
- to a given address.*/
-
+/** This function looks up the entry in the shadow table corresponding to a
+ * given address.*/
static uint64_t * lookupAddressEntry(void * address) {
struct ShadowTable *currtable=root;
#ifdef BIT48
* Expands a record from the compact form to the full form. This is
* necessary for multiple readers or for very large thread ids or time
* stamps. */
-
static void expandRecord(uint64_t * shadow) {
uint64_t shadowval=*shadow;
}
/** This function is called when we detect a data race.*/
-
static void reportDataRace() {
printf("The reportDataRace method should report useful things about this datarace!\n");
}
-/** This function does race detection for a write on an expanded
- * record. */
-
+/** This function does race detection for a write on an expanded record. */
void fullRaceCheckWrite(thread_id_t thread, uint64_t * shadow, ClockVector *currClock) {
struct RaceRecord * record=(struct RaceRecord *) (*shadow);
record->writeClock=ourClock;
}
-/** This function does race detection on a write.
- */
-
+/** This function does race detection on a write. */
void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock) {
uint64_t * shadow=lookupAddressEntry(location);
uint64_t shadowval=*shadow;
*shadow = ENCODEOP(0, 0, threadid, ourClock);
}
-/** This function does race detection on a read for an expanded
- * record. */
-
+/** This function does race detection on a read for an expanded record. */
void fullRaceCheckRead(thread_id_t thread, uint64_t * shadow, ClockVector *currClock) {
struct RaceRecord * record=(struct RaceRecord *) (*shadow);
}
/** This function does race detection on a read. */
-
void raceCheckRead(thread_id_t thread, void *location, ClockVector *currClock) {
uint64_t * shadow=lookupAddressEntry(location);
uint64_t shadowval=*shadow;
#include "model.h"
#include "snapshot-interface.h"
-/** The thread_system_next function takes the next step in the
- * execution. @return Returns the 1 if there is another step and 0
- * otherwise.
+/**
+ * The thread_system_next function takes the next step in the execution.
+ * @return Returns the 1 if there is another step and 0 otherwise.
*/
-
static int thread_system_next(void) {
Thread *curr, *next;
/** The thread_wait_finish method runs the current execution until we
* have no more steps to take.
*/
-
static void thread_wait_finish(void) {
DBG();
/** The real_main function contains the main model checking loop. */
-
static void real_main() {
thrd_t user_thread;
ucontext_t main_context;
#endif
/** Non-snapshotting malloc for our use. */
-
void *MYMALLOC(size_t size) {
#if USE_MPROTECT_SNAPSHOT
static void *(*mallocp)(size_t size);
/** Adding the fix for not able to allocate through a reimplemented calloc at the beginning before instantiating our allocator
A bit circumspect about adding an sbrk. linux docs say to avoid using it... */
-
void * HandleEarlyAllocationRequest( size_t sz ){
if( 0 == mySpace ){
void * returnAddress = sbrk( sz );
}
/** The fact that I am not expecting more than a handful requests is implicit in my not using a binary search here*/
-
bool DontFree( void * ptr ){
if( howManyFreed == nextRequest ) return false; //a minor optimization to reduce the number of instructions executed on each free call....
if( NULL == ptr ) return true;
}
/** Snapshotting malloc implementation for user programs. */
-
void *malloc( size_t size ) {
void * earlyReq = HandleEarlyAllocationRequest( size );
if( earlyReq ) return earlyReq;
}
/** Snapshotting free implementation for user programs. */
-
void free( void * ptr ){
if( DontFree( ptr ) ) return;
mspace_free( mySpace, ptr );
}
/** Snapshotting realloc implementation for user programs. */
-
void *realloc( void *ptr, size_t size ){
return mspace_realloc( mySpace, ptr, size );
}
/** Snapshotting calloc implementation for user programs. */
-
void * calloc( size_t num, size_t size ){
void * earlyReq = HandleEarlyAllocationRequest( size * num );
if( earlyReq ) {
}
/** Snapshotting new operator for user programs. */
-
void * operator new(size_t size) throw(std::bad_alloc) {
return malloc(size);
}
/** Snapshotting delete operator for user programs. */
-
void operator delete(void *p) throw() {
free(p);
}
/** Snapshotting new[] operator for user programs. */
-
void * operator new[](size_t size) throw(std::bad_alloc) {
return malloc(size);
}
/** Snapshotting delete[] operator for user programs. */
-
void operator delete[](void *p, size_t size) {
free(p);
}
/** MEMALLOC declares the allocators for a class to allocate
* memory in the non-snapshotting heap. */
-
#define MEMALLOC \
void * operator new(size_t size) { \
return MYMALLOC(size);\
/** SNAPSHOTALLOC declares the allocators for a class to allocate
* memory in the snapshotting heap. */
-
#define SNAPSHOTALLOC
void *MYMALLOC(size_t size);
* This software is provided "as is" without express or implied
* warranty, and with no claim as to its suitability for any purpose.
*/
-
template <class T>
class MyAlloc {
public:
* @param seqindex is the sequence number to rollback before.
* @return is the sequence number we actually rolled back to.
*/
-
int SnapshotStack::backTrackBeforeStep(int seqindex) {
while(true) {
if (stack->index<=seqindex) {
}
}
-/** This method takes a snapshot at the given sequence number.
- */
-
+/** This method takes a snapshot at the given sequence number. */
void SnapshotStack::snapshotStep(int seqindex) {
struct stackEntry *tmp=(struct stackEntry *)MYMALLOC(sizeof(struct stackEntry));
tmp->next=stack;
projects / model-checker.git / commitdiff