Optimize ThreadModel

Signed-off-by: Tianrui Zheng <[email protected]>
hernanponcedeleon · Dec 4, 2024 · c23fe23 · c23fe23
1 parent 8cf4620
commit c23fe23
Show file tree

Hide file tree

Showing 5 changed files with 20 additions and 14 deletions.
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java
@@ -240,8 +240,10 @@ public static File generateExecutionGraphFile(VerificationTask task, ProverEnvir
         // we get some data flow information by observing the edge
         // FR edges only give ordering information which is known if the pair is also in PO
         // CO edges only give ordering information which is known if the pair is also in PO
-        return generateGraphvizFile(encodingContext, prover.getModel(), 1, (x, y) -> true, (x, y) -> !x.getThread().equals(y.getThread()),
-                (x, y) -> !x.getThread().equals(y.getThread()), getOrCreateOutputDirectory() + "/", name,
+        return generateGraphvizFile(encodingContext, prover.getModel(), 1, (x, y) -> true,
+                (x, y) -> !x.getThreadModel().getThread().equals(y.getThreadModel().getThread()),
+                (x, y) -> !x.getThreadModel().getThread().equals(y.getThreadModel().getThread()),
+                getOrCreateOutputDirectory() + "/", name,
                 synContext, witnessType.convertToPng());
     }
 

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ThreadModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ThreadModel.java
@@ -22,6 +22,10 @@ public void addEvent(EventModel event) {
         eventList.add(event);
     }
 
+    public Thread getThread() {
+        return thread;
+    }
+
     public int getId() {
         return thread.getId();
     }
@@ -37,10 +41,4 @@ public List<EventModel> getEventModels() {
     public List<EventModel> getVisibleEventModels() {
         return eventList.stream().filter(e -> e.isVisible()).toList();
     }
-
-    public List<EventModel> getEventModelsToShow() {
-        return eventList.stream()
-                        .filter(e -> e.isVisible() || e.isLocal() || e.isAssert())
-                        .toList();
-    }
 }
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/DefaultEventModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/DefaultEventModel.java
@@ -28,7 +28,7 @@ public Event getEvent() {
     }
 
     @Override
-    public ThreadModel getThread() {
+    public ThreadModel getThreadModel() {
         return thread;
     }
 

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/EventModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/EventModel.java
@@ -7,7 +7,7 @@
 public interface EventModel extends Comparable<EventModel> {
     Event getEvent();
 
-    ThreadModel getThread();
+    ThreadModel getThreadModel();
 
     int getId();
 

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ExecutionGraphVisualizer.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ExecutionGraphVisualizer.java
@@ -171,7 +171,10 @@ private ExecutionGraphVisualizer addProgramOrder(ExecutionModelNext model, Strin
         String label = String.format("label=\"%s\"", name);
         BiPredicate<EventModel, EventModel> filter = getFilter(PO);
         for (ThreadModel tm : model.getThreadModels()) {
-            List<EventModel> eventsToShow = tm.getEventModelsToShow();
+            List<EventModel> eventsToShow = tm.getEventModels()
+                                              .stream()
+                                              .filter(e -> e.isVisible() || e.isLocal() || e.isAssert())
+                                              .toList();
             if (eventsToShow.size() <= 1) { continue; }
             for (int i = 1; i < eventsToShow.size(); i++) {
                 EventModel from = eventsToShow.get(i - 1);
@@ -247,7 +250,10 @@ private ExecutionGraphVisualizer addAllThreadPos(ExecutionModelNext model) {
     }
 
     private ExecutionGraphVisualizer addThreadPo(ThreadModel tm, ExecutionModelNext model) {
-        List<EventModel> threadEvents = tm.getEventModelsToShow();
+        List<EventModel> threadEvents = tm.getEventModels()
+                                          .stream()
+                                          .filter(e -> e.isVisible() || e.isLocal() || e.isAssert())
+                                          .toList();
         if (threadEvents.size() <= 1) {
             // This skips init threads.
             return this;
@@ -300,8 +306,8 @@ private String eventToNode(EventModel e) {
         final String callStack = makeContextString(
             synContext.getContextInfo(e.getEvent()).getContextOfType(CallContext.class), " -> \\n");
         final String nodeString = String.format("%s:T%s/E%s\\n%s%s\n%s",
-                e.getThread().getName(),
-                e.getThread().getId(),
+                e.getThreadModel().getName(),
+                e.getThreadModel().getId(),
                 e.getEvent().getGlobalId(),
                 callStack.isEmpty() ? callStack : callStack + " -> \\n",
                 getSourceLocationString(e.getEvent()),