diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/SymmetryEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/SymmetryEncoder.java index 15bd147561..df6b2afc6e 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/SymmetryEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/SymmetryEncoder.java @@ -3,8 +3,8 @@ import com.dat3m.dartagnan.program.Thread; import com.dat3m.dartagnan.program.analysis.BranchEquivalence; import com.dat3m.dartagnan.program.analysis.ThreadSymmetry; -import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.core.MemoryCoreEvent; import com.dat3m.dartagnan.utils.equivalence.EquivalenceClass; import com.dat3m.dartagnan.wmm.Wmm; import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis; @@ -144,8 +144,9 @@ private BooleanFormula encodeSymmetryBreakingOnClass(EventGraph maySet, Encoding private List computeThreadTuples(EventGraph maySet, EquivalenceClass symmClass, Thread thread) { List tuples = new ArrayList<>(); + List spawned = thread.getSpawningEvents(); maySet.apply((a, b) -> { - if (!a.hasTag(Tag.C11.PTHREAD) && !b.hasTag(Tag.C11.PTHREAD) + if (!spawned.contains(a) && !spawned.contains(b) && a.getThread() == thread && symmClass.contains(b.getThread())) { tuples.add(new Tuple(a, b)); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/Thread.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/Thread.java index 391088cdb0..b9c3c370c3 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/Thread.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/Thread.java @@ -1,6 +1,10 @@ package com.dat3m.dartagnan.program; import com.dat3m.dartagnan.expression.type.FunctionType; +import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.core.Load; +import com.dat3m.dartagnan.program.event.core.MemoryCoreEvent; +import com.dat3m.dartagnan.program.event.core.Store; import com.dat3m.dartagnan.program.event.core.threading.ThreadStart; import com.google.common.base.Preconditions; @@ -61,4 +65,20 @@ public ThreadStart getEntry() { public String toString() { return String.format("T%d:%s", id, name); } + + public List getSpawningEvents() { + final ThreadStart start = getEntry(); + if (!start.isSpawned()) { + return List.of(); + } + + Event cur = start; + while (!(cur instanceof Load startLoad)) { cur = cur.getSuccessor(); } + cur = start.getCreator(); + while (!(cur instanceof Store startStore)) { cur = cur.getSuccessor(); } + + assert startStore.getAddress().equals(startLoad.getAddress()); + + return List.of(startLoad, startStore); + } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java index 47951e886b..cc39f27971 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java @@ -125,8 +125,6 @@ private C11() { public static final String MO_ACQUIRE_RELEASE = "ACQ_REL"; public static final String MO_SC = "SC"; - public static final String PTHREAD = "__PTHREAD"; - public static String intToMo(int i) { switch (i) { case 0: return MO_RELAXED; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessBuilder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessBuilder.java index 5d279f8b6d..c11f364e3d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessBuilder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessBuilder.java @@ -7,6 +7,7 @@ import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.core.Assert; import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.core.MemoryCoreEvent; import com.dat3m.dartagnan.program.event.core.Store; import com.dat3m.dartagnan.program.event.lang.svcomp.EndAtomic; import com.dat3m.dartagnan.program.event.metadata.SourceLocation; @@ -29,8 +30,6 @@ import java.util.stream.Collectors; import static com.dat3m.dartagnan.configuration.OptionNames.WITNESS_ORIGINAL_PROGRAM_PATH; -import static com.dat3m.dartagnan.program.event.Tag.C11.PTHREAD; -import static com.dat3m.dartagnan.program.event.Tag.WRITE; import static com.dat3m.dartagnan.utils.Result.FAIL; import static com.dat3m.dartagnan.witness.EdgeAttributes.*; import static com.dat3m.dartagnan.witness.GraphAttributes.*; @@ -91,7 +90,7 @@ private static String getLtlPropertyFromSummary(String summary) { public WitnessGraph build() { for (Thread t : context.getTask().getProgram().getThreads()) { for (Event e : t.getEntry().getSuccessors()) { - eventThreadMap.put(e, t.getId() - 1); + eventThreadMap.put(e, t.getId()); } } @@ -131,8 +130,19 @@ public WitnessGraph build() { return graph; } + Program program = context.getTask().getProgram(); + + // Compute stores related to thread spawning + List creates = new ArrayList<>(); + for (Thread thread : program.getThreads()) { + List spawned = thread.getSpawningEvents(); + if(spawned.size() == 2) { + creates.add(spawned.get(1)); + } + } + try (Model model = prover.getModel()) { - List execution = reOrderBasedOnAtomicity(context.getTask().getProgram(), getSCExecutionOrder(model)); + List execution = reOrderBasedOnAtomicity(program, getSCExecutionOrder(model)); for (int i = 0; i < execution.size(); i++) { Event e = execution.get(i); @@ -148,9 +158,7 @@ public WitnessGraph build() { edge.addAttribute(THREADID.toString(), valueOf(eventThreadMap.get(e))); edge.addAttribute(STARTLINE.toString(), valueOf(cLine)); - // End is also WRITE and PTHREAD, but it does not have - // CLines and thus won't create an edge (as expected) - if (e.hasTag(WRITE) && e.hasTag(PTHREAD)) { + if (creates.contains(e)) { edge.addAttribute(CREATETHREAD.toString(), valueOf(threads)); threads++; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/RelationAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/RelationAnalysis.java index b929aeee4d..6df95832b0 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/RelationAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/RelationAnalysis.java @@ -768,22 +768,14 @@ public Knowledge visitReadFrom(Relation rel) { // Here we add must-rf edges between loads/stores that synchronize threads. for (Thread thread : program.getThreads()) { - final ThreadStart start = thread.getEntry(); - if (!start.isSpawned()) { - continue; - } - - // Must-rf edge for thread spawning - Event cur = start; - while (!(cur instanceof Load startLoad)) { cur = cur.getSuccessor(); } - cur = start.getCreator(); - while (!(cur instanceof Store startStore)) { cur = cur.getSuccessor(); } - - assert startStore.getAddress().equals(startLoad.getAddress()); - - must.add(startStore, startLoad); - if (eq.isImplied(startLoad, startStore)) { - may.removeIf((e1, e2) -> e2 == startLoad && e1 != startStore); + List spawned = thread.getSpawningEvents(); + if(spawned.size() == 2) { + MemoryCoreEvent startLoad = spawned.get(0); + MemoryCoreEvent startStore = spawned.get(1); + must.add(startStore, startLoad); + if (eq.isImplied(startLoad, startStore)) { + may.removeIf((e1, e2) -> e2 == startLoad && e1 != startStore); + } } }