diff --git a/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/engine/main/RVPredict.java b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/engine/main/RVPredict.java index e013996e98..b0d1b2bae0 100644 --- a/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/engine/main/RVPredict.java +++ b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/engine/main/RVPredict.java @@ -32,6 +32,7 @@ import static com.runtimeverification.rvpredict.config.Configuration.RV_PREDICT_JAR; import java.io.IOException; +import java.time.Clock; import java.util.ArrayList; import java.util.Collections; import java.util.List; @@ -40,6 +41,10 @@ import com.runtimeverification.rvpredict.log.ILoggingEngine; import com.runtimeverification.rvpredict.metadata.CompactMetadata; import com.runtimeverification.rvpredict.metadata.Metadata; +import com.runtimeverification.rvpredict.progressindicator.ConsoleOneLineProgressIndicatorUI; +import com.runtimeverification.rvpredict.progressindicator.ProgressIndicator; +import com.runtimeverification.rvpredict.progressindicator.ProgressTimerThread; +import com.runtimeverification.rvpredict.trace.JavaTraceCache; import com.runtimeverification.rvpredict.trace.LLVMCompactTraceCache; import com.runtimeverification.rvpredict.trace.LLVMTraceCache; import com.runtimeverification.rvpredict.trace.Trace; @@ -67,7 +72,8 @@ public RVPredict(Configuration config) { traceCache = new LLVMTraceCache(config, Metadata.singleton()); } } else { - traceCache = new TraceCache(config, Metadata.readFrom(config.getMetadataPath(), config.isCompactTrace())); + traceCache = new JavaTraceCache( + config, Metadata.readFrom(config.getMetadataPath(), config.isCompactTrace())); } this.detector = new RaceDetector(config); } @@ -75,23 +81,33 @@ public RVPredict(Configuration config) { public void start() { try { traceCache.setup(); - // process the trace window by window - Trace trace; - while (true) { - if ((trace = traceCache.getTraceWindow()) != null) { - detector.run(trace); - } else { - break; + ProgressIndicator progressIndicator = new ProgressIndicator( + traceCache.getFileSize(), + config.solver_timeout, + new ConsoleOneLineProgressIndicatorUI(), + Clock.systemDefaultZone()); + try (ProgressTimerThread ignored = new ProgressTimerThread(progressIndicator)) { + // process the trace window by window + Trace trace; + while (true) { + if ((trace = traceCache.getTraceWindow()) != null) { + detector.run(trace, progressIndicator); + progressIndicator.endWindow(traceCache.getTotalRead()); + } else { + break; + } } - } + progressIndicator.end(); + System.out.println(); - List reports = detector.getRaceReports(); - if (reports.isEmpty()) { - config.logger().report("No races found.", Logger.MSGTYPE.INFO); - } else { - reports.forEach(r -> config.logger().report(r, Logger.MSGTYPE.REAL)); + List reports = detector.getRaceReports(); + if (reports.isEmpty()) { + config.logger().report("No races found.", Logger.MSGTYPE.INFO); + } else { + reports.forEach(r -> config.logger().report(r, Logger.MSGTYPE.REAL)); + } + traceCache.getLockGraph().runDeadlockDetection(); } - traceCache.getLockGraph().runDeadlockDetection(); } catch (IOException e) { System.err.println("Error: I/O error during prediction."); System.err.println(e.getMessage()); diff --git a/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/engine/main/RaceDetector.java b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/engine/main/RaceDetector.java index 505e48b05a..5aa36892a2 100644 --- a/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/engine/main/RaceDetector.java +++ b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/engine/main/RaceDetector.java @@ -12,12 +12,29 @@ import com.microsoft.z3.Params; import com.microsoft.z3.Z3Exception; import com.runtimeverification.rvpredict.config.Configuration; +import com.runtimeverification.rvpredict.progressindicator.ProgressIndicatorInterface; import com.runtimeverification.rvpredict.smt.MaximalCausalModel; import com.runtimeverification.rvpredict.smt.visitors.Z3Filter; import com.runtimeverification.rvpredict.trace.Trace; import com.runtimeverification.rvpredict.util.Constants; import com.runtimeverification.rvpredict.violation.Race; +import java.io.BufferedInputStream; +import java.io.BufferedOutputStream; +import java.io.File; +import java.io.FileOutputStream; +import java.io.IOException; +import java.io.InputStream; +import java.lang.reflect.Field; +import java.nio.file.Files; +import java.nio.file.Path; +import java.nio.file.Paths; +import java.nio.file.StandardCopyOption; +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Map; + /** * Detects data races from a given {@link Trace} object. * @@ -107,7 +124,7 @@ private Map> computeUnknownRaceSuspects(Trace trace) { return sigToRaceCandidates; } - public void run(Trace trace) { + public void run(Trace trace, ProgressIndicatorInterface progressIndicator) { if (!trace.mayContainRaces()) { return; } @@ -119,7 +136,7 @@ public void run(Trace trace) { Map result = MaximalCausalModel.create( - trace, z3filter, soundSolver, fastSolver, config.detectInterruptedThreadRace()) + trace, z3filter, soundSolver, fastSolver, progressIndicator, config.detectInterruptedThreadRace()) .checkRaceSuspects(sigToRaceSuspects); sigToRealRace.putAll(result); result.forEach((sig, race) -> { @@ -129,7 +146,7 @@ public void run(Trace trace) { }); } - public static String getNativeLibraryPath() { + private static String getNativeLibraryPath() { String nativePath = "/native"; Configuration.OS os = Configuration.OS.current(); String property = System.getProperty("os.arch"); @@ -147,7 +164,7 @@ public static String getNativeLibraryPath() { return nativePath; } - public static String getNativeLibraryName() { + private static String getNativeLibraryName() { Configuration.OS os = Configuration.OS.current(); switch (os) { case OSX: diff --git a/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/log/EventReader.java b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/log/EventReader.java index 6b19116cf9..8684fb6a78 100644 --- a/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/log/EventReader.java +++ b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/log/EventReader.java @@ -18,12 +18,15 @@ public class EventReader implements IEventReader { private final LZ4BlockInputStream in; + private final long fileSize; + private final ByteBuffer byteBuffer = ByteBuffer.allocate(Event.SIZEOF); private Event lastReadEvent; public EventReader(Path path) throws IOException { in = LZ4Utils.createDecompressionStream(path); + fileSize = in.available(); readEvent(); } @@ -56,6 +59,11 @@ public ReadonlyEventInterface lastReadEvent() { return lastReadEvent; } + @Override + public long bytesRead() throws IOException { + return fileSize - in.available(); + } + @Override public void close() throws IOException { in.close(); diff --git a/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/log/IEventReader.java b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/log/IEventReader.java index 6870d6fd5c..4e749c17ab 100644 --- a/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/log/IEventReader.java +++ b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/log/IEventReader.java @@ -12,5 +12,7 @@ public interface IEventReader extends Closeable { ReadonlyEventInterface readEvent() throws IOException; - public ReadonlyEventInterface lastReadEvent(); -} \ No newline at end of file + ReadonlyEventInterface lastReadEvent(); + + long bytesRead() throws IOException; +} diff --git a/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/log/LLVMEventReader.java b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/log/LLVMEventReader.java index 39d92e6547..00bbe32466 100644 --- a/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/log/LLVMEventReader.java +++ b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/log/LLVMEventReader.java @@ -46,6 +46,11 @@ public ReadonlyEventInterface lastReadEvent() { return this.lastReadEvent; } + @Override + public long bytesRead() { + return in.bytesRead(); + } + @Override public void close() throws IOException { in.close(); diff --git a/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/log/VolatileLoggingEngine.java b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/log/VolatileLoggingEngine.java index 16883970c9..26b2306010 100644 --- a/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/log/VolatileLoggingEngine.java +++ b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/log/VolatileLoggingEngine.java @@ -39,6 +39,7 @@ import com.runtimeverification.rvpredict.config.Configuration; import com.runtimeverification.rvpredict.engine.main.RaceDetector; import com.runtimeverification.rvpredict.metadata.Metadata; +import com.runtimeverification.rvpredict.progressindicator.NullProgressIndicator; import com.runtimeverification.rvpredict.trace.RawTrace; import com.runtimeverification.rvpredict.trace.TraceState; import com.runtimeverification.rvpredict.util.Constants; @@ -210,7 +211,7 @@ protected void runRaceDetection(int numOfEvents) { if (rawTraces.size() == 1) { crntState.fastProcess(rawTraces.iterator().next()); } else { - detector.run(crntState.initNextTraceWindow(rawTraces)); + detector.run(crntState.initNextTraceWindow(rawTraces), new NullProgressIndicator()); } } catch (Throwable e) { config.logger().debug(e); @@ -244,7 +245,7 @@ public void log(EventType eventType, int locId, int addr1, int addr2, long value * However, the race detection thread only reads {@code cursor} after * blocking the GID counter and all on-going {@code finalizeEvents()} * finish, while the logging thread only writes to {@code cursor} after - * successfully acquiring GIDs and before incrementing the {@link finalized} + * successfully acquiring GIDs and before incrementing the {@link VolatileLoggingEngine#finalized} * counter. Therefore, it is impossible for the two threads to access * {@code cursor} concurrently. * diff --git a/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/log/compact/CompactEventReader.java b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/log/compact/CompactEventReader.java index 7834478e77..ff3c4aac70 100644 --- a/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/log/compact/CompactEventReader.java +++ b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/log/compact/CompactEventReader.java @@ -124,7 +124,7 @@ public static int getNumberOfValues() { public List read( Context context, CompactEventFactory compactEventFactory, - TraceHeader header, InputStream stream) + TraceHeader header, InputStreamByteCounterWrapper stream) throws InvalidTraceDataException, IOException { if (buffer == null) { buffer = new byte[reader.size(header)]; @@ -188,7 +188,7 @@ List readEvent( private TraceHeader header; private CompactEventFactory factory; private Context context; - private InputStream inputStream; + private InputStreamByteCounterWrapper inputStream; private ByteBuffer pcBuffer; private Address pc; private long minDeltaAndEventType; @@ -201,7 +201,7 @@ public CompactEventReader(Path path) throws IOException, InvalidTraceDataExcepti this(new BufferedInputStream(new FileInputStream(path.toFile()))); } public CompactEventReader(InputStream inputStream) throws IOException, InvalidTraceDataException { - this.inputStream = inputStream; + this.inputStream = new InputStreamByteCounterWrapper(inputStream); header = new TraceHeader(inputStream); pc = new Address(header); pcBuffer = ByteBuffer.allocate(pc.size()).order(header.getByteOrder()); @@ -287,9 +287,37 @@ public ReadonlyEventInterface lastReadEvent() { return events.get(currentEvent); } + @Override + public long bytesRead() throws IOException { + return inputStream.getBytesRead(); + } + @Override public void close() throws IOException { inputStream.close(); } + static class InputStreamByteCounterWrapper { + private final InputStream inputStream; + private long bytesRead; + + private InputStreamByteCounterWrapper(InputStream inputStream) { + this.inputStream = inputStream; + this.bytesRead = 0; + } + + private int read(byte[] buffer) throws IOException { + int count = inputStream.read(buffer); + bytesRead += count; + return count; + } + + private void close() throws IOException { + inputStream.close(); + } + + private long getBytesRead() { + return bytesRead; + } + } } diff --git a/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/progressindicator/ConsoleOneLineProgressIndicatorUI.java b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/progressindicator/ConsoleOneLineProgressIndicatorUI.java new file mode 100644 index 0000000000..784be14442 --- /dev/null +++ b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/progressindicator/ConsoleOneLineProgressIndicatorUI.java @@ -0,0 +1,24 @@ +package com.runtimeverification.rvpredict.progressindicator; + +import java.util.concurrent.TimeUnit; + +public class ConsoleOneLineProgressIndicatorUI implements ProgressIndicatorUI { + @Override + public void reportState( + OneItemProgress inputFile, + OneItemProgress races, + long racesFound, + OneItemProgress totalTasksProgress, + OneItemProgress smtTimeMillis) { + System.out.print(String.format( + "Input: %1$3d%%. Races found: %2$3d. Current input tasks: %3$3d%%. Time left: %4$2ss.\r", + inputFile.intPercentageDone(), + racesFound, + totalTasksProgress.intPercentageDone(), + TimeUnit.MILLISECONDS.toSeconds(smtTimeMillis.getTotal() - smtTimeMillis.getDone()))); + System.out.flush(); + } + public void reportEnd() { + System.out.println(); + } +} diff --git a/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/progressindicator/NullProgressIndicator.java b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/progressindicator/NullProgressIndicator.java new file mode 100644 index 0000000000..d5ef233c58 --- /dev/null +++ b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/progressindicator/NullProgressIndicator.java @@ -0,0 +1,33 @@ +package com.runtimeverification.rvpredict.progressindicator; + +import java.util.List; + +public class NullProgressIndicator implements ProgressIndicatorInterface { + @Override + public void startComputation(List raceCounts) { + } + + @Override + public void endWindow(long filePosition) { + } + + @Override + public void startRace(int raceIndex) { + } + + @Override + public void noRaceFound() { + } + + @Override + public void raceFound() { + } + + @Override + public void startRaceAttempt() { + } + + @Override + public void finishRaceAttempt() { + } +} diff --git a/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/progressindicator/OneItemProgress.java b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/progressindicator/OneItemProgress.java new file mode 100644 index 0000000000..1aafac0d2c --- /dev/null +++ b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/progressindicator/OneItemProgress.java @@ -0,0 +1,69 @@ +package com.runtimeverification.rvpredict.progressindicator; + +import com.google.common.annotations.VisibleForTesting; + +class OneItemProgress { + private final long total; + private final long done; + + OneItemProgress(long total) { + this.total = total; + this.done = 0; + } + + @VisibleForTesting + OneItemProgress(long total, long done) { + this.total = total; + this.done = done; + } + + OneItemProgress withTaskDone() { + assert done < total; + return new OneItemProgress(total, done + 1); + } + + OneItemProgress withProgress(long progress) { + long finalValue = this.done + progress; + assert finalValue <= total; + return new OneItemProgress(total, finalValue); + } + + OneItemProgress withProgressCapped(long progress) { + long finalValue = done + progress; + if (finalValue > total) { + finalValue = total; + } + return new OneItemProgress(total, finalValue); + } + + long getTotal() { + return total; + } + + long getDone() { + return done; + } + + int intPercentageDone() { + return Math.toIntExact(done * 100 / total); + } + + @Override + public int hashCode() { + return Long.hashCode(total) ^ Long.hashCode(done); + } + + @Override + public boolean equals(Object obj) { + if (!(obj instanceof OneItemProgress)) { + return false; + } + OneItemProgress other = (OneItemProgress) obj; + return total == other.total && done == other.done; + } + + @Override + public String toString() { + return "(" + done + " of " + total + ")"; + } +} diff --git a/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/progressindicator/ProgressIndicator.java b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/progressindicator/ProgressIndicator.java new file mode 100644 index 0000000000..b6ef3b9779 --- /dev/null +++ b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/progressindicator/ProgressIndicator.java @@ -0,0 +1,151 @@ +package com.runtimeverification.rvpredict.progressindicator; + +import com.google.common.collect.ImmutableList; + +import java.time.Clock; +import java.util.List; +import java.util.Optional; +import java.util.OptionalLong; +import java.util.concurrent.TimeUnit; + +public class ProgressIndicator implements ProgressIndicatorInterface { + private final ProgressIndicatorUI ui; + private final Clock clock; + private OneItemProgress smtTimeMillis; + private OneItemProgress inputFile; + private Optional maybeComputationData; + + private final class ComputationData { + private final ImmutableList raceCounts; + private OneItemProgress races; + private OneItemProgress totalTasksProgress; + private Optional maybeCurrentRace; + + private ComputationData(List raceCounts) { + this.raceCounts = ImmutableList.copyOf(raceCounts); + this.races = new OneItemProgress(this.raceCounts.size()); + this.totalTasksProgress = + new OneItemProgress(raceCounts.stream().mapToInt(counts -> counts).sum()); + this.maybeCurrentRace = Optional.of(new OneItemProgress(raceCounts.get(0))); + } + + private void startRace(int raceIndex) { + assert raceIndex == races.getDone(); + races = races.withProgress(raceIndex - races.getDone()); + maybeCurrentRace = Optional.of(new OneItemProgress(raceCounts.get(raceIndex))); + } + + private void raceEnd() { + races = races.withTaskDone(); + assert maybeCurrentRace.isPresent(); + OneItemProgress currentRace = maybeCurrentRace.get(); + long remainingTasks = currentRace.getTotal() - currentRace.getDone(); + currentRace.withProgress(remainingTasks); + totalTasksProgress = totalTasksProgress.withProgress(remainingTasks); + } + + private void finishRaceAttempt() { + totalTasksProgress = totalTasksProgress.withTaskDone(); + assert maybeCurrentRace.isPresent(); + OneItemProgress currentRace = maybeCurrentRace.get(); + maybeCurrentRace = Optional.of(currentRace.withTaskDone()); + } + } + + private long racesFound; + + private OptionalLong currentTaskUncountedTimeStart; + + public ProgressIndicator(long inputFileSize, int maximumSmtTimeSeconds, ProgressIndicatorUI ui, Clock clock) { + this.ui = ui; + this.clock = clock; + this.inputFile = new OneItemProgress(inputFileSize); + this.smtTimeMillis = + new OneItemProgress(TimeUnit.SECONDS.toMillis(maximumSmtTimeSeconds)); + this.currentTaskUncountedTimeStart = OptionalLong.empty(); + this.racesFound = 0; + this.maybeComputationData = Optional.empty(); + } + + public synchronized void startComputation(List raceCounts) { + this.currentTaskUncountedTimeStart = OptionalLong.empty(); + this.maybeComputationData = Optional.of(new ComputationData(raceCounts)); + reportUiState(); + } + + public synchronized void end() { + reportUiState(); + ui.reportEnd(); + } + public synchronized void endWindow(long filePosition) { + inputFile = inputFile.withProgress(filePosition - inputFile.getDone()); + this.maybeComputationData = Optional.empty(); + } + + public synchronized void startRace(int raceIndex) { + assert maybeComputationData.isPresent(); + ComputationData computationData = maybeComputationData.get(); + computationData.startRace(raceIndex); + reportUiState(); + } + + public synchronized void noRaceFound() { + raceEnd(); + } + + public synchronized void raceFound() { + this.racesFound++; + raceEnd(); + } + + public synchronized void startRaceAttempt() { + currentTaskUncountedTimeStart = OptionalLong.of(clock.millis()); + reportUiState(); + } + + public synchronized void finishRaceAttempt() { + assert currentTaskUncountedTimeStart.isPresent(); + long currentTimeMillis = clock.millis(); + smtTimeMillis = smtTimeMillis.withProgressCapped( + currentTimeMillis - currentTaskUncountedTimeStart.orElse(currentTimeMillis)); + this.currentTaskUncountedTimeStart = OptionalLong.empty(); + + assert maybeComputationData.isPresent(); + ComputationData computationData = maybeComputationData.get(); + computationData.finishRaceAttempt(); + + reportUiState(); + } + + synchronized void timerTick() { + long currentTimeMillis = clock.millis(); + if (this.currentTaskUncountedTimeStart.isPresent()) { + smtTimeMillis = smtTimeMillis.withProgressCapped( + currentTimeMillis - currentTaskUncountedTimeStart.getAsLong()); + currentTaskUncountedTimeStart = OptionalLong.of(currentTimeMillis); + } + reportUiState(); + } + + private void raceEnd() { + assert maybeComputationData.isPresent(); + ComputationData computationData = maybeComputationData.get(); + computationData.raceEnd(); + + reportUiState(); + } + + private void reportUiState() { + Optional maybeComputationData = this.maybeComputationData; + if (!maybeComputationData.isPresent()) { + return; + } + ComputationData computationData = maybeComputationData.get(); + ui.reportState( + inputFile, + computationData.races, + racesFound, + computationData.totalTasksProgress, + smtTimeMillis); + } +} diff --git a/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/progressindicator/ProgressIndicatorInterface.java b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/progressindicator/ProgressIndicatorInterface.java new file mode 100644 index 0000000000..8117bf5843 --- /dev/null +++ b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/progressindicator/ProgressIndicatorInterface.java @@ -0,0 +1,13 @@ +package com.runtimeverification.rvpredict.progressindicator; + +import java.util.List; + +public interface ProgressIndicatorInterface { + void startComputation(List raceCounts); + void endWindow(long filePosition); + void startRace(int raceIndex); + void noRaceFound(); + void raceFound(); + void startRaceAttempt(); + void finishRaceAttempt(); +} diff --git a/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/progressindicator/ProgressIndicatorUI.java b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/progressindicator/ProgressIndicatorUI.java new file mode 100644 index 0000000000..5bd1cc7754 --- /dev/null +++ b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/progressindicator/ProgressIndicatorUI.java @@ -0,0 +1,11 @@ +package com.runtimeverification.rvpredict.progressindicator; + +interface ProgressIndicatorUI { + void reportState( + OneItemProgress inputFile, + OneItemProgress races, + long racesFound, + OneItemProgress totalTasksProgress, + OneItemProgress smtTimeMillis); + void reportEnd(); +} diff --git a/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/progressindicator/ProgressTimerThread.java b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/progressindicator/ProgressTimerThread.java new file mode 100644 index 0000000000..cc6818e445 --- /dev/null +++ b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/progressindicator/ProgressTimerThread.java @@ -0,0 +1,27 @@ +package com.runtimeverification.rvpredict.progressindicator; + +import java.util.Timer; +import java.util.TimerTask; + +public class ProgressTimerThread extends TimerTask implements AutoCloseable { + private final Timer timer; + private ProgressIndicator progressIndicator; + + + public ProgressTimerThread(ProgressIndicator progressIndicator) { + this.timer = new Timer("progress-timer", true); + this.progressIndicator = progressIndicator; + + this.timer.schedule(this, 100L, 100L); + } + + @Override + public void run() { + progressIndicator.timerTick(); + } + + @Override + public void close() { + this.timer.cancel(); + } +} diff --git a/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/smt/MaximalCausalModel.java b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/smt/MaximalCausalModel.java index 0704346642..cb7de6ce60 100644 --- a/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/smt/MaximalCausalModel.java +++ b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/smt/MaximalCausalModel.java @@ -1,4 +1,4 @@ -/******************************************************************************* +/* ****************************************************************************** * Copyright (c) 2013 University of Illinois * * All rights reserved. @@ -25,7 +25,7 @@ * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. - ******************************************************************************/ + * *****************************************************************************/ package com.runtimeverification.rvpredict.smt; import com.google.common.collect.ImmutableList; @@ -35,6 +35,7 @@ import com.microsoft.z3.Status; import com.runtimeverification.rvpredict.config.Configuration; import com.runtimeverification.rvpredict.log.ReadonlyEventInterface; +import com.runtimeverification.rvpredict.progressindicator.ProgressIndicatorInterface; import com.runtimeverification.rvpredict.smt.constraintsources.SignalStartMask; import com.runtimeverification.rvpredict.smt.formula.BoolFormula; import com.runtimeverification.rvpredict.smt.formula.BooleanConstant; @@ -108,24 +109,31 @@ public class MaximalCausalModel { private final com.microsoft.z3.Solver fastSolver; private final com.microsoft.z3.Solver soundSolver; + private final ProgressIndicatorInterface progressIndicator; + private final boolean detectInterruptedThreadRace; public static MaximalCausalModel create( - Trace trace, Z3Filter z3filter, Solver fastSolver, Solver soundSolver, boolean detectInterruptedThreadRace) { + Trace trace, Z3Filter z3filter, Solver fastSolver, Solver soundSolver, + ProgressIndicatorInterface progressIndicator, + boolean detectInterruptedThreadRace) { MaximalCausalModel model = new MaximalCausalModel( - trace, z3filter, fastSolver, soundSolver, detectInterruptedThreadRace); + trace, z3filter, fastSolver, soundSolver, progressIndicator, detectInterruptedThreadRace); model.addConstraints(); return model; } private MaximalCausalModel( - Trace trace, Z3Filter z3filter, Solver fastSolver, Solver soundSolver, boolean detectInterruptedThreadRace) { + Trace trace, Z3Filter z3filter, Solver fastSolver, Solver soundSolver, + ProgressIndicatorInterface progressIndicator, + boolean detectInterruptedThreadRace) { this.trace = trace; this.z3filter = z3filter; this.fastSolver = fastSolver; this.soundSolver = soundSolver; this.detectInterruptedThreadRace = detectInterruptedThreadRace; + this.progressIndicator = progressIndicator; trace.eventsByThreadID().forEach((tid, events) -> events.forEach(event -> nameToEvent.put(OrderVariable.get(event).toString(), event))); } @@ -371,6 +379,14 @@ public Map checkRaceSuspects(Map> sigToRaceSusp if (sigToRaceSuspects.isEmpty()) { return Collections.emptyMap(); } + ImmutableList>> orderedSigToRaceSuspects = + ImmutableList.copyOf(sigToRaceSuspects.entrySet()); + + this.progressIndicator.startComputation( + orderedSigToRaceSuspects.stream().map(entry -> entry.getValue().size()).collect(Collectors.toList())); + +// trace.logger().debug().println("start analyzing: " + trace.getBaseGID()); +// sigToRaceSuspects.forEach((sig, l) -> trace.logger().debug().println(sig + ": " + l.size())); Map result = new HashMap<>(); try { @@ -385,7 +401,10 @@ public Map checkRaceSuspects(Map> sigToRaceSusp /* check race suspects */ boolean atLeastOneRace = false; - for (Map.Entry> entry : sigToRaceSuspects.entrySet()) { + for (int i = 0; i < orderedSigToRaceSuspects.size(); i++) { + this.progressIndicator.startRace(i); + Map.Entry> entry = orderedSigToRaceSuspects.get(i); + boolean hadRace = false; for (Race race : entry.getValue()) { fastSolver.push(); fastSolver.add(z3filter.filter(suspectToAsst.get(race))); @@ -396,11 +415,12 @@ public Map checkRaceSuspects(Map> sigToRaceSusp isRace = soundSolver.check() == Status.SATISFIABLE; atLeastOneRace |= isRace; if (isRace) { + hadRace = true; Map> threadToExecution = extractExecution(soundSolver); Map signalParents = extractSignalParents(soundSolver); fillSignalStack(threadToExecution, signalParents, race); if (Configuration.debug) { - dumpOrderingWithLessThreadSwitches( + dumpOrdering( threadToExecution, Optional.of(race.firstEvent()), Optional.of(race.secondEvent()), signalParents); @@ -413,6 +433,13 @@ public Map checkRaceSuspects(Map> sigToRaceSusp result.put(entry.getKey(), race); break; } + this.progressIndicator.finishRaceAttempt(); + } + if (hadRace) { + atLeastOneRace = true; + this.progressIndicator.raceFound(); + } else { + this.progressIndicator.noRaceFound(); } } if (!atLeastOneRace && Configuration.debug) { @@ -506,7 +533,7 @@ private List computeSignalStack( private void findAndDumpOrdering(Solver solver) { solver.push(); if (solver.check() == Status.SATISFIABLE) { - dumpOrderingWithLessThreadSwitches( + dumpOrdering( extractExecution(solver), Optional.empty(), Optional.empty(), extractSignalParents(solver)); } solver.pop(); @@ -532,78 +559,6 @@ private Map> extractExecution(Solver solver) { } private void dumpOrdering( - Map> threadToExecution, - ReadonlyEventInterface firstRaceEvent, ReadonlyEventInterface secondRaceEvent, - Map signalParents) { - System.out.println("Possible ordering of events .........."); - Map lastIndexPerThread = new HashMap<>(); - threadToExecution.keySet().forEach(threadId -> lastIndexPerThread.put(threadId, 0)); - - long lastThread = ((long) Integer.MAX_VALUE) + 1; - boolean hasData; - do { - hasData = false; - long minOrder = Integer.MAX_VALUE; - int minIndex = Integer.MAX_VALUE; - int minThread = Integer.MAX_VALUE; - for (Map.Entry indexEntry : lastIndexPerThread.entrySet()) { - Integer threadId = indexEntry.getKey(); - Integer index = indexEntry.getValue(); - List execution = threadToExecution.get(threadId); - if (index >= execution.size()) { - continue; - } - EventWithOrder currentEvent = execution.get(index); - if (minOrder > currentEvent.getOrderId() - || (minOrder == currentEvent.getOrderId() && minThread == threadId)) { - minOrder = currentEvent.getOrderId(); - minIndex = index; - minThread = threadId; - hasData = true; - } - } - if (hasData) { - boolean foundRace = false; - EventWithOrder event = threadToExecution.get(minThread).get(minIndex); - lastIndexPerThread.put(minThread, minIndex + 1); - if (isRaceEvent(event, firstRaceEvent, secondRaceEvent)) { - for (Map.Entry indexEntry : lastIndexPerThread.entrySet()) { - Integer threadId = indexEntry.getKey(); - Integer index = indexEntry.getValue(); - List execution = threadToExecution.get(threadId); - if (index >= execution.size()) { - continue; - } - EventWithOrder currentEvent = execution.get(index); - if (currentEvent.getEvent().getEventId() != event.getEvent().getEventId() - && isRaceEvent(currentEvent, firstRaceEvent, secondRaceEvent)) { - foundRace = true; - lastIndexPerThread.put(threadId, index + 1); - System.out.println("-- Found race for threads " - + threadDescription(minThread, event, signalParents) + " and " - + threadDescription(threadId, currentEvent, signalParents) + " --"); - lastThread = Integer.MAX_VALUE; - System.out.println(prettyPrint(event.getEvent())); - System.out.println(" -- vs"); - System.out.println(prettyPrint(currentEvent.getEvent())); - break; - } - } - assert foundRace; - } - if (!foundRace) { - if (lastThread != minThread) { - System.out.println( - "-- Switching to thread " + threadDescription(minThread, event, signalParents) + " --"); - lastThread = minThread; - } - System.out.println(prettyPrint(event.getEvent())); - } - } - } while (hasData); - } - - private void dumpOrderingWithLessThreadSwitches( Map> threadToExecution, Optional firstRaceEvent, Optional secondRaceEvent, Map signalParents) { @@ -877,14 +832,6 @@ private String prettyPrint(ReadonlyEventInterface event) { return event.getType().getPrinter().print(event); } - private boolean isRaceEvent( - EventWithOrder event, - ReadonlyEventInterface firstRaceEvent, - ReadonlyEventInterface secondRaceEvent) { - return (firstRaceEvent != null && firstRaceEvent.getEventId() == event.getEvent().getEventId()) - || (secondRaceEvent != null && secondRaceEvent.getEventId() == event.getEvent().getEventId()); - } - private String threadDescription(int threadId, EventWithOrder event, Map signalParents) { if (trace.getThreadType(threadId) == ThreadType.THREAD) { return "T" + event.getEvent().getOriginalThreadId(); @@ -921,7 +868,7 @@ private String getInterruptionDescription(int threadId, Map si private void checkTraceConsistency(Z3Filter z3filter, com.microsoft.z3.Solver solver) throws Exception { List blks = new ArrayList<>(); - trace.memoryAccessBlocksByThreadID().values().forEach(l -> blks.addAll(l)); + trace.memoryAccessBlocksByThreadID().values().forEach(blks::addAll); Collections.sort(blks); solver.push(); diff --git a/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/trace/BinaryParser.java b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/trace/BinaryParser.java index 6d2f990a4f..83b12dac5e 100644 --- a/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/trace/BinaryParser.java +++ b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/trace/BinaryParser.java @@ -21,10 +21,12 @@ public class BinaryParser implements Closeable { private final ByteBuffer byteBuffer = ByteBuffer.allocate(8).order(ByteOrder.nativeOrder()); - private BufferedInputStream in; + private final BufferedInputStream in; + private long bytesRead; - public BinaryParser(File file) throws IOException { + BinaryParser(File file) throws IOException { in = new BufferedInputStream(new FileInputStream(file)); + bytesRead = 0; } public BinaryParser(Path path) throws IOException { @@ -36,10 +38,11 @@ public final int readByte() throws IOException { if(rd == -1) { throw new EOFException(); } + bytesRead++; return rd; } - private final void putBytes(int n) throws IOException { + private void putBytes(int n) throws IOException { for(int i = 0; i < n; ++i) { byteBuffer.put((byte)readByte()); } @@ -60,7 +63,7 @@ public final Integer readInt() throws IOException { return ret; } - public final String readString() throws IOException { + final String readString() throws IOException { StringBuilder sb = new StringBuilder(); int rd = readByte(); @@ -77,4 +80,8 @@ public final String readString() throws IOException { public void close() throws IOException { in.close(); } + + public long bytesRead() { + return bytesRead; + } } diff --git a/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/trace/JavaTraceCache.java b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/trace/JavaTraceCache.java new file mode 100644 index 0000000000..41fe655d5f --- /dev/null +++ b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/trace/JavaTraceCache.java @@ -0,0 +1,52 @@ +package com.runtimeverification.rvpredict.trace; + +import com.runtimeverification.rvpredict.config.Configuration; +import com.runtimeverification.rvpredict.log.EventReader; +import com.runtimeverification.rvpredict.log.compact.CompactEventReader; +import com.runtimeverification.rvpredict.log.compact.InvalidTraceDataException; +import com.runtimeverification.rvpredict.metadata.MetadataInterface; + +import java.io.IOException; +import java.nio.file.Path; +import java.util.OptionalLong; + +public class JavaTraceCache extends TraceCache { + private OptionalLong fileSize; + + public JavaTraceCache(Configuration config, MetadataInterface metadata) { + super(config, metadata); + fileSize = OptionalLong.empty(); + } + + @Override + public void setup() throws IOException { + int logFileId = 0; + if (config.isCompactTrace()) { + try { + Path path = config.getCompactTraceFilePath(); + readers.add(new CompactEventReader(path)); + fileSize = OptionalLong.of(path.toFile().length()); + } catch (InvalidTraceDataException e) { + throw new IOException(e); + } + return; + } + long size = 0; + while (true) { + Path path = config.getTraceFilePath(logFileId++); + if (!path.toFile().exists()) { + break; + } + size += path.toFile().length(); + readers.add(new EventReader(path)); + } + fileSize = OptionalLong.of(size); + } + + @Override + public long getFileSize() { + assert fileSize.isPresent(); + return fileSize.getAsLong(); + } + +} diff --git a/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/trace/LLVMCompactTraceCache.java b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/trace/LLVMCompactTraceCache.java index b09169c9b0..5460ba791e 100644 --- a/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/trace/LLVMCompactTraceCache.java +++ b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/trace/LLVMCompactTraceCache.java @@ -5,20 +5,29 @@ import com.runtimeverification.rvpredict.log.compact.InvalidTraceDataException; import com.runtimeverification.rvpredict.metadata.CompactMetadata; -import java.io.EOFException; import java.io.IOException; +import java.util.OptionalLong; public class LLVMCompactTraceCache extends TraceCache { + private OptionalLong fileSize; public LLVMCompactTraceCache(Configuration config, CompactMetadata metadata) { super(config, metadata); + fileSize = OptionalLong.empty(); } @Override public void setup() throws IOException { try { readers.add(new CompactEventReader(config.getCompactTraceFilePath())); + fileSize = OptionalLong.of(config.getCompactTraceFilePath().toFile().length()); } catch (InvalidTraceDataException e) { throw new IOException(e); } } + + @Override + public long getFileSize() { + assert fileSize.isPresent(); + return fileSize.getAsLong(); + } } diff --git a/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/trace/LLVMTraceCache.java b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/trace/LLVMTraceCache.java index cdccff4672..bb54948d9f 100644 --- a/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/trace/LLVMTraceCache.java +++ b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/trace/LLVMTraceCache.java @@ -2,14 +2,13 @@ import com.runtimeverification.rvpredict.config.Configuration; import com.runtimeverification.rvpredict.log.LLVMEventReader; -import com.runtimeverification.rvpredict.log.compact.CompactEventReader; -import com.runtimeverification.rvpredict.log.compact.InvalidTraceDataException; import com.runtimeverification.rvpredict.metadata.Metadata; import com.runtimeverification.rvpredict.util.Logger; -import java.io.*; +import java.io.EOFException; +import java.io.IOException; import java.nio.file.Path; -import java.util.Arrays; +import java.util.OptionalLong; /** * Class reading the trace from an LLVM execution debug log. @@ -18,6 +17,7 @@ */ public class LLVMTraceCache extends TraceCache { private final Metadata metadata; + private OptionalLong fileSize; public LLVMTraceCache(Configuration config, Metadata metadata) { super(config, metadata); @@ -25,7 +25,7 @@ public LLVMTraceCache(Configuration config, Metadata metadata) { } private interface MetadataLogger { - public void log(Object[] args); + void log(Object[] args); } private class BinaryReader { @@ -51,34 +51,17 @@ private void parseInfo(MetadataLogger logger, BinaryReader reader, String prefix } private void parseVarInfo() throws IOException { - parseInfo(new MetadataLogger() { - @Override - public void log(Object[] args) { - metadata.setVariableSig((Integer)args[0], (String)args[1]); - } - }, new BinaryReader() { + parseInfo(args -> metadata.setVariableSig((Integer)args[0], (String)args[1]), new BinaryReader() { }, "var"); } private void parseLocInfo() throws IOException { - parseInfo(new MetadataLogger() { - @Override - public void log(Object[] args) { - metadata.setLocationSig((Integer)args[0], (String)args[1]); - } - }, new BinaryReader() + parseInfo(args -> metadata.setLocationSig((Integer)args[0], (String)args[1]), new BinaryReader() , "loc"); } private void parseThdInfo() throws IOException { - parseInfo(new MetadataLogger() { - - @Override - public void log(Object[] args) { - metadata.addOriginalThreadCreationInfo((long)args[0], (long)args[1], (int)args[2]); - - } - }, new BinaryReader() { + parseInfo(args -> metadata.addOriginalThreadCreationInfo((long)args[0], (long)args[1], (int)args[2]), new BinaryReader() { @Override public Object[] read(BinaryParser in) throws IOException { @@ -95,7 +78,7 @@ private void readMetadata() throws IOException { try { parseVarInfo(); } catch (Metadata.TooManyVariables e) { - config.logger().report("Maximum number of variables allowed (" + metadata.MAX_NUM_OF_VARIABLES + + config.logger().report("Maximum number of variables allowed (" + Metadata.MAX_NUM_OF_VARIABLES + ") exceeded.", Logger.MSGTYPE.ERROR); } parseLocInfo(); @@ -107,10 +90,19 @@ public void setup() throws IOException { readMetadata(); int logId = 0; Path path = config.getTraceFilePath(logId); + long size = 0; while(path.toFile().exists()) { + size += path.toFile().length(); readers.add(new LLVMEventReader(path)); ++logId; path = config.getTraceFilePath(logId); } + fileSize = OptionalLong.of(size); + } + + @Override + public long getFileSize() { + assert fileSize.isPresent(); + return fileSize.getAsLong(); } } diff --git a/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/trace/TestTraceCache.java b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/trace/TestTraceCache.java new file mode 100644 index 0000000000..9e27ab868b --- /dev/null +++ b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/trace/TestTraceCache.java @@ -0,0 +1,33 @@ +package com.runtimeverification.rvpredict.trace; + +import com.google.common.annotations.VisibleForTesting; +import com.runtimeverification.rvpredict.config.Configuration; +import com.runtimeverification.rvpredict.engine.deadlock.LockGraph; +import com.runtimeverification.rvpredict.log.IEventReader; + +import java.io.IOException; +import java.util.List; + +@VisibleForTesting +public class TestTraceCache extends TraceCache { + private TestTraceCache( + Configuration config, TraceState traceState, LockGraph lockGraph, List defaultReaders) { + super(config, traceState, lockGraph, defaultReaders); + } + + @VisibleForTesting + static TraceCache createForTesting( + Configuration config, TraceState traceState, LockGraph lockGraph, List readers) { + return new TestTraceCache(config, traceState, lockGraph, readers); + } + + @Override + public void setup() throws IOException { + + } + + @Override + public long getFileSize() { + return 0; + } +} diff --git a/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/trace/TraceCache.java b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/trace/TraceCache.java index faf845aef3..ca33d4dbf1 100644 --- a/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/trace/TraceCache.java +++ b/rv-predict-source/src/main/java/com/runtimeverification/rvpredict/trace/TraceCache.java @@ -3,17 +3,13 @@ import com.google.common.annotations.VisibleForTesting; import com.runtimeverification.rvpredict.config.Configuration; import com.runtimeverification.rvpredict.engine.deadlock.LockGraph; -import com.runtimeverification.rvpredict.log.EventReader; import com.runtimeverification.rvpredict.log.EventType; import com.runtimeverification.rvpredict.log.IEventReader; import com.runtimeverification.rvpredict.log.ReadonlyEventInterface; -import com.runtimeverification.rvpredict.log.compact.CompactEventReader; -import com.runtimeverification.rvpredict.log.compact.InvalidTraceDataException; import com.runtimeverification.rvpredict.metadata.MetadataInterface; import java.io.EOFException; import java.io.IOException; -import java.nio.file.Path; import java.util.ArrayList; import java.util.Collections; import java.util.Iterator; @@ -27,7 +23,7 @@ * @author TraianSF * @author YilongL */ -public class TraceCache { +public abstract class TraceCache { private final LockGraph lockGraph; @@ -35,7 +31,7 @@ public class TraceCache { private final TraceState crntState; - protected long lastGID = 0; + private long lastGID = 0; protected final int capacity; private final ArrayList eventsBuffer; @@ -44,11 +40,12 @@ public class TraceCache { /** * Creates a new {@code TraceCache} structure for a trace log. */ - public TraceCache(Configuration config, MetadataInterface metadata) { + TraceCache(Configuration config, MetadataInterface metadata) { this(config, new TraceState(config, metadata), new LockGraph(config, metadata), Collections.emptyList()); } - private TraceCache( + @VisibleForTesting + TraceCache( Configuration config, TraceState traceState, LockGraph lockGraph, List defaultReaders) { this.config = config; this.crntState = traceState; @@ -62,30 +59,8 @@ private TraceCache( eventsBuffer = new ArrayList<>(capacity); } - @VisibleForTesting - static TraceCache createForTesting( - Configuration config, TraceState traceState, LockGraph lockGraph, List readers) { - return new TraceCache(config, traceState, lockGraph, readers); - } - - public void setup() throws IOException { - int logFileId = 0; - if (config.isCompactTrace()) { - try { - readers.add(new CompactEventReader(config.getCompactTraceFilePath())); - } catch (InvalidTraceDataException e) { - throw new IOException(e); - } - return; - } - while (true) { - Path path = config.getTraceFilePath(logFileId++); - if (!path.toFile().exists()) { - break; - } - readers.add(new EventReader(path)); - } - } + public abstract void setup() throws IOException; + public abstract long getFileSize(); public LockGraph getLockGraph() { return lockGraph; @@ -94,11 +69,11 @@ public LockGraph getLockGraph() { /** * Returns the power of two that is greater than the given integer. */ - protected static final int getNextPowerOfTwo(int x) { + private static int getNextPowerOfTwo(int x) { return 1 << (32 - Integer.numberOfLeadingZeros(x)); } - protected final List readEventWindow() throws IOException { + private List readEventWindow() throws IOException { List rawTraces = new ArrayList<>(); final int maxEvents = config.windowSize; if (Configuration.debug) @@ -270,4 +245,12 @@ public Trace getTraceWindow() throws IOException { /* finish reading events and create the Trace object */ return rawTraces.isEmpty() ? null : crntState.initNextTraceWindow(rawTraces); } + + public long getTotalRead() throws IOException { + long bytesRead = 0; + for (IEventReader reader : readers) { + bytesRead += reader.bytesRead(); + } + return bytesRead; + } } diff --git a/rv-predict-source/src/test/java/com/runtimeverification/rvpredict/progressindicator/OneItemProgressTest.java b/rv-predict-source/src/test/java/com/runtimeverification/rvpredict/progressindicator/OneItemProgressTest.java new file mode 100644 index 0000000000..83c8a39a29 --- /dev/null +++ b/rv-predict-source/src/test/java/com/runtimeverification/rvpredict/progressindicator/OneItemProgressTest.java @@ -0,0 +1,45 @@ +package com.runtimeverification.rvpredict.progressindicator; + +import com.runtimeverification.rvpredict.testutils.MoreAsserts; +import org.junit.Assert; +import org.junit.Test; + +public class OneItemProgressTest { + @Test + public void returnsGivenValues() { + OneItemProgress progress = new OneItemProgress(5); + Assert.assertEquals(5, progress.getTotal()); + Assert.assertEquals(0, progress.getDone()); + } + + @Test + public void oneTaskDoneIncrementsDone() { + OneItemProgress progress = new OneItemProgress(5).withTaskDone(); + Assert.assertEquals(5, progress.getTotal()); + Assert.assertEquals(1, progress.getDone()); + } + + @Test + public void recordsProgress() { + OneItemProgress progress = new OneItemProgress(5).withProgress(3); + Assert.assertEquals(5, progress.getTotal()); + Assert.assertEquals(3, progress.getDone()); + } + + @Test + public void capsProgressWhenAsked() { + OneItemProgress progress = new OneItemProgress(5).withProgressCapped(7); + Assert.assertEquals(5, progress.getTotal()); + Assert.assertEquals(5, progress.getDone()); + } + + @Test + public void throwsExceptionWhenProgressingTooMuch() { + MoreAsserts.assertException(() -> new OneItemProgress(5).withProgress(7)); + } + + @Test + public void computesPercentageDone() { + Assert.assertEquals(60, new OneItemProgress(5).withProgress(3).intPercentageDone()); + } +} diff --git a/rv-predict-source/src/test/java/com/runtimeverification/rvpredict/progressindicator/ProgressIndicatorTest.java b/rv-predict-source/src/test/java/com/runtimeverification/rvpredict/progressindicator/ProgressIndicatorTest.java new file mode 100644 index 0000000000..e04367ba52 --- /dev/null +++ b/rv-predict-source/src/test/java/com/runtimeverification/rvpredict/progressindicator/ProgressIndicatorTest.java @@ -0,0 +1,543 @@ +package com.runtimeverification.rvpredict.progressindicator; + +import org.junit.Test; +import org.junit.runner.RunWith; +import org.mockito.Mock; +import org.mockito.runners.MockitoJUnitRunner; + +import java.time.Clock; +import java.util.Arrays; +import java.util.Collections; + +import static org.mockito.Matchers.any; +import static org.mockito.Matchers.anyLong; +import static org.mockito.Matchers.eq; +import static org.mockito.Mockito.never; +import static org.mockito.Mockito.times; +import static org.mockito.Mockito.verify; +import static org.mockito.Mockito.when; + +@RunWith(MockitoJUnitRunner.class) +public class ProgressIndicatorTest { + @Mock private ProgressIndicatorUI mockProgressIndicatorUI; + @Mock private Clock mockClock; + + @Test + public void noUiCallsIfThereIsNoDataToShow() { + ProgressIndicator progressIndicator = new ProgressIndicator( + 10, 60, mockProgressIndicatorUI, mockClock); + progressIndicator.timerTick(); + verify(mockProgressIndicatorUI, never()).reportState(any(), any(), anyLong(), any(), any()); + } + + @Test + public void displaysProgressAfterStartingComputation() { + ProgressIndicator progressIndicator = new ProgressIndicator( + 10, 60, mockProgressIndicatorUI, mockClock); + verify(mockProgressIndicatorUI, never()).reportState(any(), any(), anyLong(), any(), any()); + progressIndicator.startComputation(Collections.singletonList(3)); + verify(mockProgressIndicatorUI, times(1)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 0)), + eq(0L), + eq(new OneItemProgress(3, 0)), + eq(new OneItemProgress(60000, 0))); + verify(mockProgressIndicatorUI, times(1)) + .reportState(any(), any(), anyLong(), any(), any()); + } + + @Test + public void displaysTickProgressAfterStartingComputation() { + ProgressIndicator progressIndicator = new ProgressIndicator( + 10, 60, mockProgressIndicatorUI, mockClock); + verify(mockProgressIndicatorUI, never()).reportState(any(), any(), anyLong(), any(), any()); + progressIndicator.startComputation(Collections.singletonList(3)); + progressIndicator.timerTick(); + verify(mockProgressIndicatorUI, times(2)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 0)), + eq(0L), + eq(new OneItemProgress(3, 0)), + eq(new OneItemProgress(60000, 0))); + verify(mockProgressIndicatorUI, times(2)) + .reportState(any(), any(), anyLong(), any(), any()); + } + + @Test + public void displaysProgressAfterStartingRace() { + ProgressIndicator progressIndicator = new ProgressIndicator( + 10, 60, mockProgressIndicatorUI, mockClock); + verify(mockProgressIndicatorUI, never()).reportState(any(), any(), anyLong(), any(), any()); + + progressIndicator.startComputation(Collections.singletonList(3)); + verify(mockProgressIndicatorUI, times(1)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 0)), + eq(0L), + eq(new OneItemProgress(3, 0)), + eq(new OneItemProgress(60000, 0))); + verify(mockProgressIndicatorUI, times(1)) + .reportState(any(), any(), anyLong(), any(), any()); + + progressIndicator.startRace(0); + verify(mockProgressIndicatorUI, times(2)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 0)), + eq(0L), + eq(new OneItemProgress(3, 0)), + eq(new OneItemProgress(60000, 0))); + verify(mockProgressIndicatorUI, times(2)) + .reportState(any(), any(), anyLong(), any(), any()); + } + + @Test + public void displaysProgressAfterStartingRaceAttempt() { + when(mockClock.millis()).thenReturn(100L); + ProgressIndicator progressIndicator = new ProgressIndicator( + 10, 60, mockProgressIndicatorUI, mockClock); + verify(mockProgressIndicatorUI, never()).reportState(any(), any(), anyLong(), any(), any()); + + progressIndicator.startComputation(Collections.singletonList(3)); + verify(mockProgressIndicatorUI, times(1)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 0)), + eq(0L), + eq(new OneItemProgress(3, 0)), + eq(new OneItemProgress(60000, 0))); + verify(mockProgressIndicatorUI, times(1)) + .reportState(any(), any(), anyLong(), any(), any()); + + progressIndicator.startRace(0); + verify(mockProgressIndicatorUI, times(2)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 0)), + eq(0L), + eq(new OneItemProgress(3, 0)), + eq(new OneItemProgress(60000, 0))); + verify(mockProgressIndicatorUI, times(2)) + .reportState(any(), any(), anyLong(), any(), any()); + + progressIndicator.startRaceAttempt(); + verify(mockProgressIndicatorUI, times(3)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 0)), + eq(0L), + eq(new OneItemProgress(3, 0)), + eq(new OneItemProgress(60000, 0))); + verify(mockProgressIndicatorUI, times(3)) + .reportState(any(), any(), anyLong(), any(), any()); + } + + @Test + public void incrementsTimeForTicksDuringRaceAttempt() { + when(mockClock.millis()).thenReturn(100L); + ProgressIndicator progressIndicator = new ProgressIndicator( + 10, 60, mockProgressIndicatorUI, mockClock); + verify(mockProgressIndicatorUI, never()).reportState(any(), any(), anyLong(), any(), any()); + + progressIndicator.startComputation(Collections.singletonList(3)); + verify(mockProgressIndicatorUI, times(1)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 0)), + eq(0L), + eq(new OneItemProgress(3, 0)), + eq(new OneItemProgress(60000, 0))); + verify(mockProgressIndicatorUI, times(1)) + .reportState(any(), any(), anyLong(), any(), any()); + + progressIndicator.startRace(0); + verify(mockProgressIndicatorUI, times(2)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 0)), + eq(0L), + eq(new OneItemProgress(3, 0)), + eq(new OneItemProgress(60000, 0))); + verify(mockProgressIndicatorUI, times(2)) + .reportState(any(), any(), anyLong(), any(), any()); + + progressIndicator.startRaceAttempt(); + verify(mockProgressIndicatorUI, times(3)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 0)), + eq(0L), + eq(new OneItemProgress(3, 0)), + eq(new OneItemProgress(60000, 0))); + verify(mockProgressIndicatorUI, times(3)) + .reportState(any(), any(), anyLong(), any(), any()); + + when(mockClock.millis()).thenReturn(300L); + progressIndicator.timerTick(); + verify(mockProgressIndicatorUI, times(1)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 0)), + eq(0L), + eq(new OneItemProgress(3, 0)), + eq(new OneItemProgress(60000, 200L))); + verify(mockProgressIndicatorUI, times(4)) + .reportState(any(), any(), anyLong(), any(), any()); + + when(mockClock.millis()).thenReturn(500L); + progressIndicator.timerTick(); + verify(mockProgressIndicatorUI, times(1)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 0)), + eq(0L), + eq(new OneItemProgress(3, 0)), + eq(new OneItemProgress(60000, 400L))); + verify(mockProgressIndicatorUI, times(5)) + .reportState(any(), any(), anyLong(), any(), any()); + } + + @Test + public void incrementsDoneTasksAndTimerWhenFinishingRaceAttempt() { + when(mockClock.millis()).thenReturn(100L); + ProgressIndicator progressIndicator = new ProgressIndicator( + 10, 60, mockProgressIndicatorUI, mockClock); + verify(mockProgressIndicatorUI, never()).reportState(any(), any(), anyLong(), any(), any()); + + progressIndicator.startComputation(Collections.singletonList(3)); + verify(mockProgressIndicatorUI, times(1)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 0)), + eq(0L), + eq(new OneItemProgress(3, 0)), + eq(new OneItemProgress(60000, 0))); + verify(mockProgressIndicatorUI, times(1)) + .reportState(any(), any(), anyLong(), any(), any()); + + progressIndicator.startRace(0); + verify(mockProgressIndicatorUI, times(2)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 0)), + eq(0L), + eq(new OneItemProgress(3, 0)), + eq(new OneItemProgress(60000, 0))); + verify(mockProgressIndicatorUI, times(2)) + .reportState(any(), any(), anyLong(), any(), any()); + + progressIndicator.startRaceAttempt(); + verify(mockProgressIndicatorUI, times(3)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 0)), + eq(0L), + eq(new OneItemProgress(3, 0)), + eq(new OneItemProgress(60000, 0))); + verify(mockProgressIndicatorUI, times(3)) + .reportState(any(), any(), anyLong(), any(), any()); + + when(mockClock.millis()).thenReturn(300L); + progressIndicator.timerTick(); + verify(mockProgressIndicatorUI, times(1)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 0)), + eq(0L), + eq(new OneItemProgress(3, 0)), + eq(new OneItemProgress(60000, 200L))); + verify(mockProgressIndicatorUI, times(4)) + .reportState(any(), any(), anyLong(), any(), any()); + + when(mockClock.millis()).thenReturn(500L); + progressIndicator.finishRaceAttempt(); + verify(mockProgressIndicatorUI, times(1)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 0)), + eq(0L), + eq(new OneItemProgress(3, 1)), + eq(new OneItemProgress(60000, 400L))); + verify(mockProgressIndicatorUI, times(5)) + .reportState(any(), any(), anyLong(), any(), any()); + } + + @Test + public void doesNotIncrementTimerBetweenRaceAttempts() { + when(mockClock.millis()).thenReturn(100L); + ProgressIndicator progressIndicator = new ProgressIndicator( + 10, 60, mockProgressIndicatorUI, mockClock); + verify(mockProgressIndicatorUI, never()).reportState(any(), any(), anyLong(), any(), any()); + + progressIndicator.startComputation(Collections.singletonList(3)); + verify(mockProgressIndicatorUI, times(1)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 0)), + eq(0L), + eq(new OneItemProgress(3, 0)), + eq(new OneItemProgress(60000, 0))); + verify(mockProgressIndicatorUI, times(1)) + .reportState(any(), any(), anyLong(), any(), any()); + + progressIndicator.startRace(0); + verify(mockProgressIndicatorUI, times(2)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 0)), + eq(0L), + eq(new OneItemProgress(3, 0)), + eq(new OneItemProgress(60000, 0))); + verify(mockProgressIndicatorUI, times(2)) + .reportState(any(), any(), anyLong(), any(), any()); + + progressIndicator.startRaceAttempt(); + verify(mockProgressIndicatorUI, times(3)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 0)), + eq(0L), + eq(new OneItemProgress(3, 0)), + eq(new OneItemProgress(60000, 0))); + verify(mockProgressIndicatorUI, times(3)) + .reportState(any(), any(), anyLong(), any(), any()); + + when(mockClock.millis()).thenReturn(500L); + progressIndicator.finishRaceAttempt(); + verify(mockProgressIndicatorUI, times(1)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 0)), + eq(0L), + eq(new OneItemProgress(3, 1)), + eq(new OneItemProgress(60000, 400L))); + verify(mockProgressIndicatorUI, times(4)) + .reportState(any(), any(), anyLong(), any(), any()); + + when(mockClock.millis()).thenReturn(600L); + progressIndicator.timerTick(); + verify(mockProgressIndicatorUI, times(2)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 0)), + eq(0L), + eq(new OneItemProgress(3, 1)), + eq(new OneItemProgress(60000, 400L))); + verify(mockProgressIndicatorUI, times(5)) + .reportState(any(), any(), anyLong(), any(), any()); + } + + @Test + public void endsAllRaceAttemptsForRaceAndIncrementsRaceCounterWhenFindingRace() { + when(mockClock.millis()).thenReturn(100L); + ProgressIndicator progressIndicator = new ProgressIndicator( + 10, 60, mockProgressIndicatorUI, mockClock); + verify(mockProgressIndicatorUI, never()).reportState(any(), any(), anyLong(), any(), any()); + + progressIndicator.startComputation(Collections.singletonList(3)); + verify(mockProgressIndicatorUI, times(1)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 0)), + eq(0L), + eq(new OneItemProgress(3, 0)), + eq(new OneItemProgress(60000, 0))); + verify(mockProgressIndicatorUI, times(1)) + .reportState(any(), any(), anyLong(), any(), any()); + + progressIndicator.startRace(0); + verify(mockProgressIndicatorUI, times(2)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 0)), + eq(0L), + eq(new OneItemProgress(3, 0)), + eq(new OneItemProgress(60000, 0))); + verify(mockProgressIndicatorUI, times(2)) + .reportState(any(), any(), anyLong(), any(), any()); + + progressIndicator.startRaceAttempt(); + verify(mockProgressIndicatorUI, times(3)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 0)), + eq(0L), + eq(new OneItemProgress(3, 0)), + eq(new OneItemProgress(60000, 0))); + verify(mockProgressIndicatorUI, times(3)) + .reportState(any(), any(), anyLong(), any(), any()); + + when(mockClock.millis()).thenReturn(500L); + progressIndicator.finishRaceAttempt(); + verify(mockProgressIndicatorUI, times(1)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 0)), + eq(0L), + eq(new OneItemProgress(3, 1)), + eq(new OneItemProgress(60000, 400L))); + verify(mockProgressIndicatorUI, times(4)) + .reportState(any(), any(), anyLong(), any(), any()); + + progressIndicator.raceFound(); + verify(mockProgressIndicatorUI, times(1)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 1)), + eq(1L), + eq(new OneItemProgress(3, 3)), + eq(new OneItemProgress(60000, 400L))); + verify(mockProgressIndicatorUI, times(5)) + .reportState(any(), any(), anyLong(), any(), any()); + } + + @Test + public void endsAllRaceAttemptsForRaceAndIncrementsRaceCounterWhenFinishingRace() { + when(mockClock.millis()).thenReturn(100L); + ProgressIndicator progressIndicator = new ProgressIndicator( + 10, 60, mockProgressIndicatorUI, mockClock); + verify(mockProgressIndicatorUI, never()).reportState(any(), any(), anyLong(), any(), any()); + + progressIndicator.startComputation(Collections.singletonList(3)); + verify(mockProgressIndicatorUI, times(1)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 0)), + eq(0L), + eq(new OneItemProgress(3, 0)), + eq(new OneItemProgress(60000, 0))); + verify(mockProgressIndicatorUI, times(1)) + .reportState(any(), any(), anyLong(), any(), any()); + + progressIndicator.startRace(0); + verify(mockProgressIndicatorUI, times(2)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 0)), + eq(0L), + eq(new OneItemProgress(3, 0)), + eq(new OneItemProgress(60000, 0))); + verify(mockProgressIndicatorUI, times(2)) + .reportState(any(), any(), anyLong(), any(), any()); + + progressIndicator.startRaceAttempt(); + verify(mockProgressIndicatorUI, times(3)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 0)), + eq(0L), + eq(new OneItemProgress(3, 0)), + eq(new OneItemProgress(60000, 0))); + verify(mockProgressIndicatorUI, times(3)) + .reportState(any(), any(), anyLong(), any(), any()); + + when(mockClock.millis()).thenReturn(500L); + progressIndicator.finishRaceAttempt(); + verify(mockProgressIndicatorUI, times(1)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 0)), + eq(0L), + eq(new OneItemProgress(3, 1)), + eq(new OneItemProgress(60000, 400L))); + verify(mockProgressIndicatorUI, times(4)) + .reportState(any(), any(), anyLong(), any(), any()); + + progressIndicator.noRaceFound(); + verify(mockProgressIndicatorUI, times(1)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 1)), + eq(0L), + eq(new OneItemProgress(3, 3)), + eq(new OneItemProgress(60000, 400L))); + verify(mockProgressIndicatorUI, times(5)) + .reportState(any(), any(), anyLong(), any(), any()); + } + + @Test + public void fileProgress() { + when(mockClock.millis()).thenReturn(100L); + ProgressIndicator progressIndicator = new ProgressIndicator( + 10, 60, mockProgressIndicatorUI, mockClock); + verify(mockProgressIndicatorUI, never()).reportState(any(), any(), anyLong(), any(), any()); + + progressIndicator.startComputation(Collections.singletonList(3)); + verify(mockProgressIndicatorUI, times(1)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 0)), + eq(0L), + eq(new OneItemProgress(3, 0)), + eq(new OneItemProgress(60000, 0))); + verify(mockProgressIndicatorUI, times(1)) + .reportState(any(), any(), anyLong(), any(), any()); + + progressIndicator.startRace(0); + verify(mockProgressIndicatorUI, times(2)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 0)), + eq(0L), + eq(new OneItemProgress(3, 0)), + eq(new OneItemProgress(60000, 0))); + verify(mockProgressIndicatorUI, times(2)) + .reportState(any(), any(), anyLong(), any(), any()); + + progressIndicator.startRaceAttempt(); + verify(mockProgressIndicatorUI, times(3)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 0)), + eq(0L), + eq(new OneItemProgress(3, 0)), + eq(new OneItemProgress(60000, 0))); + verify(mockProgressIndicatorUI, times(3)) + .reportState(any(), any(), anyLong(), any(), any()); + + when(mockClock.millis()).thenReturn(500L); + progressIndicator.finishRaceAttempt(); + verify(mockProgressIndicatorUI, times(1)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 0)), + eq(0L), + eq(new OneItemProgress(3, 1)), + eq(new OneItemProgress(60000, 400L))); + verify(mockProgressIndicatorUI, times(4)) + .reportState(any(), any(), anyLong(), any(), any()); + + progressIndicator.raceFound(); + verify(mockProgressIndicatorUI, times(1)) + .reportState( + eq(new OneItemProgress(10, 0)), + eq(new OneItemProgress(1, 1)), + eq(1L), + eq(new OneItemProgress(3, 3)), + eq(new OneItemProgress(60000, 400L))); + verify(mockProgressIndicatorUI, times(5)) + .reportState(any(), any(), anyLong(), any(), any()); + + progressIndicator.endWindow(5); + verify(mockProgressIndicatorUI, times(5)) + .reportState(any(), any(), anyLong(), any(), any()); + + progressIndicator.timerTick(); + verify(mockProgressIndicatorUI, times(5)) + .reportState(any(), any(), anyLong(), any(), any()); + + progressIndicator.startComputation(Arrays.asList(4, 5)); + verify(mockProgressIndicatorUI, times(1)) + .reportState( + eq(new OneItemProgress(10, 5)), + eq(new OneItemProgress(2, 0)), + eq(1L), + eq(new OneItemProgress(9, 0)), + eq(new OneItemProgress(60000, 400L))); + verify(mockProgressIndicatorUI, times(6)) + .reportState(any(), any(), anyLong(), any(), any()); + } +} diff --git a/rv-predict-source/src/test/java/com/runtimeverification/rvpredict/smt/MaximalCausalModelTest.java b/rv-predict-source/src/test/java/com/runtimeverification/rvpredict/smt/MaximalCausalModelTest.java index c1455c1ed8..45a9fd2ce4 100644 --- a/rv-predict-source/src/test/java/com/runtimeverification/rvpredict/smt/MaximalCausalModelTest.java +++ b/rv-predict-source/src/test/java/com/runtimeverification/rvpredict/smt/MaximalCausalModelTest.java @@ -8,6 +8,7 @@ import com.runtimeverification.rvpredict.log.compact.Context; import com.runtimeverification.rvpredict.log.compact.InvalidTraceDataException; import com.runtimeverification.rvpredict.metadata.Metadata; +import com.runtimeverification.rvpredict.progressindicator.NullProgressIndicator; import com.runtimeverification.rvpredict.smt.visitors.Z3Filter; import com.runtimeverification.rvpredict.testutils.TraceUtils; import com.runtimeverification.rvpredict.trace.RawTrace; @@ -1771,7 +1772,7 @@ private Map findRaces( trace = traceState.initNextTraceWindow(rawTraces); } MaximalCausalModel model = MaximalCausalModel.create( - trace, z3Filter, fastSolver, soundSolver, detectInterruptedThreadRace); + trace, z3Filter, fastSolver, soundSolver, new NullProgressIndicator(), detectInterruptedThreadRace); Map> sigToRaceSuspects = new HashMap<>(); ArrayList raceSuspects = new ArrayList<>(); diff --git a/rv-predict-source/src/test/java/com/runtimeverification/rvpredict/trace/TraceCacheTest.java b/rv-predict-source/src/test/java/com/runtimeverification/rvpredict/trace/TraceCacheTest.java index a00093afc9..7a8f66daa1 100644 --- a/rv-predict-source/src/test/java/com/runtimeverification/rvpredict/trace/TraceCacheTest.java +++ b/rv-predict-source/src/test/java/com/runtimeverification/rvpredict/trace/TraceCacheTest.java @@ -90,7 +90,7 @@ public void createsOneRawTracePerThread() throws IOException { beginThread1, readData1Thread1, beginThread2, readDataThread2, readData2Thread1)); TraceCache traceCache = - TraceCache.createForTesting( + TestTraceCache.createForTesting( mockConfiguration, mockTraceState, mockLockGraph, Collections.singletonList(eventReader)); Assert.assertEquals(mockTrace, traceCache.getTraceWindow()); @@ -136,7 +136,7 @@ public void createsOneRawTracePerSignal() throws IOException { beginThread1, readData1Thread1, beginSignal, readDataSignal, readData2Thread1)); TraceCache traceCache = - TraceCache.createForTesting( + TestTraceCache.createForTesting( mockConfiguration, mockTraceState, mockLockGraph, Collections.singletonList(eventReader)); Assert.assertEquals(mockTrace, traceCache.getTraceWindow()); @@ -192,7 +192,7 @@ public void splitsConsecutiveSignalRunsIntoRawTraces() throws IOException { readData2Thread1)); TraceCache traceCache = - TraceCache.createForTesting( + TestTraceCache.createForTesting( mockConfiguration, mockTraceState, mockLockGraph, Collections.singletonList(eventReader)); Assert.assertEquals(mockTrace, traceCache.getTraceWindow()); @@ -244,7 +244,7 @@ public void usesNewIdForStartingThread() throws IOException { new ListEventReader(Arrays.asList(beginThread1, readData1Thread1)); TraceCache traceCache = - TraceCache.createForTesting( + TestTraceCache.createForTesting( mockConfiguration, mockTraceState, mockLockGraph, Collections.singletonList(eventReader)); Assert.assertEquals(mockTrace, traceCache.getTraceWindow()); @@ -280,7 +280,7 @@ public void usesPreviousThreadIdForContinuingThread() throws IOException { new ListEventReader(Arrays.asList(beginThread1, readData1Thread1)); TraceCache traceCache = - TraceCache.createForTesting( + TestTraceCache.createForTesting( mockConfiguration, mockTraceState, mockLockGraph, Collections.singletonList(eventReader)); Assert.assertEquals(mockTrace, traceCache.getTraceWindow()); @@ -317,7 +317,7 @@ public void usesNewIdForStartingSignal() throws IOException { new ListEventReader(Collections.singletonList(beginSignal)); TraceCache traceCache = - TraceCache.createForTesting( + TestTraceCache.createForTesting( mockConfiguration, mockTraceState, mockLockGraph, Collections.singletonList(eventReader)); Assert.assertEquals(mockTrace, traceCache.getTraceWindow()); @@ -352,7 +352,7 @@ public void usesPreviousThreadIdForContinuingSignal() throws IOException { new ListEventReader(Collections.singletonList(readData)); TraceCache traceCache = - TraceCache.createForTesting( + TestTraceCache.createForTesting( mockConfiguration, mockTraceState, mockLockGraph, Collections.singletonList(eventReader)); Assert.assertEquals(mockTrace, traceCache.getTraceWindow()); @@ -388,7 +388,7 @@ public void clearsThreadIdForEndingSignal() throws IOException { new ListEventReader(Arrays.asList(readData, endSignal)); TraceCache traceCache = - TraceCache.createForTesting( + TestTraceCache.createForTesting( mockConfiguration, mockTraceState, mockLockGraph, Collections.singletonList(eventReader)); Assert.assertEquals(mockTrace, traceCache.getTraceWindow()); @@ -428,7 +428,7 @@ public void clearsThreadIdAndGetsNonReusableIdForEndingSignalContainedWithinWind new ListEventReader(Arrays.asList(beginSignal, readData, endSignal)); TraceCache traceCache = - TraceCache.createForTesting( + TestTraceCache.createForTesting( mockConfiguration, mockTraceState, mockLockGraph, Collections.singletonList(eventReader)); Assert.assertEquals(mockTrace, traceCache.getTraceWindow()); @@ -467,7 +467,7 @@ public void savesNewIdForContinuingSignalEvenIfPreviousSignalStops() throws IOEx new ListEventReader(Arrays.asList(endSignal1, beginSignal2)); TraceCache traceCache = - TraceCache.createForTesting( + TestTraceCache.createForTesting( mockConfiguration, mockTraceState, mockLockGraph, Collections.singletonList(eventReader)); Assert.assertEquals(mockTrace, traceCache.getTraceWindow()); @@ -518,7 +518,7 @@ public void canProcessThreadWithIdLargerThanAThreadWithSignals() throws IOExcept ListEventReader eventReader = new ListEventReader(events); TraceCache traceCache = - TraceCache.createForTesting( + TestTraceCache.createForTesting( mockConfiguration, mockTraceState, mockLockGraph, Collections.singletonList(eventReader)); Assert.assertEquals(mockTrace, traceCache.getTraceWindow()); @@ -625,6 +625,11 @@ public ReadonlyEventInterface lastReadEvent() { return lastReadEvent; } + @Override + public long bytesRead() throws IOException { + return 0; + } + @Override public void close() throws IOException {