From 882eaadff620e65c3a20b855c107e472a4b020e9 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Thu, 12 Sep 2024 11:03:30 +0200 Subject: [PATCH] Added proper ProgressModel settings to unit tests. --- .../configuration/ProgressModel.java | 16 ++++++------ .../program/analysis/ExecutionAnalysis.java | 25 +++++-------------- .../com/dat3m/dartagnan/c/AbstractCTest.java | 5 +++- .../compilation/AbstractCompilationTest.java | 5 ++-- .../dartagnan/litmus/AbstractLitmusTest.java | 16 +++++++++--- .../litmus/LitmusVulkanFairLivenessTest.java | 9 ------- .../litmus/LitmusVulkanHsaLivenessTest.java | 9 +++---- .../litmus/LitmusVulkanObeLivenessTest.java | 9 +++---- .../dartagnan/utils/rules/Providers.java | 11 ++++---- 9 files changed, 47 insertions(+), 58 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/ProgressModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/ProgressModel.java index 933f81c3dd..2a3d808a3c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/ProgressModel.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/ProgressModel.java @@ -8,13 +8,15 @@ public enum ProgressModel { OBE, // Threads that made at least one step get fairly scheduled. UNFAIR; // No fair scheduling - public static ProgressModel getDefault() { return FAIR; } + public static ProgressModel getDefault() { + return FAIR; + } // Used to decide the order shown by the selector in the UI - public static ProgressModel[] orderedValues() { - ProgressModel[] order = { FAIR, HSA, OBE, UNFAIR }; - // Be sure no element is missing - assert(Arrays.asList(order).containsAll(Arrays.asList(values()))); - return order; - } + public static ProgressModel[] orderedValues() { + ProgressModel[] order = {FAIR, HSA, OBE, UNFAIR}; + // Be sure no element is missing + assert (Arrays.asList(order).containsAll(Arrays.asList(values()))); + return order; + } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ExecutionAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ExecutionAnalysis.java index f915763d12..454d26c708 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ExecutionAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ExecutionAnalysis.java @@ -62,25 +62,12 @@ public boolean isImplied(Event start, Event implied) { return true; } // weakest implication holds but not strongest: progress model decides - final boolean implication; - switch (progressModel) { - case FAIR -> { - implication = weakestImplication; // TRUE - } - case HSA -> { - implication = implied.getThread() == lowestIdThread; - } - case OBE -> { - implication = isSameThread(start, implied); - } - case UNFAIR -> { - implication = strongestImplication; // FALSE - } - default -> { - assert false; - implication = strongestImplication; - } - } + final boolean implication = switch (progressModel) { + case FAIR -> weakestImplication; // TRUE + case HSA -> implied.getThread() == lowestIdThread; + case OBE -> isSameThread(start, implied); + case UNFAIR -> strongestImplication; // FALSE + }; return implication; } diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/AbstractCTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/AbstractCTest.java index 39d4ef879d..986af60fb3 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/c/AbstractCTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/c/AbstractCTest.java @@ -2,6 +2,7 @@ import com.dat3m.dartagnan.configuration.Arch; import com.dat3m.dartagnan.configuration.OptionNames; +import com.dat3m.dartagnan.configuration.ProgressModel; import com.dat3m.dartagnan.configuration.Property; import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.program.Program; @@ -79,10 +80,11 @@ protected Provider getConfigurationProvider() { protected final Provider boundProvider = getBoundProvider(); protected final Provider programProvider = Providers.createProgramFromPath(filePathProvider); protected final Provider wmmProvider = getWmmProvider(); + protected final Provider progressModelProvider = () -> ProgressModel.FAIR; protected final Provider solverProvider = getSolverProvider(); protected final Provider> propertyProvider = getPropertyProvider(); protected final Provider configurationProvider = getConfigurationProvider(); - protected final Provider taskProvider = Providers.createTask(programProvider, wmmProvider, propertyProvider, targetProvider, boundProvider, configurationProvider); + protected final Provider taskProvider = Providers.createTask(programProvider, wmmProvider, propertyProvider, targetProvider, progressModelProvider, boundProvider, configurationProvider); protected final Provider contextProvider = Providers.createSolverContextFromManager(shutdownManagerProvider, solverProvider); protected final Provider proverProvider = Providers.createProverWithFixedOptions(contextProvider, SolverContext.ProverOptions.GENERATE_MODELS); @@ -99,6 +101,7 @@ protected Provider getConfigurationProvider() { .around(boundProvider) .around(programProvider) .around(wmmProvider) + .around(progressModelProvider) .around(solverProvider) .around(propertyProvider) .around(taskProvider) diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/compilation/AbstractCompilationTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/compilation/AbstractCompilationTest.java index f0d6f31d2a..d895eba4d5 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/compilation/AbstractCompilationTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/compilation/AbstractCompilationTest.java @@ -1,6 +1,7 @@ package com.dat3m.dartagnan.compilation; import com.dat3m.dartagnan.configuration.Arch; +import com.dat3m.dartagnan.configuration.ProgressModel; import com.dat3m.dartagnan.configuration.Property; import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.program.Program; @@ -95,8 +96,8 @@ protected Provider getConfigurationProvider() { protected final Provider wmm2Provider = getTargetWmmProvider(); protected final Provider> propertyProvider = getPropertyProvider(); protected final Provider configProvider = getConfigurationProvider(); - protected final Provider task1Provider = Providers.createTask(program1Provider, wmm1Provider, propertyProvider, sourceProvider, () -> 1, configProvider); - protected final Provider task2Provider = Providers.createTask(program2Provider, wmm2Provider, propertyProvider, targetProvider, () -> 1, configProvider); + protected final Provider task1Provider = Providers.createTask(program1Provider, wmm1Provider, propertyProvider, sourceProvider, () -> ProgressModel.FAIR, () -> 1, configProvider); + protected final Provider task2Provider = Providers.createTask(program2Provider, wmm2Provider, propertyProvider, targetProvider, () -> ProgressModel.FAIR, () -> 1, configProvider); protected final Provider context1Provider = Providers.createSolverContextFromManager(shutdownManagerProvider, () -> Solvers.Z3); protected final Provider context2Provider = Providers.createSolverContextFromManager(shutdownManagerProvider, () -> Solvers.Z3); protected final Provider prover1Provider = Providers.createProverWithFixedOptions(context1Provider, ProverOptions.GENERATE_MODELS); diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/AbstractLitmusTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/AbstractLitmusTest.java index 3316d114eb..78ff645797 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/AbstractLitmusTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/AbstractLitmusTest.java @@ -1,6 +1,7 @@ package com.dat3m.dartagnan.litmus; import com.dat3m.dartagnan.configuration.Arch; +import com.dat3m.dartagnan.configuration.ProgressModel; import com.dat3m.dartagnan.configuration.Property; import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.program.Program; @@ -10,8 +11,8 @@ import com.dat3m.dartagnan.utils.rules.Providers; import com.dat3m.dartagnan.utils.rules.RequestShutdownOnError; import com.dat3m.dartagnan.verification.VerificationTask; -import com.dat3m.dartagnan.verification.solving.RefinementSolver; import com.dat3m.dartagnan.verification.solving.AssumeSolver; +import com.dat3m.dartagnan.verification.solving.RefinementSolver; import com.dat3m.dartagnan.wmm.Wmm; import org.junit.Rule; import org.junit.Test; @@ -27,7 +28,10 @@ import java.nio.file.Files; import java.nio.file.Path; import java.nio.file.Paths; -import java.util.*; +import java.util.ArrayList; +import java.util.EnumSet; +import java.util.Map; +import java.util.Set; import java.util.stream.Stream; import static com.dat3m.dartagnan.configuration.OptionNames.INITIALIZE_REGISTERS; @@ -88,6 +92,10 @@ protected Provider getConfigurationProvider() { .build()); } + protected Provider getProgressModelProvider() { + return () -> ProgressModel.FAIR; + } + protected Provider getBoundProvider() { return Provider.fromSupplier(() -> 1); } @@ -105,10 +113,11 @@ protected long getTimeout() { protected final Provider boundProvider = getBoundProvider(); protected final Provider programProvider = Providers.createProgramFromPath(filePathProvider); protected final Provider wmmProvider = getWmmProvider(); + protected final Provider progressModelProvider = getProgressModelProvider(); protected final Provider> propertyProvider = getPropertyProvider(); protected final Provider expectedResultProvider = Provider.fromSupplier(() -> expectedResults.get(filePathProvider.get().substring(filePathProvider.get().indexOf("/") + 1))); protected final Provider configProvider = getConfigurationProvider(); - protected final Provider taskProvider = Providers.createTask(programProvider, wmmProvider, propertyProvider, targetProvider, boundProvider, configProvider); + protected final Provider taskProvider = Providers.createTask(programProvider, wmmProvider, propertyProvider, targetProvider, progressModelProvider, boundProvider, configProvider); protected final Provider contextProvider = Providers.createSolverContextFromManager(shutdownManagerProvider, () -> Solvers.Z3); protected final Provider proverProvider = Providers.createProverWithFixedOptions(contextProvider, ProverOptions.GENERATE_MODELS); protected final Provider prover2Provider = Providers.createProverWithFixedOptions(contextProvider, ProverOptions.GENERATE_MODELS); @@ -124,6 +133,7 @@ protected long getTimeout() { .around(boundProvider) .around(programProvider) .around(wmmProvider) + .around(progressModelProvider) .around(propertyProvider) .around(configProvider) .around(taskProvider) diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/LitmusVulkanFairLivenessTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/LitmusVulkanFairLivenessTest.java index 9698905a5a..c59f004528 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/LitmusVulkanFairLivenessTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/LitmusVulkanFairLivenessTest.java @@ -6,8 +6,6 @@ import com.dat3m.dartagnan.utils.rules.Provider; import org.junit.runner.RunWith; import org.junit.runners.Parameterized; -import org.sosy_lab.common.configuration.Configuration; -import static com.dat3m.dartagnan.configuration.OptionNames.PROGRESSMODEL; import java.io.IOException; import java.util.EnumSet; @@ -24,13 +22,6 @@ public static Iterable data() throws IOException { return buildLitmusTests("litmus/VULKAN/", "VULKAN-Liveness-Fair"); } - @Override - protected Provider getConfigurationProvider() { - return Provider.fromSupplier(() -> Configuration.builder() - .setOption(PROGRESSMODEL, "fair") - .build()); - } - @Override protected Provider getTargetProvider() { return () -> Arch.VULKAN; diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/LitmusVulkanHsaLivenessTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/LitmusVulkanHsaLivenessTest.java index db351c4c19..62a759226b 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/LitmusVulkanHsaLivenessTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/LitmusVulkanHsaLivenessTest.java @@ -1,13 +1,12 @@ package com.dat3m.dartagnan.litmus; import com.dat3m.dartagnan.configuration.Arch; +import com.dat3m.dartagnan.configuration.ProgressModel; import com.dat3m.dartagnan.configuration.Property; import com.dat3m.dartagnan.utils.Result; import com.dat3m.dartagnan.utils.rules.Provider; import org.junit.runner.RunWith; import org.junit.runners.Parameterized; -import org.sosy_lab.common.configuration.Configuration; -import static com.dat3m.dartagnan.configuration.OptionNames.PROGRESSMODEL; import java.io.IOException; import java.util.EnumSet; @@ -25,10 +24,8 @@ public static Iterable data() throws IOException { } @Override - protected Provider getConfigurationProvider() { - return Provider.fromSupplier(() -> Configuration.builder() - .setOption(PROGRESSMODEL, "hsa") - .build()); + protected Provider getProgressModelProvider() { + return () -> ProgressModel.HSA; } @Override diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/LitmusVulkanObeLivenessTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/LitmusVulkanObeLivenessTest.java index cd4b4fc0a7..b921ae86f1 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/LitmusVulkanObeLivenessTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/LitmusVulkanObeLivenessTest.java @@ -1,13 +1,12 @@ package com.dat3m.dartagnan.litmus; import com.dat3m.dartagnan.configuration.Arch; +import com.dat3m.dartagnan.configuration.ProgressModel; import com.dat3m.dartagnan.configuration.Property; import com.dat3m.dartagnan.utils.Result; import com.dat3m.dartagnan.utils.rules.Provider; import org.junit.runner.RunWith; import org.junit.runners.Parameterized; -import org.sosy_lab.common.configuration.Configuration; -import static com.dat3m.dartagnan.configuration.OptionNames.PROGRESSMODEL; import java.io.IOException; import java.util.EnumSet; @@ -25,10 +24,8 @@ public static Iterable data() throws IOException { } @Override - protected Provider getConfigurationProvider() { - return Provider.fromSupplier(() -> Configuration.builder() - .setOption(PROGRESSMODEL, "obe") - .build()); + protected Provider getProgressModelProvider() { + return () -> ProgressModel.OBE; } @Override diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/utils/rules/Providers.java b/dartagnan/src/test/java/com/dat3m/dartagnan/utils/rules/Providers.java index f31db39a13..419ef92690 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/utils/rules/Providers.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/utils/rules/Providers.java @@ -1,15 +1,15 @@ package com.dat3m.dartagnan.utils.rules; +import com.dat3m.dartagnan.configuration.Arch; +import com.dat3m.dartagnan.configuration.ProgressModel; +import com.dat3m.dartagnan.configuration.Property; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.parsers.cat.ParserCat; import com.dat3m.dartagnan.parsers.program.ProgramParser; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.utils.TestHelper; import com.dat3m.dartagnan.verification.VerificationTask; import com.dat3m.dartagnan.wmm.Wmm; -import com.dat3m.dartagnan.configuration.Arch; -import com.dat3m.dartagnan.configuration.Property; -import com.dat3m.dartagnan.encoding.ProverWithTracker; - import org.sosy_lab.common.ShutdownManager; import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.common.configuration.Configuration; @@ -63,11 +63,12 @@ public static Provider createProgramFromFile(Supplier fileSupplie // =========================== Task related providers ============================== public static Provider createTask(Supplier programSupplier, Supplier wmmSupplier, Supplier> propertySupplier, - Supplier targetSupplier, Supplier boundSupplier, Supplier config) { + Supplier targetSupplier, Supplier progressModelSupplier, Supplier boundSupplier, Supplier config) { return Provider.fromSupplier(() -> VerificationTask.builder(). withConfig(config.get()). withTarget(targetSupplier.get()). withBound(boundSupplier.get()). + withProgressModel(progressModelSupplier.get()). build(programSupplier.get(), wmmSupplier.get(), propertySupplier.get())); }