Refactor EventFactory, Compilers and Parsers by xeren · Pull Request #1009 · hernanponcedeleon/Dat3M

xeren · 2026-03-13T11:50:15Z

Mostly cleans up some imports, but also

outlines some memory barrier generations in compilers.
outlines uses of ProgramBuilder.addChild in litmus parsers.
integrates FenceNameRepository into EventFactory

Modifications to `EventFactory`

Added

AArch64.newRMWLoadExclusive, AArch64.newRMWStoreExclusive
X86.newLoadFence, newStoreFence (still not implemented, but merges two places)
RISCV.newRMWLoadExclusive
Power.newRMWLoadExclusive

Modified

newRMWStoreExclusive, newRMWStoreExclusiveWithMo
AArch64.newDmbBarrier, etc.
AArch64.newBarrier(String,String) (moved from newFenceOpt)
RISCV.newRMWStoreConditional

hernanponcedeleon · 2026-03-23T14:48:27Z

@xeren can you please rebase and fix the conflicts?

…actory # Conflicts: # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusC.java # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPTX.java # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusRISCV.java # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusVulkan.java # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusX86.java # dartagnan/src/test/java/com/dat3m/dartagnan/others/miscellaneous/AnalysisTest.java

hernanponcedeleon

Why are you adding newRMWLoadExclusive for each arch if they all end up calling the general case? While I could see an argument in the factory for having the method for each arch, we do have other "common" events that use a single method, e.g. newRMWStoreExclusiveWithMo

hernanponcedeleon · 2026-03-25T19:21:52Z

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java

-                        AArch64.DSB.newISHLDBarrier() :
-                        null;
+        Event fence = switch (e.getMo()) {
+            case Tag.C11.MO_RELEASE, Tag.C11.MO_SC -> AArch64.newDmbIshBarrier();


You are missing the mo.equals(C11.MO_ACQUIRE_RELEASE) case

ThomasHaas · 2026-03-26T15:03:39Z

Why are you adding newRMWLoadExclusive for each arch if they all end up calling the general case? While I could see an argument in the factory for having the method for each arch, we do have other "common" events that use a single method, e.g. newRMWStoreExclusiveWithMo

I agree with you but maybe from a different point of view. I think it becomes more and more unclear of whether a XYZ.newEvent factory method generates a core event or not. For parsers, you want to NOT generate core events to support compilation(*), but for the Compilation passes you need to ensure to generate only core events.
I think this is particularly true for the C11.newThreadFence events which should NOT be called by the parser (for the most part) and only during Compilation. And those can reasonably well be moved in the dedicated compilation pass.
For example, the LKMM compiler has some helper methods for the lowering that are not otherwise exposed to parsers/other callers.

(*) It is fine to generate core events from the parser, but not if you intend to support compilation to other targets on those events (at least in our current architecture).

Fix missing tag.

xeren · 2026-03-26T18:52:28Z

With the different newRMWLoadExclusive methods, I wanted to group all the usages in the program target-wise. It should have made them easier to be altered per-architecture. Ideally, Common, newRMWLoadExclusive, newLoadWithMo, newStoreWithMo and newFence are never used directly by parsers. As you noticed, my refactoring was incomplete.

ThomasHaas · 2026-04-02T09:28:25Z

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusC.java

+    private Expression addCmpXchg(Register register, Expression address, Expression expectedAddress, Expression value,
+            String mo, boolean strong, OpenCLScopeContext scope, ParserRuleContext ctx) {
+        final Event event = EventFactory.Atomic.newCompareExchange(register, address, expectedAddress, value, mo, strong);
+        addScopeTag(event, scope);
+        append(event, ctx);
        return register;


I suggest to not return the register as it is totally unclear why this function should do that.
I would rather have the call-sites explicitly returning the register.

ThomasHaas · 2026-04-02T09:30:34Z

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusC.java

+    private Object append(Event event, ParserRuleContext ctx) {
+        final int line = ctx.getStart().getLine();
+        return programBuilder.addChild(currentThread, event, line);
+    }


The return type should be as specific as possible, i.e., Event.

ThomasHaas · 2026-04-02T09:31:45Z

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java

+    private Object append(Event event, ParserRuleContext ctx) {
+        return programBuilder.addChild(mainThread, event, ctx.getStart().getLine());
+    }


Return type Event

ThomasHaas · 2026-04-02T09:32:32Z

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPTX.java

+    private Object append(Event event, ParserRuleContext ctx) {
+        return programBuilder.addChild(mainThread, event, ctx.getStart().getLine());
+    }


Return type Event

ThomasHaas · 2026-04-02T09:33:18Z

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusRISCV.java

+    private Object append(Event event, ParserRuleContext ctx) {
+        return programBuilder.addChild(mainThread, event, ctx.getStart().getLine());
+    }


Return type Event

ThomasHaas · 2026-04-02T10:12:12Z

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java

+        public static GenericVisibleEvent newThreadFenceAcquire() {
+            return newThreadFence(Tag.C11.MO_ACQUIRE);
+        }
+
+        public static GenericVisibleEvent newThreadFenceRelease() {
+            return newThreadFence(Tag.C11.MO_RELEASE);
+        }
+
+        public static GenericVisibleEvent newThreadFenceAcquireRelease() {
+            return newThreadFence(Tag.C11.MO_ACQUIRE_RELEASE);
+        }
+
+        public static GenericVisibleEvent newThreadFenceSequentiallyConsistent() {
+            return newThreadFence(Tag.C11.MO_SC);
+        }


I don't see much benefit in these 4 functions. They are not really much cleaner just than calling newThreadFence(Tag.C11.MO_XYZ)

ThomasHaas · 2026-04-02T10:23:11Z

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java

+        Register statusReg = strong ? null : e.getFunction().newRegister("status(" + e.getLocalId() + ")", types.getBooleanType());
+        ExecutionStatus optionalExecStatus = strong ? null : newExecutionStatus(statusReg, storeValue);
+        Local optionalUpdateCasCmpResult = strong ? null : newLocal(booleanResultRegister, expressions.makeNot(statusReg));


Just FYI, eventSequence can actually take nested lists as input and it will flatten them.
So one could write:

List<Event> optional = strong ? List.of() : List.of( newExectutionStatus(...), newLocal(...) );

and then use the optional list as input to eventSequence. I don't know whether it's cleaner though.

Actually, I originally added this feature because I wanted to use it for fake control dependencies, where newFakeCtrlDep(Register reg) would return both the jump and the label... Well, we never used this feature and I believe that, except for me, probably no one knew that eventSequence could do this :P.

ThomasHaas · 2026-04-02T10:27:14Z

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPower.java

+        Event optionalBarrierBefore = switch (e.getMo()) {
+            case C11.MO_SC -> leadingSync() ? newSync() : newLwSync();
+            case C11.MO_RELEASE -> newLwSync();
+            default -> null;
+        };


You added optionalBarrierBefore/After methods that you could use here.
I think you decided halfway during the changes to add the helper function but forgot to use it for the already changed code :P

ThomasHaas · 2026-04-02T10:33:44Z

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorRISCV.java

+        Load load = newRMWLoadExclusive(dummy, address, "");
        Local localOp = newLocal(dummy, expressions.makeIntBinary(dummy, e.getOperator(), e.getOperand()));
-        Store store = newRMWStoreExclusiveWithMo(address, dummy, true, mo.equals(Tag.Linux.MO_MB) ? Tag.RISCV.MO_REL : "");
+        Store store = newRMWStoreExclusiveWithMo(address, dummy, true, false, storeMo);


This should be a newRMWStoreConditional, no?

ThomasHaas · 2026-04-02T10:34:04Z

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorRISCV.java

                newAssume(expressions.makeEQ(dummy, zero)),
-                newRMWStoreExclusive(e.getLock(), one, true),
-                RISCV.newRRWFence()
+                newRMWStoreExclusive(e.getLock(), one, true, false),


Same here: conditional store

xeren added 2 commits March 13, 2026 11:18

Refactor

595744e

fixup! Refactor

62a9f58

hernanponcedeleon reviewed Mar 25, 2026

View reviewed changes

xeren added 4 commits March 26, 2026 18:35

fixup! Refactor

952ad54

Fix missing tag.

Move newRMWLoadExclusive from EventFactory to compilers

b6d6ab2

fixup! Move newRMWLoadExclusive from EventFactory to compilers

0385200

fixup! Move newRMWLoadExclusive from EventFactory to compilers

ebd62db

xeren added 2 commits March 26, 2026 22:34

Refactor VisitorLitmusAArch64

c3acefb

fixup! Refactor VisitorLitmusAArch64

b82a538

ThomasHaas reviewed Apr 2, 2026

View reviewed changes

Conversation

xeren commented Mar 13, 2026

Modifications to EventFactory

Added

Modified

Uh oh!

hernanponcedeleon commented Mar 23, 2026

Uh oh!

hernanponcedeleon left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ThomasHaas commented Mar 26, 2026

Uh oh!

xeren commented Mar 26, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Modifications to `EventFactory`