Skip to content

Commit

Permalink
Replace CAATs RangeIdentityGraph by a general ProjectionIdentityGraph…
Browse files Browse the repository at this point in the history 
… (can do Range and Domain)

Remove default fallback to StaticDefaultWMMGraph for unknown relations in ExecutionGraph.
This fallback was dangerous. Instead, the RefinementSolver shall cut unknown relations.
  • Loading branch information
@ThomasHaas
ThomasHaas committed Nov 21, 2024
1 parent e84b166 commit 336e853
Show file tree
Hide file tree
Showing 5 changed files with 46 additions and 19 deletions.
2 changes: 1 addition & 1 deletion ...agnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/misc/PredicateVisitor.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ public interface PredicateVisitor<TRet, TData, TContext> {
default TRet visitCartesian(RelationGraph graph, TData data, TContext context) { return visitGraph(graph, data, context); }
default TRet visitInverse(RelationGraph graph, TData data, TContext context) { return visitGraph(graph, data, context); }
default TRet visitSetIdentity(RelationGraph graph, TData data, TContext context) { return visitGraph(graph, data, context); }
default TRet visitRangeIdentity(RelationGraph graph, TData data, TContext context) { return visitGraph(graph, data, context); }
default TRet visitProjectionIdentity(RelationGraph graph, TData data, TContext context) { return visitGraph(graph, data, context); }
default TRet visitReflexiveClosure(RelationGraph graph, TData data, TContext context) { return visitGraph(graph, data, context); }
default TRet visitTransitiveClosure(RelationGraph graph, TData data, TContext context) { return visitGraph(graph, data, context); }
default TRet visitRecursiveGraph(RelationGraph graph, TData data, TContext context) { return visitGraph(graph, data, context); }
Expand Down
21 changes: 17 additions & 4 deletions ...ionGraphs/derived/RangeIdentityGraph.java → ...aphs/derived/ProjectionIdentityGraph.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,21 +12,34 @@
import java.util.List;
import java.util.stream.Collectors;

public class RangeIdentityGraph extends MaterializedGraph {
public class ProjectionIdentityGraph extends MaterializedGraph {

public enum Dimension {
DOMAIN,
RANGE
}

private final RelationGraph inner;
private final Dimension dimension;

@Override
public List<RelationGraph> getDependencies() {
return List.of(inner);
}

public RangeIdentityGraph(RelationGraph inner) {
public Dimension getProjectionDimension() { return dimension; }

public ProjectionIdentityGraph(RelationGraph inner, Dimension dimension) {
this.inner = inner;
this.dimension = dimension;
}

private Edge derive(Edge e) {
return new Edge(e.getSecond(), e.getSecond(), e.getTime(), e.getDerivationLength() + 1);
int id = switch (this.dimension) {
case RANGE -> e.getSecond();
case DOMAIN -> e.getFirst();
};
return new Edge(id, id, e.getTime(), e.getDerivationLength() + 1);
}

@Override
Expand All @@ -50,7 +63,7 @@ public Collection<Edge> forwardPropagate(CAATPredicate changedSource, Collection

@Override
public <TRet, TData, TContext> TRet accept(PredicateVisitor<TRet, TData, TContext> visitor, TData data, TContext context) {
return visitor.visitRangeIdentity(this, data, context);
return visitor.visitProjectionIdentity(this, data, context);
}

}
16 changes: 11 additions & 5 deletions dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/reasoning/Reasoner.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@
import com.dat3m.dartagnan.solver.caat.predicates.misc.PredicateVisitor;
import com.dat3m.dartagnan.solver.caat.predicates.relationGraphs.Edge;
import com.dat3m.dartagnan.solver.caat.predicates.relationGraphs.RelationGraph;
import com.dat3m.dartagnan.solver.caat.predicates.relationGraphs.derived.ProjectionIdentityGraph;
import com.dat3m.dartagnan.solver.caat.predicates.sets.Element;
import com.dat3m.dartagnan.solver.caat.predicates.sets.SetPredicate;
import com.dat3m.dartagnan.utils.logic.Conjunction;
Expand Down Expand Up @@ -220,19 +221,24 @@ public Conjunction<CAATLiteral> visitSetIdentity(RelationGraph graph, Edge edge,
}

@Override
public Conjunction<CAATLiteral> visitRangeIdentity(RelationGraph graph, Edge edge, Void unused) {
public Conjunction<CAATLiteral> visitProjectionIdentity(RelationGraph graph, Edge edge, Void unused) {
assert edge.isLoop();

RelationGraph inner = (RelationGraph) graph.getDependencies().get(0);
for (Edge inEdge : inner.inEdges(edge.getSecond())) {
ProjectionIdentityGraph.Dimension dim = ((ProjectionIdentityGraph)graph).getProjectionDimension();
Iterable<Edge> edges = switch (dim) {
case RANGE -> inner.inEdges(edge.getSecond());
case DOMAIN -> inner.outEdges(edge.getFirst());
};
for (Edge e : edges) {
// We use the first edge we find
if (inEdge.getDerivationLength() < edge.getDerivationLength()) {
Conjunction<CAATLiteral> reason = computeReason(inner, inEdge);
if (e.getDerivationLength() < edge.getDerivationLength()) {
Conjunction<CAATLiteral> reason = computeReason(inner, e);
assert !reason.isFalse();
return reason;
}
}
throw new IllegalStateException("RangeIdentityGraph: No matching edge is found");
throw new IllegalStateException("ProjectionIdentityGraph: No matching edge is found");
}

@Override
Expand Down
17 changes: 11 additions & 6 deletions dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -230,11 +230,15 @@ private RelationGraph createGraphFromRelation(Relation rel) {
graph = new ProgramOrderGraph();
} else if (relClass == Coherence.class) {
graph = new CoherenceGraph();
} else if (relClass == Inverse.class || relClass == TransitiveClosure.class || relClass == RangeIdentity.class) {
} else if (relClass == RangeIdentity.class || relClass == DomainIdentity.class) {
RelationGraph g = getOrCreateGraphFromRelation(dependencies.get(0));
graph = relClass == Inverse.class ? new InverseGraph(g) :
relClass == TransitiveClosure.class ? new TransitiveGraph(g) :
new RangeIdentityGraph(g);
ProjectionIdentityGraph.Dimension dim = relClass == RangeIdentity.class ?
ProjectionIdentityGraph.Dimension.RANGE :
ProjectionIdentityGraph.Dimension.DOMAIN;
graph = new ProjectionIdentityGraph(g, dim);
} else if (relClass == Inverse.class || relClass == TransitiveClosure.class) {
RelationGraph g = getOrCreateGraphFromRelation(dependencies.get(0));
graph = relClass == Inverse.class ? new InverseGraph(g) : new TransitiveGraph(g);
} else if (relClass == Union.class || relClass == Intersection.class) {
RelationGraph[] graphs = new RelationGraph[dependencies.size()];
for (int i = 0; i < graphs.length; i++) {
Expand Down Expand Up @@ -264,8 +268,9 @@ private RelationGraph createGraphFromRelation(Relation rel) {
} else if (relClass == Empty.class) {
graph = new EmptyGraph();
} else {
// This is a fallback for all unimplemented static graphs
graph = new StaticDefaultWMMGraph(rel, ra);
final String error = String.format("Cannot handle relation %s with definition of type %s.",
rel, relClass.getSimpleName());
throw new UnsupportedOperationException(error);
}

graph.setName(rel.getNameOrTerm());
Expand Down
9 changes: 6 additions & 3 deletions dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,11 +11,11 @@
import com.dat3m.dartagnan.program.analysis.alias.AliasAnalysis;
import com.dat3m.dartagnan.program.event.Event;
import com.dat3m.dartagnan.program.event.MemoryEvent;
import com.dat3m.dartagnan.program.event.Tag;
import com.dat3m.dartagnan.program.event.core.MemoryCoreEvent;
import com.dat3m.dartagnan.program.event.metadata.OriginalId;
import com.dat3m.dartagnan.program.event.metadata.SourceLocation;
import com.dat3m.dartagnan.program.filter.Filter;
import com.dat3m.dartagnan.program.event.Tag;
import com.dat3m.dartagnan.solver.caat.CAATSolver;
import com.dat3m.dartagnan.solver.caat4wmm.RefinementModel;
import com.dat3m.dartagnan.solver.caat4wmm.Refiner;
Expand Down Expand Up @@ -234,7 +234,7 @@ private void runInternal(SolverContext ctx, ProverWithTracker prover, Verificati
final Refiner refiner = new Refiner(refinementModel);
final Property.Type propertyType = Property.getCombinedType(task.getProperty(), task);

logger.info("Starting encoding using " + ctx.getVersion());
logger.info("Starting encoding using {}", ctx.getVersion());
prover.writeComment("Program encoding");
prover.addConstraint(programEncoder.encodeFullProgram());
prover.writeComment("Memory model (baseline) encoding");
Expand Down Expand Up @@ -491,7 +491,10 @@ private static boolean isUnknownDefinitionForCAAT(Definition def) {
// TODO: We should probably automatically cut all "unknown relation",
// i.e., use a white-list of known relations instead of a blacklist of unknown one's.
return def instanceof LinuxCriticalSections // LKMM
|| def instanceof SyncFence || def instanceof SyncBar || def instanceof SameVirtualLocation; // GPUs
|| def instanceof CASDependency // IMM
// GPUs
|| def instanceof SameScope || def instanceof SyncWith
|| def instanceof SyncFence || def instanceof SyncBar || def instanceof SameVirtualLocation;
}

private static RefinementModel generateRefinementModel(Wmm original) {
Expand Down

0 comments on commit 336e853

Please sign in to comment.