Add a progress indicator for RV-Predict.

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,31 +72,42 @@ 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);
     }
 
     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<String> 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<String> 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());

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<String, List<Race>> 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<String, Race> 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:

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();

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();
-}
+    ReadonlyEventInterface lastReadEvent();
+
+    long bytesRead() throws IOException;
+}

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();

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.
      *

rv-predict-source/src/main/java/com/runtimeverification/rvpredict/log/compact/CompactEventReader.java

@@ -124,7 +124,7 @@ public static int getNumberOfValues() {
 
         public List<ReadonlyEventInterface> 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<ReadonlyEventInterface> 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;
+        }
+    }
 }

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();
+    }
+}

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<Integer> 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() {
+    }
+}