From 72866a0e3c45f095d4faa04758cd90c0643ba234 Mon Sep 17 00:00:00 2001
From: lemberge <lemberge@4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c>
Date: Fri, 10 Nov 2023 15:37:54 +0000
Subject: [PATCH] Make ParallelAlgorithm generate nested algorithms from the
 threads that they run in

At least MathSAT5 does not like to be accessed from a thread that is different
from the thread it was created in
(see https://github.com/sosy-lab/java-smt/issues/339\). To work around this,
move the generation of nested algorithms into the individual threads that they run in.

Before this commit, the initialization of the algorithms nested in ParallelAlgorithm
was done sequentially at the construction of ParallelAlgorithm.
With this commit, this initialization moves to the run of ParallelAlgorithm,
and happens concurrently for the nested algorithms.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/branches/svcomp24-parallel-portfolio-approach@45076 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
---
 .../core/algorithm/ParallelAlgorithm.java     | 43 ++++++++++---------
 1 file changed, 22 insertions(+), 21 deletions(-)

diff --git a/src/org/sosy_lab/cpachecker/core/algorithm/ParallelAlgorithm.java b/src/org/sosy_lab/cpachecker/core/algorithm/ParallelAlgorithm.java
index a0e6c095b79..48776f9d07c 100644
--- a/src/org/sosy_lab/cpachecker/core/algorithm/ParallelAlgorithm.java
+++ b/src/org/sosy_lab/cpachecker/core/algorithm/ParallelAlgorithm.java
@@ -273,28 +273,29 @@ private Callable<ParallelAnalysisResult> createParallelAnalysis(
     final ResourceLimitChecker singleAnalysisOverallLimit =
         ResourceLimitChecker.fromConfiguration(singleConfig, singleLogger, singleShutdownManager);
 
-    final CoreComponentsFactory coreComponents =
-        new CoreComponentsFactory(
-            singleConfig,
-            singleLogger,
-            singleShutdownManager.getNotifier(),
-            aggregatedReachedSetManager.asView());
-
-    final ConfigurableProgramAnalysis cpa = coreComponents.createCPA(cfa, specification);
-    final Algorithm algorithm = coreComponents.createAlgorithm(cpa, cfa, specification);
-    final ReachedSet reached = coreComponents.createReachedSet(cpa);
-
-    AtomicBoolean terminated = new AtomicBoolean(false);
-    StatisticsEntry statisticsEntry =
-        stats.getNewSubStatistics(
-            reached,
-            singleConfigFileName.toString(),
-            Iterables.getOnlyElement(
-                FluentIterable.from(singleAnalysisOverallLimit.getResourceLimits())
-                    .filter(ThreadCpuTimeLimit.class),
-                null),
-            terminated);
     return () -> {
+      final CoreComponentsFactory coreComponents =
+          new CoreComponentsFactory(
+              singleConfig,
+              singleLogger,
+              singleShutdownManager.getNotifier(),
+              aggregatedReachedSetManager.asView());
+
+      final ConfigurableProgramAnalysis cpa = coreComponents.createCPA(cfa, specification);
+      final Algorithm algorithm = coreComponents.createAlgorithm(cpa, cfa, specification);
+      final ReachedSet reached = coreComponents.createReachedSet(cpa);
+
+      AtomicBoolean terminated = new AtomicBoolean(false);
+      StatisticsEntry statisticsEntry =
+          stats.getNewSubStatistics(
+              reached,
+              singleConfigFileName.toString(),
+              Iterables.getOnlyElement(
+                  FluentIterable.from(singleAnalysisOverallLimit.getResourceLimits())
+                      .filter(ThreadCpuTimeLimit.class),
+                  null),
+              terminated);
+
       if (algorithm instanceof ConditionAdjustmentEventSubscriber) {
         conditionAdjustmentEventSubscribers.add((ConditionAdjustmentEventSubscriber) algorithm);
       }