diff --git a/tlatools/src/tlc2/TLCGlobals.java b/tlatools/src/tlc2/TLCGlobals.java index 8907e8f25fd5a72be9e74ea5e0f72fdabea9e078..c24ce83f4f01407a0a530e47e239f08107ea6f94 100644 --- a/tlatools/src/tlc2/TLCGlobals.java +++ b/tlatools/src/tlc2/TLCGlobals.java @@ -26,6 +26,12 @@ public class TLCGlobals // Number of concurrent workers private static int numWorkers = 1; + + /** + * Execute liveness checking when any of the disk graphs' size has increased + * exceeding the threshold (10% by default). + */ + public static double livenessThreshold = 0.1d; public synchronized static void setNumWorkers(int n) { diff --git a/tlatools/src/tlc2/tool/AbstractChecker.java b/tlatools/src/tlc2/tool/AbstractChecker.java index 86c1246e9dbfd16f7af651b728c84995d6307ded..cac02087403e4bc837d1ec2df70ee62e1aac834e 100644 --- a/tlatools/src/tlc2/tool/AbstractChecker.java +++ b/tlatools/src/tlc2/tool/AbstractChecker.java @@ -29,12 +29,9 @@ import util.FilenameToStream; */ public abstract class AbstractChecker implements Cancelable { - public static final String NEXT_LIVECHECK = AbstractChecker.class.getName() + ".nextLiveCheck"; - protected static final boolean LIVENESS_STATS = Boolean.getBoolean(Liveness.class.getPackage().getName() + ".statistics"); // SZ Mar 9, 2009: static modifier removed - protected long nextLiveCheck; protected AtomicLong numOfGenStates; protected TLCState predErrState; protected TLCState errState; @@ -84,17 +81,6 @@ public abstract class AbstractChecker implements Cancelable // moved to file utilities this.metadir = FileUtil.makeMetaDir(specDir, fromChkpt); - // The number of states generated before the first liveness check is - // performed. This value of 1000 sounds low, but since the value is - // doubled after each check up to a maximum of 640K (a number embedded - // in several places in the code), it probably doesn't much matter. - // - // The default of 1000 states can be overridden with a system property. - // This is e.g. used by unit tests to prevent periodic liveness checking - // (setting nextLiveCheck to Long.MAX_VALUE) and force TLC to check - // liveness only at the end of model checking. This gives predictable - // results required by unit tests. - this.nextLiveCheck = Long.getLong(NEXT_LIVECHECK, 1000); this.numOfGenStates = new AtomicLong(0); this.errState = null; this.predErrState = null; diff --git a/tlatools/src/tlc2/tool/DFIDModelChecker.java b/tlatools/src/tlc2/tool/DFIDModelChecker.java index 3f26db5849d3e8c37018a1453017a72aafffc405..6cf83959cfe510fa255c5168eafb90180dc4e0f2 100644 --- a/tlatools/src/tlc2/tool/DFIDModelChecker.java +++ b/tlatools/src/tlc2/tool/DFIDModelChecker.java @@ -618,16 +618,12 @@ public class DFIDModelChecker extends AbstractChecker synchronized (this.theFPSet) { // Run liveness checking, if needed: - long stateNum = this.theFPSet.size(); - boolean doCheck = this.checkLiveness && (stateNum >= nextLiveCheck); - if (doCheck) + if (this.checkLiveness) { - MP.printMessage(EC.TLC_CHECKING_TEMPORAL_PROPS, new String[] {"current", Long.toString(stateNum)}); - if (!liveCheck.check()) + if (!liveCheck.check(false)) { return false; } - nextLiveCheck = (stateNum < 600000) ? stateNum * 2 : stateNum + 200000; } if (TLCGlobals.doCheckPoint()) { diff --git a/tlatools/src/tlc2/tool/ModelChecker.java b/tlatools/src/tlc2/tool/ModelChecker.java index bff94e3d073c76b957ac98ccf40726a84f786f33..8b31f20f14163e6bbe92d7087d46fb752a7bf5a6 100644 --- a/tlatools/src/tlc2/tool/ModelChecker.java +++ b/tlatools/src/tlc2/tool/ModelChecker.java @@ -648,14 +648,10 @@ public class ModelChecker extends AbstractChecker if (this.theStateQueue.suspendAll()) { // Run liveness checking, if needed: - long stateNum = this.theFPSet.size(); - boolean doCheck = this.checkLiveness && (stateNum >= nextLiveCheck); - if (doCheck) + if (this.checkLiveness) { - MP.printMessage(EC.TLC_CHECKING_TEMPORAL_PROPS, new String[] { "current", Long.toString(stateNum) }); - if (!liveCheck.check()) + if (!liveCheck.check(false)) return false; - nextLiveCheck = (stateNum <= 640000) ? stateNum * 2 : stateNum + 640000; } if (TLCGlobals.doCheckPoint()) { diff --git a/tlatools/src/tlc2/tool/liveness/AbstractDiskGraph.java b/tlatools/src/tlc2/tool/liveness/AbstractDiskGraph.java index 7eea7644373f8d157d83935c1c479154e690dbd2..b2865fbd0a95d58389e5a29af446c35719fd8e45 100644 --- a/tlatools/src/tlc2/tool/liveness/AbstractDiskGraph.java +++ b/tlatools/src/tlc2/tool/liveness/AbstractDiskGraph.java @@ -84,6 +84,8 @@ public abstract class AbstractDiskGraph { private final IBucketStatistics outDegreeGraphStats; + private long sizeAtCheck = 1; // initialize with 1 to avoid div by zero + public AbstractDiskGraph(String metadir, int soln, IBucketStatistics graphStats) throws IOException { this.metadir = metadir; this.outDegreeGraphStats = graphStats; @@ -259,6 +261,15 @@ public abstract class AbstractDiskGraph { */ public abstract long size(); + + public long getSizeAtLastCheck() { + return sizeAtCheck; + } + + public void recordSize() { + this.sizeAtCheck = size(); + } + /** * Only useful for debugging. * @@ -393,12 +404,10 @@ public abstract class AbstractDiskGraph { tidx = nodeRAF.readInt(); } - @Override public String toString() { return "NodeRAFRecord [fp=" + fp + ", tidx=" + tidx + "]"; } - @Override public int hashCode() { final int prime = 31; int result = 1; @@ -408,7 +417,6 @@ public abstract class AbstractDiskGraph { return result; } - @Override public boolean equals(Object obj) { if (this == obj) return true; diff --git a/tlatools/src/tlc2/tool/liveness/ILiveCheck.java b/tlatools/src/tlc2/tool/liveness/ILiveCheck.java index 3284edf928beb1ed8f68ed62b0335473456c97e5..171a00672f42ed8b829429dc06ea9a16959de998 100644 --- a/tlatools/src/tlc2/tool/liveness/ILiveCheck.java +++ b/tlatools/src/tlc2/tool/liveness/ILiveCheck.java @@ -23,10 +23,17 @@ public interface ILiveCheck { void addNextState(TLCState s0, long fp0, StateVec nextStates, LongVec nextFPs) throws IOException; /** - * Check liveness properties for the current partial state graph. Returns + * Check liveness properties for the current (potentially partial) state graph. Returns * true iff it finds no errors. + * + * @param forceCheck + * Always checks liveness if true, otherwise heuristics about the + * partial graph are taken into account if it is worthwhile to + * check liveness. + * @return true iff it finds no errors or if liveness has not been checked + * on the partial graph because it was deemed worthless. */ - boolean check() throws Exception; + boolean check(boolean forceCheck) throws Exception; /** * No states can be added with add*State once finalCheck has been called. diff --git a/tlatools/src/tlc2/tool/liveness/LiveCheck.java b/tlatools/src/tlc2/tool/liveness/LiveCheck.java index 5b2d866e848c7bfd9a72e16ca2ad2c483013105d..4aa5c699bbbef22f729027b8c661c26bd6daad1c 100644 --- a/tlatools/src/tlc2/tool/liveness/LiveCheck.java +++ b/tlatools/src/tlc2/tool/liveness/LiveCheck.java @@ -93,10 +93,31 @@ public class LiveCheck implements ILiveCheck { } /* (non-Javadoc) - * @see tlc2.tool.liveness.ILiveCheck#check() + * @see tlc2.tool.liveness.ILiveCheck#check(boolean) */ - public boolean check() throws Exception { - return check(false); + public boolean check(boolean forceCheck) throws Exception { + if (forceCheck) { + return check0(false); + } + for (int i = 0; i < checker.length; i++) { + // If anyone of the disk graphs has increased by the given + // percentage, run liveness checking. This is the best heuristic I + // can come up with quickly. + // + // TODO Alternatively the level could be taken + // into account. Unless the level (height) of the graph increases, + // no new cycle won't be found anyway. All other aspects of liveness + // checking are checked as part of regular safety checking. + final AbstractDiskGraph diskGraph = checker[i].getDiskGraph(); + final long sizeAtLastCheck = diskGraph.getSizeAtLastCheck(); + final long sizeCurrently = diskGraph.size(); + final double delta = (sizeCurrently - sizeAtLastCheck) / (sizeAtLastCheck * 1.d); + if (delta > TLCGlobals.livenessThreshold) { + return check0(false); + } + } + + return true; } /* (non-Javadoc) @@ -105,10 +126,23 @@ public class LiveCheck implements ILiveCheck { public boolean finalCheck() throws InterruptedException, IOException { // Do *not* re-create the nodePtrTable after the check which takes a // while for larger disk graphs. - return check(true); + return check0(true); } - private boolean check(final boolean finalCheck) throws InterruptedException, IOException { + /** + * @param finalCheck + * If the internal nodePtrTbl should be restored for a subsequent + * liveness check. If this is the final/last check, it's pointless + * to re-create the nodePtrTable. + */ + private boolean check0(final boolean finalCheck) throws InterruptedException, IOException { + long sum = 0L; + for (int i = 0; i < checker.length; i++) { + sum += checker[i].getDiskGraph().size(); + } + MP.printMessage(EC.TLC_CHECKING_TEMPORAL_PROPS, + new String[] { "current", Long.toString(sum) }); + // Copy the array of checkers into a concurrent-enabled queue // that allows LiveWorker threads to easily get the next // LiveChecker to work on. We don't really need the FIFO @@ -133,7 +167,7 @@ public class LiveCheck implements ILiveCheck { LiveWorker worker = new LiveWorker(0, this, queue); worker.run(); } else { - LiveWorker[] workers = new LiveWorker[wNum]; + final LiveWorker[] workers = new LiveWorker[wNum]; for (int i = 0; i < wNum; i++) { workers[i] = new LiveWorker(i, this, queue); workers[i].start(); @@ -192,7 +226,8 @@ public class LiveCheck implements ILiveCheck { final TLCState lastState = stateTrace.elementAt(stateTrace.size() - 1); addNextState(lastState, lastState.fingerPrint(), new StateVec(0), new LongVec(0)); - if (!finalCheck()) { //HACK Calling finalCheck here to prevent code from re-creating the nodeptrtable from a non existant file. + // Do *not* re-create the nodePtrTbl when it is thrown away anyway. + if (!check0(true)) { throw new LiveException(); } diff --git a/tlatools/src/tlc2/tool/liveness/LiveCheck1.java b/tlatools/src/tlc2/tool/liveness/LiveCheck1.java index ac8772513c9c5e7baa2a3ba09e7a949280c4693e..d09308dc91ab06ba25f5c6faa7d55649b96854d0 100644 --- a/tlatools/src/tlc2/tool/liveness/LiveCheck1.java +++ b/tlatools/src/tlc2/tool/liveness/LiveCheck1.java @@ -442,7 +442,7 @@ public class LiveCheck1 implements ILiveCheck { * "bad" cycle. A "bad" cycle gives rise to a violation of liveness * property. */ - public synchronized boolean check() { + public synchronized boolean check(boolean forceCheck) { int slen = solutions.length; if (slen == 0) { return true; @@ -910,7 +910,7 @@ public class LiveCheck1 implements ILiveCheck { * @see tlc2.tool.liveness.ILiveCheck#finalCheck() */ public boolean finalCheck() throws Exception { - return check(); + return check(true); } /* (non-Javadoc) diff --git a/tlatools/src/tlc2/tool/liveness/LiveWorker.java b/tlatools/src/tlc2/tool/liveness/LiveWorker.java index 27589913625aac0d7be16ac756a7662381a76d27..00dffb898622c0ae567a23fb182cea525eb68901 100644 --- a/tlatools/src/tlc2/tool/liveness/LiveWorker.java +++ b/tlatools/src/tlc2/tool/liveness/LiveWorker.java @@ -700,6 +700,10 @@ public class LiveWorker extends IdThread { } } this.dg.destroyCache(); + // Record the size of the disk graph at the time its checked. This + // information is later used to decide if it it makes sense to + // run the next check on the larger but still *partial* graph. + this.dg.recordSize(); } } catch (Exception e) { MP.printError(EC.GENERAL, "checking liveness", e); // LL changed diff --git a/tlatools/src/tlc2/tool/liveness/NoOpLiveCheck.java b/tlatools/src/tlc2/tool/liveness/NoOpLiveCheck.java index 9e4d05c0f9972ecbbd6ca4db0642fab5c6fc4fac..5466402f300ba70f4faf0ad69f290186d745f80c 100644 --- a/tlatools/src/tlc2/tool/liveness/NoOpLiveCheck.java +++ b/tlatools/src/tlc2/tool/liveness/NoOpLiveCheck.java @@ -60,9 +60,9 @@ public class NoOpLiveCheck implements ILiveCheck { } /* (non-Javadoc) - * @see tlc2.tool.liveness.ILiveCheck#check() + * @see tlc2.tool.liveness.ILiveCheck#check(boolean) */ - public boolean check() throws Exception { + public boolean check(boolean forceCheck) throws Exception { return true; } diff --git a/tlatools/test-long/tlc2/tool/liveness/MultiThreadedSpecTest.java b/tlatools/test-long/tlc2/tool/liveness/MultiThreadedSpecTest.java index f8cc0af6a178a955ea4e401a05867256e82361f4..f2e0f4dcf5db43857d0b3340afadda9b23bfae0a 100644 --- a/tlatools/test-long/tlc2/tool/liveness/MultiThreadedSpecTest.java +++ b/tlatools/test-long/tlc2/tool/liveness/MultiThreadedSpecTest.java @@ -36,8 +36,8 @@ import java.util.concurrent.CountDownLatch; import java.util.concurrent.TimeUnit; import java.util.concurrent.TimeoutException; +import tlc2.TLCGlobals; import tlc2.output.EC; -import tlc2.tool.AbstractChecker; import tlc2.tool.WorkerMonitor; /** @@ -129,12 +129,12 @@ public abstract class MultiThreadedSpecTest extends ModelCheckerTestCase { } public void setUp() { - // Set the number of states before TLC (periodically) checks liveness to - // the largest possible value. This essentially stops TLC for checking + // Set the threshold before TLC (periodically) checks liveness to + // the largest possible value. This essentially stops TLC from checking // liveness during model checking and delays it until the end when one // final liveness check is run. We only then get deterministic behavior // needed by this test to e.g. check the number of states generated... - System.setProperty(AbstractChecker.NEXT_LIVECHECK, Long.toString(Long.MAX_VALUE)); + TLCGlobals.livenessThreshold = Double.MAX_VALUE; final ThreadMXBean threadBean = ManagementFactory.getThreadMXBean(); // Enable contention thread statistics to have the JVM measure