Squash and merges #748: first version of PEx parallel

Author: aman-goel

Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/RuntimeExecutor.java

@@ -4,6 +4,7 @@
 import pexplicit.runtime.STATUS;
 import pexplicit.runtime.logger.PExplicitLogger;
 import pexplicit.runtime.logger.StatWriter;
+import pexplicit.runtime.scheduler.Scheduler;
 import pexplicit.runtime.scheduler.explicit.ExplicitSearchScheduler;
 import pexplicit.runtime.scheduler.replay.ReplayScheduler;
 import pexplicit.utils.exceptions.BugFoundException;
@@ -14,25 +15,35 @@
 
 import java.time.Duration;
 import java.time.Instant;
+import java.util.ArrayList;
 import java.util.concurrent.*;
 
 /**
  * Represents the runtime executor that executes the analysis engine
  */
 public class RuntimeExecutor {
-    private static ExecutorService executor;
-    private static Future<Integer> future;
-    private static ExplicitSearchScheduler scheduler;
+    private static ThreadPoolExecutor executor;
+    private static ArrayList<Future<Integer>> futures = new ArrayList<>();
+    private static ArrayList<ExplicitSearchScheduler> schedulers = new ArrayList<>();
 
     private static void runWithTimeout(long timeLimit)
             throws TimeoutException,
             InterruptedException,
             RuntimeException {
-        try {
+        try { // PIN: If thread gets exception, need to kill the other threads.
             if (timeLimit > 0) {
-                future.get(timeLimit, TimeUnit.SECONDS);
+                
+                for (Future<Integer> future : futures) {
+                    // Future<Integer> future = futures.get(i);
+                    future.get(timeLimit, TimeUnit.SECONDS);
+                }
+
             } else {
-                future.get();
+
+                for (int i = 0; i < PExplicitGlobal.getMaxThreads(); i++) {
+                    Future<Integer> future = futures.get(i);
+                    future.get();
+                }
             }
         } catch (TimeoutException | BugFoundException e) {
             throw e;
@@ -55,7 +66,11 @@ private static void runWithTimeout(long timeLimit)
 
     private static void printStats() {
         double searchTime = TimeMonitor.stopInterval();
-        scheduler.recordStats();
+        for (int i = 0; i < PExplicitGlobal.getMaxThreads(); i++) {
+            ExplicitSearchScheduler scheduler = schedulers.get(i);
+            scheduler.recordStats();
+        }
+
         if (PExplicitGlobal.getResult().equals("correct for any depth")) {
             PExplicitGlobal.setStatus(STATUS.VERIFIED);
         } else if (PExplicitGlobal.getResult().startsWith("correct up to step")) {
@@ -69,9 +84,9 @@ private static void preprocess() {
         PExplicitLogger.logInfo(String.format("... Checker is using '%s' strategy (seed:%s)",
                 PExplicitGlobal.getConfig().getSearchStrategyMode(), PExplicitGlobal.getConfig().getRandomSeed()));
 
-        executor = Executors.newSingleThreadExecutor();
+        executor = (ThreadPoolExecutor) Executors.newFixedThreadPool(PExplicitGlobal.getMaxThreads());
 
-        PExplicitGlobal.setResult("error");
+        // PExplicitGlobal.setResult("error"); // TODO: Set Results, need to take care of.
 
         double preSearchTime =
                 TimeMonitor.findInterval(TimeMonitor.getStart());
@@ -84,10 +99,29 @@ private static void preprocess() {
 
     private static void process(boolean resume) throws Exception {
         try {
-            TimedCall timedCall = new TimedCall(scheduler, resume);
-            future = executor.submit(timedCall);
+            // create and add first task through scheduler 0
+            schedulers.get(0).getSearchStrategy().createFirstTask();
+
+            ArrayList<TimedCall> timedCalls = new ArrayList<>();
+            for (int i = 0; i < PExplicitGlobal.getMaxThreads(); i++) {
+                timedCalls.add(new TimedCall(schedulers.get(i), resume, i));
+            }
+
+            for (int i = 0; i < PExplicitGlobal.getMaxThreads(); i++) {
+                Future<Integer> future = executor.submit(timedCalls.get(i));
+                futures.add(future);
+            }
+
+            Thread.sleep(1000); // Sleep for 1 second, so that threads can pick up the task from the executor object
+
+            // Get the number of pending tasks
+            int pendingTasks = executor.getQueue().size();
+            PExplicitLogger.logInfo("Number of pending tasks: " + pendingTasks);
+
             TimeMonitor.startInterval();
+
             runWithTimeout((long) PExplicitGlobal.getConfig().getTimeLimit());
+
         } catch (TimeoutException e) {
             PExplicitGlobal.setStatus(STATUS.TIMEOUT);
             throw new Exception("TIMEOUT", e);
@@ -96,13 +130,21 @@ private static void process(boolean resume) throws Exception {
             throw new Exception("MEMOUT", e);
         } catch (BugFoundException e) {
             PExplicitGlobal.setStatus(STATUS.BUG_FOUND);
-            PExplicitGlobal.setResult(String.format("found cex of length %d", scheduler.getStepNumber()));
+
+
             PExplicitLogger.logStackTrace(e);
 
-            ReplayScheduler replayer = new ReplayScheduler(scheduler.schedule);
-            PExplicitGlobal.setScheduler(replayer);
+            ArrayList<ReplayScheduler> replayers = new ArrayList<>();
+            for (int i = 0; i < PExplicitGlobal.getMaxThreads(); i++)
+                replayers.add(new ReplayScheduler((schedulers.get(i)).schedule));
+
+            ArrayList<Scheduler> localSchedulers = PExplicitGlobal.getSchedulers();
+            for (int i = 0; i < PExplicitGlobal.getMaxThreads(); i++)
+                localSchedulers.set(i, replayers.get(i));
+
             try {
-                replayer.run();
+                for (int i = 0; i < PExplicitGlobal.getMaxThreads(); i++)
+                    (replayers.get(i)).run();
             } catch (NullPointerException | StackOverflowError | ClassCastException replayException) {
                 PExplicitLogger.logStackTrace((Exception) replayException);
                 throw new BugFoundException(replayException.getMessage(), replayException);
@@ -121,20 +163,34 @@ private static void process(boolean resume) throws Exception {
             PExplicitGlobal.setStatus(STATUS.ERROR);
             throw new Exception("ERROR", e);
         } finally {
-            future.cancel(true);
+            for (int i = 0; i < PExplicitGlobal.getMaxThreads(); i++) {
+                Future<Integer> future = futures.get(i);
+                future.cancel(true);
+            }
             executor.shutdownNow();
-            scheduler.updateResult();
+            for (int i = 0; i < PExplicitGlobal.getMaxThreads(); i++)
+                (schedulers.get(i)).updateResult();
             printStats();
-            PExplicitLogger.logEndOfRun(scheduler, Duration.between(TimeMonitor.getStart(), Instant.now()).getSeconds());
+            for (int i = 0; i < PExplicitGlobal.getMaxThreads(); i++)
+                PExplicitLogger.logEndOfRun(schedulers.get(i), Duration.between(TimeMonitor.getStart(), Instant.now()).getSeconds());
         }
     }
 
     public static void run() throws Exception {
-        scheduler = new ExplicitSearchScheduler();
-        PExplicitGlobal.setScheduler(scheduler);
+        ArrayList<Scheduler> localSchedulers = PExplicitGlobal.getSchedulers();
+        for (int i = 0; i < PExplicitGlobal.getMaxThreads(); i++) {
+            ExplicitSearchScheduler localCopy = new ExplicitSearchScheduler();
+            schedulers.add(localCopy);
+            localSchedulers.add(localCopy);
+        }
+
 
         preprocess();
+
+
         process(false);
+
+
     }
 
 }

Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitConfig.java

@@ -11,6 +11,9 @@
  */
 @Getter
 public class PExplicitConfig {
+    @Getter
+    @Setter
+    private static int numThreads = 1;
     // default name of the test driver
     final String testDriverDefault = "DefaultImpl";
     // name of the test driver
@@ -64,4 +67,5 @@ public class PExplicitConfig {
     //max number of children search tasks
     @Setter
     int maxChildrenPerTask = 2;
+
 }

Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitOptions.java

@@ -148,7 +148,16 @@ public class PExplicitOptions {
                         .build();
         addOption(randomSeed);
 
-
+        // Number of threads
+        Option numThreads =
+                Option.builder()
+                        .longOpt("nproc")
+                        .desc("Specify the number of threads to use")
+                        .numberOfArgs(1)
+                        .hasArg()
+                        .argName("No. of threads (integer)")
+                        .build();
+        addOption(numThreads);
         /*
          * Invisible/expert options
          */
@@ -336,6 +345,9 @@ public static PExplicitConfig ParseCommandlineArgs(String[] args) {
                                 option, String.format("Expected an integer value, got %s", option.getValue()));
                     }
                     break;
+                case "nproc":
+                    PExplicitConfig.setNumThreads(Integer.parseInt(option.getValue()));
+                    break;
                 // invisible expert options
                 case "state-caching":
                     switch (option.getValue()) {

Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/ForeignFunctionInterface.java

@@ -5,24 +5,24 @@
 import java.util.function.Function;
 
 public class ForeignFunctionInterface {
-  /**
-   * Invoke a foreign function with a void return type
-   *
-   * @param fn function to invoke
-   * @param args arguments
-   */
-  public static void accept(Consumer<List<Object>> fn, Object... args) {
-    fn.accept(List.of(args));
-  }
+    /**
+     * Invoke a foreign function with a void return type
+     *
+     * @param fn   function to invoke
+     * @param args arguments
+     */
+    public static void accept(Consumer<List<Object>> fn, Object... args) {
+        fn.accept(List.of(args));
+    }
 
-  /**
-   * Invoke a foreign function with a non-void return type
-   *
-   * @param fn function to invoke
-   * @param args arguments
-   * @return the return value of the function
-   */
-  public static Object apply(Function<List<Object>, Object> fn, Object... args) {
-    return fn.apply(List.of(args));
-  }
+    /**
+     * Invoke a foreign function with a non-void return type
+     *
+     * @param fn   function to invoke
+     * @param args arguments
+     * @return the return value of the function
+     */
+    public static Object apply(Function<List<Object>, Object> fn, Object... args) {
+        return fn.apply(List.of(args));
+    }
 }