Skip to content

Move ProgressModel and RoundingMode to Program #978

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
ThomasHaas wants to merge 2 commits into
base: development
Choose a base branch
from
Open

Move ProgressModel and RoundingMode to Program #978

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
7d75239
- Add Program.SemanticConfig to configure progress model and floating…
ThomasHaas Feb 9, 2026
341792b
Fix ProgressModel in AbstractCTest
ThomasHaas Feb 9, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 7 additions & 3 deletions dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,6 @@
import com.dat3m.dartagnan.witness.graphml.WitnessGraph;
import com.dat3m.dartagnan.wmm.Wmm;
import com.dat3m.dartagnan.wmm.axiom.Axiom;

import com.google.common.base.Preconditions;
import com.google.common.collect.ImmutableSet;
import com.google.common.io.CharSource;
Expand Down Expand Up @@ -83,6 +82,11 @@ private Dartagnan(Configuration config) throws InvalidConfigurationException {
config.recursiveInject(this);
}

static {
// Register type converters globally
Configuration.getDefaultConverters().put(ProgressModel.Hierarchy.class, ProgressModel.HIERARCHY_CONVERTER);
}

private static Configuration loadConfiguration(String[] args) throws InvalidConfigurationException, IOException {
final var preamble = new StringBuilder();
final var options = new StringBuilder();
Expand All @@ -95,7 +99,6 @@ private static Configuration loadConfiguration(String[] args) throws InvalidConf
}
final CharSource source = CharSource.concat(CharSource.wrap(preamble), CharSource.wrap(options));
return Configuration.builder()
.addConverter(ProgressModel.Hierarchy.class, ProgressModel.HIERARCHY_CONVERTER)
.loadFromSource(source, ".", ".")
.build();
}
Expand Down Expand Up @@ -146,10 +149,11 @@ public static void main(String[] args) throws Exception {
p.setEntrypoint(new Entrypoint.Simple(p.getFunctionByName(o.getEntryFunction()).orElseThrow(
() -> new MalformedProgramException(String.format("Program has no function named %s. Select a different entry point.", o.getEntryFunction())))));
}
p.injectConfig(config);

final Wmm mcm = new ParserCat(Path.of(o.getCatIncludePath())).parse(fileModel);
final VerificationTaskBuilder builder = VerificationTask.builder()
.withConfig(config)
.withProgressModel(o.getProgressModel())
.withWitness(witness);
// If the arch has been set during parsing (this only happens for litmus tests)
// and the user did not explicitly add the target option, we use the one
Expand Down
23 changes: 22 additions & 1 deletion dartagnan/src/main/java/com/dat3m/dartagnan/configuration/ProgressModel.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@
import com.google.common.collect.Maps;
import com.google.common.reflect.TypeToken;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.sosy_lab.common.configuration.Configuration;
import org.sosy_lab.common.configuration.InvalidConfigurationException;
import org.sosy_lab.common.configuration.converters.TypeConverter;
import org.sosy_lab.common.log.LogManager;
Expand Down Expand Up @@ -78,12 +79,27 @@ public ProgressModel getDefaultProgress() {

@Override
public String toString() {
if (scope2Progress.isEmpty()) {
if (isUniform()) {
return defaultProgress.toString();
} else {
return scope2Progress + " with default=" + defaultProgress;
}
}

public String toOptionString() {
if (isUniform()) {
return defaultProgress.toString();
} else {
StringBuilder builder = new StringBuilder();
builder.append("[");
scope2Progress.entrySet().stream()
.map(e -> e.getKey() + "=" + e.getValue().toString())
.forEach(builder::append);
builder.append(", default=").append(defaultProgress.toString());
builder.append("]");
return builder.toString();
}
}
}

// ================================================================================================================
Expand Down Expand Up @@ -141,4 +157,9 @@ public String toString() {
return value;
}
};

static {
// Register type converter globally
Configuration.getDefaultConverters().put(ProgressModel.Hierarchy.class, ProgressModel.HIERARCHY_CONVERTER);
}
}
20 changes: 3 additions & 17 deletions dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,28 +24,21 @@
import com.dat3m.dartagnan.wmm.axiom.Acyclicity;
import com.dat3m.dartagnan.wmm.utils.graph.EventGraph;
import com.google.common.collect.Iterables;

import org.slf4j.Logger;
import org.slf4j.LoggerFactory;
import org.sosy_lab.common.configuration.InvalidConfigurationException;
import org.sosy_lab.common.configuration.Option;
import org.sosy_lab.common.configuration.Options;
import org.sosy_lab.java_smt.api.*;
import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
import org.sosy_lab.java_smt.api.FloatingPointRoundingMode;

import java.util.Collection;
import java.util.HashMap;
import java.util.LinkedHashSet;
import java.util.List;
import java.util.Map;
import java.util.*;

import static com.dat3m.dartagnan.configuration.OptionNames.*;
import static com.dat3m.dartagnan.program.event.Tag.INIT;
import static com.dat3m.dartagnan.program.event.Tag.WRITE;
import static com.google.common.base.Preconditions.checkArgument;
import static com.google.common.base.Preconditions.checkNotNull;
import static org.sosy_lab.java_smt.api.FloatingPointRoundingMode.*;

@Options
public final class EncodingContext {
Expand Down Expand Up @@ -80,13 +73,6 @@ public final class EncodingContext {
secure = true)
boolean useIntegers = false;

// TODO: If we ever simplify floats, this option will play a role there besides than the encoding.
// If that is the case we need to move this option outside of this encoding class.
@Option(name = ROUNDING_MODE_FLOATS,
description = "Rounding mode for floating point operations.",
secure = true)
FloatingPointRoundingMode roundingModeFloats = NEAREST_TIES_TO_EVEN;

private final Map<Event, BooleanFormula> controlFlowVariables = new HashMap<>();
private final Map<Event, BooleanFormula> executionVariables = new HashMap<>();
private final Map<NamedBarrier, BooleanFormula> syncVariables = new HashMap<>();
Expand Down Expand Up @@ -128,7 +114,7 @@ public static EncodingContext of(VerificationTask task, Context analysisContext,
task.getConfig().inject(context);
logger.info("{}: {}", IDL_TO_SAT, context.useSATEncoding);
logger.info("{}: {}", MERGE_CF_VARS, context.shouldMergeCFVars);
logger.info("{}: {}", ROUNDING_MODE_FLOATS, context.roundingModeFloats);
logger.info("{}: {}", ROUNDING_MODE_FLOATS, context.getTask().getProgram().getFloatRoundingMode());
context.initialize();
if (logger.isInfoEnabled()) {
logger.info("Number of encoded edges for acyclicity: {}",
Expand Down Expand Up @@ -336,7 +322,7 @@ private void initialize() {
// Only for the standard fair progress model we can merge CF variables.
// TODO: It would also be possible for OBE/HSA in some cases if we refine the cf-equivalence classes
// to classes per thread.
final boolean mergeCFVars = shouldMergeCFVars && verificationTask.getProgressModel().isFair();
final boolean mergeCFVars = shouldMergeCFVars && verificationTask.getProgram().getProgressModel().isFair();
if (mergeCFVars) {
for (BranchEquivalence.Class cls : analysisContext.get(BranchEquivalence.class).getAllEquivalenceClasses()) {
BooleanFormula v = booleanFormulaManager.makeVariable("cf " + cls.getRepresentative().getGlobalId());
Expand Down
18 changes: 11 additions & 7 deletions dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,11 +45,15 @@ public class ExpressionEncoder {
private final FormulaManagerExt fmgr;
private final BooleanFormulaManager bmgr;
private final Visitor visitor = new Visitor();

private final FloatingPointRoundingMode roundingMode;

ExpressionEncoder(EncodingContext context) {
this.context = context;
this.fmgr = context.getFormulaManager();
this.bmgr = fmgr.getBooleanFormulaManager();

this.roundingMode = context.getTask().getProgram().getFloatRoundingMode();
}

private IntegerFormulaManager integerFormulaManager() {
Expand Down Expand Up @@ -543,7 +547,7 @@ public TypedFormula<BooleanType, BooleanFormula> visitIntCmpExpression(IntCmpExp
final Formula operand = encodeIntegerExpr(expr.getOperand()).formula();
final FloatType fType = expr.getTargetType();
final FloatingPointType targetType = getFloatFormulaType(fType);
final Formula enc = floatingPointFormulaManager().castFrom(operand, true, targetType, context.roundingModeFloats);
final Formula enc = floatingPointFormulaManager().castFrom(operand, true, targetType, roundingMode);
return new TypedFormula<>(fType, enc);
}

Expand All @@ -561,7 +565,7 @@ public TypedFormula<BooleanType, BooleanFormula> visitIntCmpExpression(IntCmpExp
} else if (floatLiteral.isMinusInf()) {
result = floatingPointFormulaManager().makeMinusInfinity(fFType);
} else {
result = floatingPointFormulaManager().makeNumber(floatLiteral.getValue(), fFType, context.roundingModeFloats);
result = floatingPointFormulaManager().makeNumber(floatLiteral.getValue(), fFType, roundingMode);
}
return new TypedFormula<>(floatLiteral.getType(), result);
}
Expand All @@ -575,10 +579,10 @@ public TypedFormula<BooleanType, BooleanFormula> visitIntCmpExpression(IntCmpExp
final FloatingPointFormulaManager fpmgr = floatingPointFormulaManager();

final FloatingPointFormula result = switch (fBin.getKind()) {
case FADD -> fpmgr.add(fp1, fp2, context.roundingModeFloats);
case FSUB -> fpmgr.subtract(fp1, fp2, context.roundingModeFloats);
case FMUL -> fpmgr.multiply(fp1, fp2, context.roundingModeFloats);
case FDIV -> fpmgr.divide(fp1, fp2, context.roundingModeFloats);
case FADD -> fpmgr.add(fp1, fp2, roundingMode);
case FSUB -> fpmgr.subtract(fp1, fp2, roundingMode);
case FMUL -> fpmgr.multiply(fp1, fp2, roundingMode);
case FDIV -> fpmgr.divide(fp1, fp2, roundingMode);
case FREM -> fpmgr.remainder(fp1, fp2);
case FMAX -> fpmgr.max(fp1, fp2);
case FMIN -> fpmgr.min(fp1, fp2);
Expand Down Expand Up @@ -644,7 +648,7 @@ private BooleanFormula fromUnordToOrd(FloatingPointFormula l, FloatingPointFormu

final FloatingPointFormulaManager fpmgr = floatingPointFormulaManager();
final FloatingPointType fType = getFloatFormulaType(expr.getTargetType());
final Formula enc = fpmgr.castFrom(inner.formula(), true, fType, context.roundingModeFloats);
final Formula enc = fpmgr.castFrom(inner.formula(), true, fType, roundingMode);
return new TypedFormula<>(expr.getType(), enc);
}

Expand Down
9 changes: 5 additions & 4 deletions dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,6 @@
import com.dat3m.dartagnan.program.memory.Memory;
import com.dat3m.dartagnan.program.memory.MemoryObject;
import com.dat3m.dartagnan.program.misc.NonDetValue;

import com.google.common.base.Preconditions;
import com.google.common.base.Verify;
import com.google.common.collect.ImmutableList;
Expand Down Expand Up @@ -192,9 +191,11 @@ private int getWorkgroupId(Thread thread) {
}

public BooleanFormula encodeControlFlow() {
logger.info("Encoding program control flow with progress model {}", context.getTask().getProgressModel());

final Program program = context.getTask().getProgram();
final ProgressModel.Hierarchy progressModel = program.getProgressModel();

logger.info("Encoding program control flow with progress model {}", progressModel);

final BooleanFormulaManager bmgr = context.getBooleanFormulaManager();
final ForwardProgressEncoder progressEncoder = new ForwardProgressEncoder();
List<BooleanFormula> enc = new ArrayList<>();
Expand All @@ -207,7 +208,7 @@ public BooleanFormula encodeControlFlow() {
}

// Actual forward progress
enc.add(progressEncoder.encodeForwardProgress(program, context.getTask().getProgressModel()));
enc.add(progressEncoder.encodeForwardProgress(program, progressModel));

return bmgr.and(enc);
}
Expand Down
70 changes: 64 additions & 6 deletions dartagnan/src/main/java/com/dat3m/dartagnan/program/Program.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
package com.dat3m.dartagnan.program;

import com.dat3m.dartagnan.configuration.Arch;
import com.dat3m.dartagnan.configuration.ProgressModel;
import com.dat3m.dartagnan.expression.Expression;
import com.dat3m.dartagnan.expression.ExpressionFactory;
import com.dat3m.dartagnan.expression.Type;
Expand All @@ -12,10 +13,19 @@
import com.dat3m.dartagnan.program.memory.MemoryObject;
import com.dat3m.dartagnan.program.misc.NonDetValue;
import com.google.common.base.Preconditions;
import org.sosy_lab.common.configuration.Configuration;
import org.sosy_lab.common.configuration.InvalidConfigurationException;
import org.sosy_lab.common.configuration.Option;
import org.sosy_lab.common.configuration.Options;
import org.sosy_lab.java_smt.api.FloatingPointRoundingMode;

import java.util.*;
import java.util.stream.Collectors;

import static com.dat3m.dartagnan.configuration.OptionNames.PROGRESSMODEL;
import static com.dat3m.dartagnan.configuration.OptionNames.ROUNDING_MODE_FLOATS;
import static org.sosy_lab.java_smt.api.FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN;

public class Program {

private static final TypeFactory types = TypeFactory.getInstance();
Expand All @@ -25,19 +35,45 @@ public enum SourceLanguage { LITMUS, LLVM, SPV }

public enum SpecificationType { EXISTS, FORALL, NOT_EXISTS, ASSERT }

private String name;
private SpecificationType specificationType = SpecificationType.ASSERT;
private Expression spec;
private Expression filterSpec; // Acts like "assume" statements, filtering out executions
@Options
private static class SemanticConfig {
@Option(name = ROUNDING_MODE_FLOATS,
description = "Default rounding mode for floating point operations (default NEAREST_TIES_TO_EVEN).",
secure = true)
private FloatingPointRoundingMode floatRoundingMode = NEAREST_TIES_TO_EVEN;

@Option(
name = PROGRESSMODEL,
description = """
The progress model to assume: fair (default), hsa, obe, lobe, hsa_obe, unfair.
To specify progress models per scope, use [<scope>=<progressModel>,...].
Defaults to "fair" for unspecified scopes unless "default=<progressModel>" is specified.
""",
toUppercase = true)
private ProgressModel.Hierarchy progressModel = ProgressModel.defaultHierarchy();
}
Comment on lines +40 to +54
Copy link
Copy Markdown
Owner

@hernanponcedeleon hernanponcedeleon Feb 18, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

While I agree we can argue the floating point rounding mode is part of the semantics of the program this is definitely not the case for the progress model; thus this is not a good place for this option. The later is dependent from the execution environment (in the same way we cannot say that the memory model is part of the program semantics per se).

Copy link
Copy Markdown
Collaborator Author

@ThomasHaas ThomasHaas Feb 18, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

While I technically agree that you can argue that the WMM and the ProgressModel are both parts of the environment (to some degree even the rounding mode might be?), I wouldn't necessarily conclude that we must treat them in a similar fashion in Dartagnan.

Generally, the way I see axiomatic program semantics is like this: there is an operational semantics (~a transition system) that models the execution of each thread in a program, and there is the axiomatic layer on top that justifies, in hindsight, each threads actions via rf-edges and possibly other dynamic relations.
In that world, everything that affects the operational part of the semantics I would consider a part of the program, i.e., control-flow, data-flow, rounding modes, speculation behavior, etc.
Then the progress model is considered part of the program as it defines the control-flow behavior of the underlying transition system.
Indeed, this is also reflected in our analyses and the encoding: the ProgramEncoder encodes the progress model, and the ExecutionAnalysis - which we consider a program analysis - reasons about it.

At this point in time, I don't see much benefit in having a third type of "Environment Model" and possibly an "EnvironmentEncoder" to go along with it.

EDIT: Just to make sure: I'm not totally against moving execution environment model elsewhere, possibly back into the VerificationTask class. But at least for now, having the environment model in the Program makes things a bit easier, especially if the model is just a few fields defined by a config.


// Shape
private final List<Thread> threads;
private final List<Function> functions;
private final List<NonDetValue> constants = new ArrayList<>();
private final Memory memory;
private Entrypoint entrypoint = new Entrypoint.None();

// Semantic options
private final SemanticConfig semanticConfig = new SemanticConfig();

// Spec
private SpecificationType specificationType = SpecificationType.ASSERT;
private Expression spec;
private Expression filterSpec; // Acts like "assume" statements, filtering out executions

// Metadata
private String name;
private final SourceLanguage format;
private Arch arch;
private int unrollingBound = 0;
private boolean isCompiled;
private final SourceLanguage format;
private int unrollingBound = 0;

private int nextThreadId = 0;
private int nextConstantId = 0;
Expand Down Expand Up @@ -128,6 +164,28 @@ public void setFilterSpecification(Expression spec) {
this.filterSpec = spec;
}

public FloatingPointRoundingMode getFloatRoundingMode() {
return semanticConfig.floatRoundingMode;
}

public void setFloatRoundingMode(FloatingPointRoundingMode roundingMode) {
this.semanticConfig.floatRoundingMode = roundingMode;
}

public ProgressModel.Hierarchy getProgressModel() {
return semanticConfig.progressModel;
}

public void setProgressModel(ProgressModel.Hierarchy progressModel) {
semanticConfig.progressModel = progressModel;
}

public void injectConfig(Configuration configuration) throws InvalidConfigurationException {
configuration.inject(semanticConfig);
}

// -----------------------------------------------------------------------------------------------------------------

public void addThread(Thread t) {
threads.add(t);
t.setProgram(this);
Expand Down
8 changes: 4 additions & 4 deletions dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ExecutionAnalysis.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,10 +18,10 @@ public interface ExecutionAnalysis {



static ExecutionAnalysis fromConfig(Program program, ProgressModel.Hierarchy progressModel, Context context, Configuration config)
static ExecutionAnalysis fromConfig(Program program, Context context, Configuration config)
throws InvalidConfigurationException {
final BranchEquivalence eq = context.requires(BranchEquivalence.class);
return new DefaultExecutionAnalysis(program, eq, progressModel);
return new DefaultExecutionAnalysis(program, eq);
}
}

Expand All @@ -35,9 +35,9 @@ class DefaultExecutionAnalysis implements ExecutionAnalysis {
private final ProgressModel.Hierarchy progressModel;
private final Thread lowestIdThread; // For HSA

public DefaultExecutionAnalysis(Program program, BranchEquivalence eq, ProgressModel.Hierarchy progressModel) {
public DefaultExecutionAnalysis(Program program, BranchEquivalence eq) {
this.eq = eq;
this.progressModel = progressModel;
this.progressModel = program.getProgressModel();

this.lowestIdThread = program.getThreads().stream().min(Comparator.comparingInt(Thread::getId)).get();
}
Expand Down
Loading