Remove PTHREAD tag and fix thread id in witness builder (#599)

* Remove Tag.PTHREAD * Fix thread id in witness builder --------- Signed-off-by: Hernan Ponce de Leon <[email protected]> Co-authored-by: Hernan Ponce de Leon <[email protected]>
hernanponcedeleon · Jan 10, 2024 · 9ee7db6 · 9ee7db6
1 parent c1371f9
commit 9ee7db6
Show file tree

Hide file tree

Showing 5 changed files with 46 additions and 27 deletions.
diff --git 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<Tuple> computeThreadTuples(EventGraph maySet, EquivalenceClass<Thread> symmClass, Thread thread) {
         List<Tuple> tuples = new ArrayList<>();
+        List<MemoryCoreEvent> 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
@@ -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<MemoryCoreEvent> 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
@@ -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
@@ -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<MemoryCoreEvent> creates = new ArrayList<>();
+        for (Thread thread : program.getThreads()) {
+            List<MemoryCoreEvent> spawned = thread.getSpawningEvents();
+            if(spawned.size() == 2) {
+                creates.add(spawned.get(1));
+            }
+        }
+
         try (Model model = prover.getModel()) {
-            List<Event> execution = reOrderBasedOnAtomicity(context.getTask().getProgram(), getSCExecutionOrder(model));
+            List<Event> 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
@@ -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<MemoryCoreEvent> 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);
+                    }
                 }
             }