Skip to content

Commit

Permalink
Added proper ProgressModel settings to unit tests.
Browse files Browse the repository at this point in the history
  • Loading branch information
@ThomasHaas
ThomasHaas committed Sep 12, 2024
1 parent 8ef02e1 commit 882eaad
Show file tree
Hide file tree
Showing 9 changed files with 47 additions and 58 deletions.
16 changes: 9 additions & 7 deletions dartagnan/src/main/java/com/dat3m/dartagnan/configuration/ProgressModel.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
}
25 changes: 6 additions & 19 deletions dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ExecutionAnalysis.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}

Expand Down
5 changes: 4 additions & 1 deletion dartagnan/src/test/java/com/dat3m/dartagnan/c/AbstractCTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -79,10 +80,11 @@ protected Provider<Configuration> getConfigurationProvider() {
protected final Provider<Integer> boundProvider = getBoundProvider();
protected final Provider<Program> programProvider = Providers.createProgramFromPath(filePathProvider);
protected final Provider<Wmm> wmmProvider = getWmmProvider();
protected final Provider<ProgressModel> progressModelProvider = () -> ProgressModel.FAIR;
protected final Provider<Solvers> solverProvider = getSolverProvider();
protected final Provider<EnumSet<Property>> propertyProvider = getPropertyProvider();
protected final Provider<Configuration> configurationProvider = getConfigurationProvider();
protected final Provider<VerificationTask> taskProvider = Providers.createTask(programProvider, wmmProvider, propertyProvider, targetProvider, boundProvider, configurationProvider);
protected final Provider<VerificationTask> taskProvider = Providers.createTask(programProvider, wmmProvider, propertyProvider, targetProvider, progressModelProvider, boundProvider, configurationProvider);
protected final Provider<SolverContext> contextProvider = Providers.createSolverContextFromManager(shutdownManagerProvider, solverProvider);
protected final Provider<ProverWithTracker> proverProvider = Providers.createProverWithFixedOptions(contextProvider, SolverContext.ProverOptions.GENERATE_MODELS);

Expand All @@ -99,6 +101,7 @@ protected Provider<Configuration> getConfigurationProvider() {
.around(boundProvider)
.around(programProvider)
.around(wmmProvider)
.around(progressModelProvider)
.around(solverProvider)
.around(propertyProvider)
.around(taskProvider)
Expand Down
5 changes: 3 additions & 2 deletions dartagnan/src/test/java/com/dat3m/dartagnan/compilation/AbstractCompilationTest.java
View file
Original file line number Diff line number Diff line change
@@ -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;
Expand Down Expand Up @@ -95,8 +96,8 @@ protected Provider<Configuration> getConfigurationProvider() {
protected final Provider<Wmm> wmm2Provider = getTargetWmmProvider();
protected final Provider<EnumSet<Property>> propertyProvider = getPropertyProvider();
protected final Provider<Configuration> configProvider = getConfigurationProvider();
protected final Provider<VerificationTask> task1Provider = Providers.createTask(program1Provider, wmm1Provider, propertyProvider, sourceProvider, () -> 1, configProvider);
protected final Provider<VerificationTask> task2Provider = Providers.createTask(program2Provider, wmm2Provider, propertyProvider, targetProvider, () -> 1, configProvider);
protected final Provider<VerificationTask> task1Provider = Providers.createTask(program1Provider, wmm1Provider, propertyProvider, sourceProvider, () -> ProgressModel.FAIR, () -> 1, configProvider);
protected final Provider<VerificationTask> task2Provider = Providers.createTask(program2Provider, wmm2Provider, propertyProvider, targetProvider, () -> ProgressModel.FAIR, () -> 1, configProvider);
protected final Provider<SolverContext> context1Provider = Providers.createSolverContextFromManager(shutdownManagerProvider, () -> Solvers.Z3);
protected final Provider<SolverContext> context2Provider = Providers.createSolverContextFromManager(shutdownManagerProvider, () -> Solvers.Z3);
protected final Provider<ProverWithTracker> prover1Provider = Providers.createProverWithFixedOptions(context1Provider, ProverOptions.GENERATE_MODELS);
Expand Down
16 changes: 13 additions & 3 deletions dartagnan/src/test/java/com/dat3m/dartagnan/litmus/AbstractLitmusTest.java
View file
Original file line number Diff line number Diff line change
@@ -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;
Expand All @@ -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;
Expand All @@ -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;
Expand Down Expand Up @@ -88,6 +92,10 @@ protected Provider<Configuration> getConfigurationProvider() {
.build());
}

protected Provider<ProgressModel> getProgressModelProvider() {
return () -> ProgressModel.FAIR;
}

protected Provider<Integer> getBoundProvider() {
return Provider.fromSupplier(() -> 1);
}
Expand All @@ -105,10 +113,11 @@ protected long getTimeout() {
protected final Provider<Integer> boundProvider = getBoundProvider();
protected final Provider<Program> programProvider = Providers.createProgramFromPath(filePathProvider);
protected final Provider<Wmm> wmmProvider = getWmmProvider();
protected final Provider<ProgressModel> progressModelProvider = getProgressModelProvider();
protected final Provider<EnumSet<Property>> propertyProvider = getPropertyProvider();
protected final Provider<Result> expectedResultProvider = Provider.fromSupplier(() -> expectedResults.get(filePathProvider.get().substring(filePathProvider.get().indexOf("/") + 1)));
protected final Provider<Configuration> configProvider = getConfigurationProvider();
protected final Provider<VerificationTask> taskProvider = Providers.createTask(programProvider, wmmProvider, propertyProvider, targetProvider, boundProvider, configProvider);
protected final Provider<VerificationTask> taskProvider = Providers.createTask(programProvider, wmmProvider, propertyProvider, targetProvider, progressModelProvider, boundProvider, configProvider);
protected final Provider<SolverContext> contextProvider = Providers.createSolverContextFromManager(shutdownManagerProvider, () -> Solvers.Z3);
protected final Provider<ProverWithTracker> proverProvider = Providers.createProverWithFixedOptions(contextProvider, ProverOptions.GENERATE_MODELS);
protected final Provider<ProverWithTracker> prover2Provider = Providers.createProverWithFixedOptions(contextProvider, ProverOptions.GENERATE_MODELS);
Expand All @@ -124,6 +133,7 @@ protected long getTimeout() {
.around(boundProvider)
.around(programProvider)
.around(wmmProvider)
.around(progressModelProvider)
.around(propertyProvider)
.around(configProvider)
.around(taskProvider)
Expand Down
9 changes: 0 additions & 9 deletions dartagnan/src/test/java/com/dat3m/dartagnan/litmus/LitmusVulkanFairLivenessTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -24,13 +22,6 @@ public static Iterable<Object[]> data() throws IOException {
return buildLitmusTests("litmus/VULKAN/", "VULKAN-Liveness-Fair");
}

@Override
protected Provider<Configuration> getConfigurationProvider() {
return Provider.fromSupplier(() -> Configuration.builder()
.setOption(PROGRESSMODEL, "fair")
.build());
}

@Override
protected Provider<Arch> getTargetProvider() {
return () -> Arch.VULKAN;
Expand Down
9 changes: 3 additions & 6 deletions dartagnan/src/test/java/com/dat3m/dartagnan/litmus/LitmusVulkanHsaLivenessTest.java
View file
Original file line number Diff line number Diff line change
@@ -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;
Expand All @@ -25,10 +24,8 @@ public static Iterable<Object[]> data() throws IOException {
}

@Override
protected Provider<Configuration> getConfigurationProvider() {
return Provider.fromSupplier(() -> Configuration.builder()
.setOption(PROGRESSMODEL, "hsa")
.build());
protected Provider<ProgressModel> getProgressModelProvider() {
return () -> ProgressModel.HSA;
}

@Override
Expand Down
9 changes: 3 additions & 6 deletions dartagnan/src/test/java/com/dat3m/dartagnan/litmus/LitmusVulkanObeLivenessTest.java
View file
Original file line number Diff line number Diff line change
@@ -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;
Expand All @@ -25,10 +24,8 @@ public static Iterable<Object[]> data() throws IOException {
}

@Override
protected Provider<Configuration> getConfigurationProvider() {
return Provider.fromSupplier(() -> Configuration.builder()
.setOption(PROGRESSMODEL, "obe")
.build());
protected Provider<ProgressModel> getProgressModelProvider() {
return () -> ProgressModel.OBE;
}

@Override
Expand Down
11 changes: 6 additions & 5 deletions dartagnan/src/test/java/com/dat3m/dartagnan/utils/rules/Providers.java
View file
Original file line number Diff line number Diff line change
@@ -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;
Expand Down Expand Up @@ -63,11 +63,12 @@ public static Provider<Program> createProgramFromFile(Supplier<File> fileSupplie
// =========================== Task related providers ==============================

public static Provider<VerificationTask> createTask(Supplier<Program> programSupplier, Supplier<Wmm> wmmSupplier, Supplier<EnumSet<Property>> propertySupplier,
Supplier<Arch> targetSupplier, Supplier<Integer> boundSupplier, Supplier<Configuration> config) {
Supplier<Arch> targetSupplier, Supplier<ProgressModel> progressModelSupplier, Supplier<Integer> boundSupplier, Supplier<Configuration> 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()));
}

Expand Down

0 comments on commit 882eaad

Please sign in to comment.