Skip to content

Commit

Permalink
TSOTraceBuilder: Record the point of replay
Browse files Browse the repository at this point in the history
This will allow the is_replaying() predicate to return the right thing,
allowing the non-determinism checking to work with Optimal-DPOR.
  • Loading branch information
margnus1 committed Apr 3, 2018
1 parent 5e9f2c7 commit 702d438
Show file tree
Hide file tree
Showing 2 changed files with 8 additions and 1 deletion.
4 changes: 3 additions & 1 deletion src/TSOTraceBuilder.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@ TSOTraceBuilder::TSOTraceBuilder(const Configuration &conf) : TSOPSOTraceBuilder
replay = false;
last_full_memory_conflict = -1;
last_md = 0;
replay_point = 0;
}

TSOTraceBuilder::~TSOTraceBuilder(){
Expand Down Expand Up @@ -161,7 +162,7 @@ void TSOTraceBuilder::mark_unavailable(int proc, int aux){
}

bool TSOTraceBuilder::is_replaying() const {
return replay;
return prefix_idx < replay_point;
}

void TSOTraceBuilder::cancel_replay(){
Expand Down Expand Up @@ -232,6 +233,7 @@ bool TSOTraceBuilder::reset(){
/* No more branching is possible. */
return false;
}
replay_point = i;

/* Setup the new Event at prefix[i] */
{
Expand Down
5 changes: 5 additions & 0 deletions src/TSOTraceBuilder.h
Original file line number Diff line number Diff line change
Expand Up @@ -358,6 +358,11 @@ class TSOTraceBuilder : public TSOPSOTraceBuilder{
*/
bool replay;

/* The number of events that were or are going to be replayed in the
* current computation.
*/
int replay_point;

/* The latest value passed to this->metadata(). */
const llvm::MDNode *last_md;

Expand Down

0 comments on commit 702d438

Please sign in to comment.