From ea6532a2672216e8d9d9dce8297dcc8d614dbbad Mon Sep 17 00:00:00 2001
From: Markus Alexander Kuppe <tlaplus.net@lemmster.de>
Date: Fri, 8 May 2015 12:05:36 +0200
Subject: [PATCH] [Bugfix] Check liveness regardless of checkpointing. Up to
now, the checkpointing interval would - as a side effect - also be the
liveness checking interval essentially turning the nextLiveCheck logic into
dead code. From now on, liveness checking is run when the amount of current
states in the fingerprint set has reached nextLiveCheck (which is probably
what was initially intended).
Note that deactivating checkpointing (with "-checkpoint 0") used to
deactivate partial liveness checking too. In this case liveness was only
checked finally at the end of model checking.
---
tlatools/src/tlc2/tool/AbstractChecker.java | 7 +--
tlatools/src/tlc2/tool/DFIDModelChecker.java | 36 +++++++-------
tlatools/src/tlc2/tool/ModelChecker.java | 49 +++++++++++---------
3 files changed, 48 insertions(+), 44 deletions(-)
diff --git a/tlatools/src/tlc2/tool/AbstractChecker.java b/tlatools/src/tlc2/tool/AbstractChecker.java
index 5115e6a3e..86c1246e9 100644
--- a/tlatools/src/tlc2/tool/AbstractChecker.java
+++ b/tlatools/src/tlc2/tool/AbstractChecker.java
@@ -257,12 +257,9 @@ public abstract class AbstractChecker implements Cancelable
// while (true) {
while (!this.cancellationFlag)
{
- if (TLCGlobals.doCheckPoint())
+ if (!this.doPeriodicWork())
{
- if (!this.doPeriodicWork())
- {
- return false;
- }
+ return false;
}
synchronized (this)
{
diff --git a/tlatools/src/tlc2/tool/DFIDModelChecker.java b/tlatools/src/tlc2/tool/DFIDModelChecker.java
index de5506dcb..3f26db584 100644
--- a/tlatools/src/tlc2/tool/DFIDModelChecker.java
+++ b/tlatools/src/tlc2/tool/DFIDModelChecker.java
@@ -630,24 +630,26 @@ public class DFIDModelChecker extends AbstractChecker
nextLiveCheck = (stateNum < 600000) ? stateNum * 2 : stateNum + 200000;
}
- // Checkpoint:
- MP.printMessage(EC.TLC_CHECKPOINT_START, this.metadir);
- // start checkpointing:
- this.theFPSet.beginChkpt();
- if (this.checkLiveness)
- {
- liveCheck.beginChkpt();
- }
- UniqueString.internTbl.beginChkpt(this.metadir);
-
- // Commit checkpoint:
- this.theFPSet.commitChkpt();
- if (this.checkLiveness)
- {
- liveCheck.commitChkpt();
+ if (TLCGlobals.doCheckPoint()) {
+ // Checkpoint:
+ MP.printMessage(EC.TLC_CHECKPOINT_START, this.metadir);
+ // start checkpointing:
+ this.theFPSet.beginChkpt();
+ if (this.checkLiveness)
+ {
+ liveCheck.beginChkpt();
+ }
+ UniqueString.internTbl.beginChkpt(this.metadir);
+
+ // Commit checkpoint:
+ this.theFPSet.commitChkpt();
+ if (this.checkLiveness)
+ {
+ liveCheck.commitChkpt();
+ }
+ UniqueString.internTbl.commitChkpt(this.metadir);
+ MP.printMessage(EC.TLC_CHECKPOINT_END);
}
- UniqueString.internTbl.commitChkpt(this.metadir);
- MP.printMessage(EC.TLC_CHECKPOINT_END);
}
return true;
}
diff --git a/tlatools/src/tlc2/tool/ModelChecker.java b/tlatools/src/tlc2/tool/ModelChecker.java
index 3db3f9819..bff94e3d0 100644
--- a/tlatools/src/tlc2/tool/ModelChecker.java
+++ b/tlatools/src/tlc2/tool/ModelChecker.java
@@ -658,29 +658,34 @@ public class ModelChecker extends AbstractChecker
nextLiveCheck = (stateNum <= 640000) ? stateNum * 2 : stateNum + 640000;
}
- // Checkpoint:
- MP.printMessage(EC.TLC_CHECKPOINT_START, this.metadir);
-
- // start checkpointing:
- this.theStateQueue.beginChkpt();
- this.trace.beginChkpt();
- this.theFPSet.beginChkpt();
- this.theStateQueue.resumeAll();
- UniqueString.internTbl.beginChkpt(this.metadir);
- if (this.checkLiveness)
- {
- liveCheck.beginChkpt();
- }
- // commit checkpoint:
- this.theStateQueue.commitChkpt();
- this.trace.commitChkpt();
- this.theFPSet.commitChkpt();
- UniqueString.internTbl.commitChkpt(this.metadir);
- if (this.checkLiveness)
- {
- liveCheck.commitChkpt();
+ if (TLCGlobals.doCheckPoint()) {
+ // Checkpoint:
+ MP.printMessage(EC.TLC_CHECKPOINT_START, this.metadir);
+
+ // start checkpointing:
+ this.theStateQueue.beginChkpt();
+ this.trace.beginChkpt();
+ this.theFPSet.beginChkpt();
+ this.theStateQueue.resumeAll();
+ UniqueString.internTbl.beginChkpt(this.metadir);
+ if (this.checkLiveness)
+ {
+ liveCheck.beginChkpt();
+ }
+ // commit checkpoint:
+ this.theStateQueue.commitChkpt();
+ this.trace.commitChkpt();
+ this.theFPSet.commitChkpt();
+ UniqueString.internTbl.commitChkpt(this.metadir);
+ if (this.checkLiveness)
+ {
+ liveCheck.commitChkpt();
+ }
+ MP.printMessage(EC.TLC_CHECKPOINT_END);
+ } else {
+ // Just resume worker threads when checkpointing is skipped
+ this.theStateQueue.resumeAll();
}
- MP.printMessage(EC.TLC_CHECKPOINT_END);
}
return true;
}
--
GitLab