From c23fe23875d652a862ea65c4ce47973755129d61 Mon Sep 17 00:00:00 2001 From: Tianrui Zheng Date: Wed, 4 Dec 2024 13:07:25 +0100 Subject: [PATCH] Optimize ThreadModel Signed-off-by: Tianrui Zheng --- .../main/java/com/dat3m/dartagnan/Dartagnan.java | 6 ++++-- .../dartagnan/verification/model/ThreadModel.java | 10 ++++------ .../model/event/DefaultEventModel.java | 2 +- .../verification/model/event/EventModel.java | 2 +- .../witness/graphviz/ExecutionGraphVisualizer.java | 14 ++++++++++---- 5 files changed, 20 insertions(+), 14 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index b97e2d60ec..644a4a9ecd 100644 --- 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 index 09f6a44fd1..3bd88b4ca3 100644 --- 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 getEventModels() { public List getVisibleEventModels() { return eventList.stream().filter(e -> e.isVisible()).toList(); } - - public List getEventModelsToShow() { - return eventList.stream() - .filter(e -> e.isVisible() || e.isLocal() || e.isAssert()) - .toList(); - } } \ No newline at end of file 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 index b8c50cd48b..a719d100d3 100644 --- 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 index 7f4d55a3d3..843dd1b99f 100644 --- 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 { 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 index 1f387025fa..6667e004b0 100644 --- 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 filter = getFilter(PO); for (ThreadModel tm : model.getThreadModels()) { - List eventsToShow = tm.getEventModelsToShow(); + List 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 threadEvents = tm.getEventModelsToShow(); + List 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()),