Skip to content

Add support for C26 atomic reductions (without compiler mappings) #985

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
ThomasHaas wants to merge 7 commits into
base: development
Choose a base branch
from
Open

Add support for C26 atomic reductions (without compiler mappings) #985

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
c6c73c8
Prototype support for atomic modify-write operations
hernan-poncedeleon Jul 17, 2025
413b210
Add c26 header for atomic (reduction) ops
ThomasHaas Feb 12, 2026
ba69de3
Rename C26 reduction operators
ThomasHaas Feb 16, 2026
dfea4c6
Add min/max operators to C
ThomasHaas Feb 16, 2026
38cdfdd
Make the loads of atomic_store_op compilation atomic, even though the…
ThomasHaas Feb 17, 2026
497ae55
Fix accidental compilation error
ThomasHaas Feb 17, 2026
1ca78bc
Noreturn -> NORETURN
hernan-poncedeleon Feb 25, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 14 additions & 0 deletions dartagnan/src/main/antlr4/C11Lexer.g4
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,3 +21,17 @@ C11AtomicXorExplicit : 'atomic_fetch_xor_explicit';
C11AtomicXor : 'atomic_fetch_xor';
C11AtomicAndExplicit : 'atomic_fetch_and_explicit';
C11AtomicAnd : 'atomic_fetch_and';
C11StoreAddExplicit : 'atomic_store_add_explicit';
C11StoreAdd : 'atomic_store_add';
C11StoreSubExplicit : 'atomic_store_sub_explicit';
C11StoreSub : 'atomic_store_sub';
C11StoreOrExplicit : 'atomic_store_or_explicit';
C11StoreOr : 'atomic_store_or';
C11StoreXorExplicit : 'atomic_store_xor_explicit';
C11StoreXor : 'atomic_store_xor';
C11StoreAndExplicit : 'atomic_store_and_explicit';
C11StoreAnd : 'atomic_store_and';
C11StoreMinExplicit : 'atomic_store_min_explicit';
C11StoreMin : 'atomic_store_min';
C11StoreMaxExplicit : 'atomic_store_max_explicit';
C11StoreMax : 'atomic_store_max';
15 changes: 15 additions & 0 deletions dartagnan/src/main/antlr4/LitmusC.g4
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -179,6 +179,21 @@ nre locals [IntBinaryOp op, String mo, String name]
| AtomicInc LPar address = re RPar {$op = IntBinaryOp.ADD;}
| AtomicDec LPar address = re RPar {$op = IntBinaryOp.SUB;}) # nreAtomicOp

| ( C11StoreAddExplicit LPar address = re Comma value = re Comma c11Mo (Comma openCLScope)? RPar {$op = IntBinaryOp.ADD;}
| C11StoreAdd LPar address = re Comma value = re (Comma openCLScope)? RPar {$op = IntBinaryOp.ADD;}
| C11StoreSubExplicit LPar address = re Comma value = re Comma c11Mo (Comma openCLScope)? RPar {$op = IntBinaryOp.SUB;}
| C11StoreSub LPar address = re Comma value = re (Comma openCLScope)? RPar {$op = IntBinaryOp.SUB;}
| C11StoreAndExplicit LPar address = re Comma value = re Comma c11Mo (Comma openCLScope)? RPar {$op = IntBinaryOp.AND;}
| C11StoreAnd LPar address = re Comma value = re (Comma openCLScope)? RPar {$op = IntBinaryOp.AND;}
| C11StoreOrExplicit LPar address = re Comma value = re Comma c11Mo (Comma openCLScope)? RPar {$op = IntBinaryOp.OR;}
| C11StoreOr LPar address = re Comma value = re (Comma openCLScope)? RPar {$op = IntBinaryOp.OR;}
| C11StoreXorExplicit LPar address = re Comma value = re Comma c11Mo (Comma openCLScope)? RPar {$op = IntBinaryOp.XOR;}
| C11StoreXor LPar address = re Comma value = re (Comma openCLScope)? RPar {$op = IntBinaryOp.XOR;}
| C11StoreMinExplicit LPar address = re Comma value = re Comma c11Mo (Comma openCLScope)? RPar {$op = IntBinaryOp.SMIN;}
| C11StoreMin LPar address = re Comma value = re (Comma openCLScope)? RPar {$op = IntBinaryOp.SMIN;}
| C11StoreMaxExplicit LPar address = re Comma value = re Comma c11Mo (Comma openCLScope)? RPar {$op = IntBinaryOp.SMAX;}
| C11StoreMax LPar address = re Comma value = re (Comma openCLScope)? RPar {$op = IntBinaryOp.SMAX;}) # nreC11AtomicOp

| ( AtomicSet LPar address = re Comma value = re RPar {$mo = Linux.MO_ONCE;}
| AtomicSetRelease LPar address = re Comma value = re RPar {$mo = Linux.MO_RELEASE;}
| SmpStoreRelease LPar address = re Comma value = re RPar {$mo = Linux.MO_RELEASE;}
Expand Down
7 changes: 7 additions & 0 deletions dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusC.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -534,6 +534,13 @@ public Object visitNreAtomicOp(LitmusCParser.NreAtomicOpContext ctx){
return programBuilder.addChild(currentThread, event);
}

@Override
public Object visitNreC11AtomicOp(LitmusCParser.NreC11AtomicOpContext ctx){
Expression value = returnExpressionOrOne(ctx.value);
Event event = EventFactory.Atomic.newRMWOp(getAddress(ctx.address), value, ctx.op, ctx.c11Mo().mo);
return programBuilder.addChild(currentThread, event);
}

@Override
public Object visitNreStore(LitmusCParser.NreStoreContext ctx){
Expression value = (Expression)ctx.value.accept(this);
Expand Down
4 changes: 4 additions & 0 deletions dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -441,6 +441,10 @@ public static AtomicFetchOp newFADD(Register register, Expression address, Expre
return newFetchOp(register, address, value, IntBinaryOp.ADD, mo);
}

public static AtomicOp newRMWOp(Expression address, Expression value, IntBinaryOp op, String mo) {
return new AtomicOp(address, op, value, mo);
}

public static AtomicFetchOp newIncrement(Register register, Expression address, String mo) {
if (!(register.getType() instanceof IntegerType integerType)) {
throw new IllegalArgumentException(
Expand Down
1 change: 1 addition & 0 deletions dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventVisitor.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -83,6 +83,7 @@ public interface EventVisitor<T> {
default T visitAtomicStore(AtomicStore e) { return visitMemEvent(e); }
default T visitAtomicThreadFence(AtomicThreadFence e) { return visitEvent(e); }
default T visitAtomicXchg(AtomicXchg e) { return visitMemEvent(e); }
default T visitAtomicOp(AtomicOp e) { return visitMemEvent(e); }

// ------------------ LLVM Events ------------------
default T visitLlvmCmpXchg(LlvmCmpXchg e) { return visitMemEvent(e); }
Expand Down
4 changes: 3 additions & 1 deletion dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -130,7 +130,9 @@ private C11() {
public static final String MO_ACQUIRE_RELEASE = "ACQ_REL";
public static final String MO_SC = "SC";

public static final String DEFAULT_MO = MO_SC;
public static final String DEFAULT_MO = MO_SC;

public static final String NORETURN = "NORETURN";

public static String intToMo(int i) {
switch (i) {
Expand Down
37 changes: 37 additions & 0 deletions dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicOp.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,37 @@
package com.dat3m.dartagnan.program.event.lang.catomic;

import com.dat3m.dartagnan.expression.Expression;
import com.dat3m.dartagnan.expression.integers.IntBinaryOp;
import com.dat3m.dartagnan.program.Register;
import com.dat3m.dartagnan.program.event.EventVisitor;
import com.dat3m.dartagnan.program.event.common.RMWOpBase;
import com.dat3m.dartagnan.program.event.Tag;
import com.google.common.base.Preconditions;

public class AtomicOp extends RMWOpBase {

public AtomicOp(Expression address, IntBinaryOp operator, Expression operand, String mo) {
super(address, operator, operand, mo);
Preconditions.checkArgument(!mo.isEmpty(), "Atomic events cannot have empty memory order");
addTags(Tag.C11.NORETURN);
}

private AtomicOp(AtomicOp other) {
super(other);
}

@Override
public String defaultString() {
return String.format("atomic_store_%s(*%s, %s, %s)\t### C11", operator.getName(), address, operand, mo);
}

@Override
public AtomicOp getCopy() {
return new AtomicOp(this);
}

@Override
public <T> T accept(EventVisitor<T> visitor) {
return visitor.visitAtomicOp(this);
}
}
53 changes: 51 additions & 2 deletions dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@
import com.dat3m.dartagnan.program.event.functions.ValueFunctionCall;
import com.dat3m.dartagnan.program.event.lang.svcomp.BeginAtomic;
import com.dat3m.dartagnan.program.memory.MemoryObject;
import com.google.common.base.Preconditions;
import com.google.common.collect.ImmutableList;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;
Expand Down Expand Up @@ -208,6 +209,8 @@ public enum Info {
LLVM_MEMCPY("llvm.memcpy", true, true, true, false, Intrinsics::inlineMemCpy),
LLVM_MEMSET("llvm.memset", true, false, true, false, Intrinsics::inlineMemSet),
LLVM_THREADLOCAL("llvm.threadlocal.address.p0", false, false, true, true, Intrinsics::inlineLLVMThreadLocal),
// --------------------------- C26 ---------------------------
C26_ATOMIC_OP("__C26_atomic_op", true, true, true, true, Intrinsics::handleC26AtomicOP),
// --------------------------- LKMM ---------------------------
LKMM_LOAD("__LKMM_load", false, true, true, true, Intrinsics::handleLKMMIntrinsic),
LKMM_STORE("__LKMM_store", true, false, true, true, Intrinsics::handleLKMMIntrinsic),
Expand Down Expand Up @@ -289,15 +292,14 @@ public boolean isEarly() {

private boolean matches(String funcName) {
boolean isPrefix = switch(this) {
case LLVM, LLVM_ASSUME, LLVM_META, LLVM_MEMCPY, LLVM_MEMSET, LLVM_EXPECT, LLVM_OBJECTSIZE -> true;
case LLVM, LLVM_ASSUME, LLVM_META, LLVM_MEMCPY, LLVM_MEMSET, LLVM_EXPECT, LLVM_OBJECTSIZE, C26_ATOMIC_OP -> true;
default -> false;
};
BiPredicate<String, String> matchingFunction = isPrefix ? String::startsWith : String::equals;
return variants.stream().anyMatch(v -> matchingFunction.test(funcName, v));
}
}


@FunctionalInterface
private interface Replacer {
List<Event> replace(Intrinsics self, FunctionCall call);
Expand Down Expand Up @@ -1406,6 +1408,53 @@ private Expression checkIfValueInRangeOfType(Expression value, IntegerType integ
);
}

// --------------------------------------------------------------------------------------------------------
// C26 atomics

private enum COp {
// WARNING: The order here must match with the enum defined in c26.h
C_ADD(IntBinaryOp.ADD),
C_SUB(IntBinaryOp.SUB),
C_AND(IntBinaryOp.AND),
C_OR(IntBinaryOp.OR),
C_XOR(IntBinaryOp.XOR),
C_MIN(IntBinaryOp.SMIN),
C_MAX(IntBinaryOp.SMAX);

private final IntBinaryOp op;
COp(IntBinaryOp op) {
this.op = op;
}
}

private IntBinaryOp toCOp(Expression opCode) {
if (!(opCode instanceof IntLiteral literal)) {
throw new UnsupportedOperationException("Variable op code \"" + opCode + "\"");
}
final COp[] cOps = COp.values();
final int index = literal.getValue().intValueExact();
Preconditions.checkArgument(0 <= index && index < cOps.length, "Invalid op code %s", opCode);
return cOps[index].op;
}

private String toCMemoryOrder(Expression moCode) {
if (!(moCode instanceof IntLiteral literal)) {
throw new UnsupportedOperationException("Variable memory order \"" + moCode + "\"");
}
return Tag.C11.intToMo(literal.getValueAsInt());
}

private List<Event> handleC26AtomicOP(FunctionCall call) {
final Expression address = call.getArguments().get(0);
final Expression value = call.getArguments().get(1);
final Expression opCode = call.getArguments().get(2);
final Expression moCode = call.getArguments().get(3);

return List.of(
EventFactory.Atomic.newRMWOp(address, value, toCOp(opCode), toCMemoryOrder(moCode))
);
}

// --------------------------------------------------------------------------------------------------------
// LKMM intrinsics

Expand Down
20 changes: 20 additions & 0 deletions dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorC11.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -91,6 +91,26 @@ public List<Event> visitAtomicFetchOp(AtomicFetchOp e) {
));
}

@Override
public List<Event> visitAtomicOp(AtomicOp e) {
Expression address = e.getAddress();
String mo = e.getMo();

Register dummyReg = e.getFunction().newRegister(e.getAccessType());
Load load = newRMWLoad(dummyReg, address);
Local localOp = newLocal(dummyReg, expressions.makeIntBinary(dummyReg, e.getOperator(), e.getOperand()));
RMWStore store = newRMWStoreWithMo(load, address, dummyReg, Tag.C11.storeMO(mo));

load.addTags(C11.ATOMIC, Tag.C11.NORETURN); // Note that the load has no mo, but is still atomic!
Copy link
Owner

@hernanponcedeleon hernanponcedeleon Feb 26, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For consistency with visitAtomicFetchOp I would rather use

Load load = newRMWLoadWithMo(dummyReg, address, Tag.C11.loadMO(mo));

and rather than getting the expected ordering guarantees "by chance" as it currently happens for rc11,
let the model explicitly state if NORETURN events should provide order or not.

It also feels strange to have an atomic event with no memory order.

Copy link
Collaborator Author

@ThomasHaas ThomasHaas Feb 26, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't like these consistency arguments... those are different operations. Tag.C11.loadMO(mo) will just be RLX or SC because you cannot specify ACQ/ACQ_REL in the first place.
I think the only really sensible options are: the load has no mo, simply because it shouldn't exist in the first place, or the load has the same mo/tags as the store and the WMM removes the tags.
Anything inbetween seems arbitrary to me.

Copy link
Owner

@hernanponcedeleon hernanponcedeleon Feb 26, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The current solution of hardcoding the atomic tag seems equally arbitrary.

I guess what you are proposing is to completely get rid of Tag.C11.loadMO/storeMO) and simply used the mo from the parsing. This would require the memory model to do some "cleanup" as lkmm does, but then we can get rid of these loadMo/storeMO as we already did for lkmm in #893.

Copy link
Collaborator Author

@ThomasHaas ThomasHaas Feb 26, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The current solution of hardcoding the atomic tag seems equally arbitrary.

The atomic tag is not arbitrary, because the whole operation is an atomic one, even by name atomic_store_XYZ.
And if you look at what our compiler does:

boolean canRace = mo == null || mo.value().equals(C11.NONATOMIC);
e.addTags(canRace ? C11.NONATOMIC : C11.ATOMIC);

then every event must be tagged either way, and NONATOMIC is certainly more wrong than ATOMIC.

I guess what you are proposing is to completely get rid of Tag.C11.loadMO/storeMO) and simply used the mo from the parsing. This would require the memory model to do some "cleanup" as lkmm does, but then we can get rid of these loadMo/storeMO as we already did for lkmm in #893.

I proposed exactly that in #984 or rather suggested it as one possible way to go forward. I think rc11.cat might already adhere to that. That being said, for now, I just took the most natural solution given the current hardcoded one:

  • A load must be generated for data-flow modelling (no way around this)
  • The load must be ignored in data races. Marking it as atomic is natural as it is part of an atomic operation independent of its memory ordering.
  • The load should not provide any orderings -> both plain (no mo) and RLX seem reasonable. Plain is closer to capturing the idea of "the load should not exist" whereas RLX is closer to capturing the idea of "the load exists but it should not give orderings", which is (funnily enough) too much ordering :)

At the end of the day, I'm not the one who writes the C memory models and sets the expectation of what is assumed to happen implicitly and what is assumed to be done in the model.

store.addTags(Tag.C11.NORETURN);

return tagList(e, eventSequence(
load,
localOp,
store
));
}

@Override
public List<Event> visitAtomicLoad(AtomicLoad e) {
return tagList(e, eventSequence(
Expand Down
41 changes: 41 additions & 0 deletions include/c26.h
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,41 @@

typedef enum {
__C26_op_add,
__C26_op_sub,
__C26_op_and,
__C26_op_or,
__C26_op_xor,
__C26_op_min,
__C26_op_max,
} __C26_op;

#define __C26__DECLARE_ATOMIC_OP(type) \
extern void __C26_atomic_op_##type(_Atomic(type)* ptr, type value, __C26_op, memory_order);

__C26__DECLARE_ATOMIC_OP(short)
__C26__DECLARE_ATOMIC_OP(int)
__C26__DECLARE_ATOMIC_OP(long)

#define __SELECT(p) _Generic((p), \
_Atomic(short)* : __C26_atomic_op_short, \
_Atomic(int)* : __C26_atomic_op_int, \
_Atomic(long)* : __C26_atomic_op_long \
)

// NOTE: for min/max we only have the signed version for now.

#define atomic_store_add_explicit(p, v, mo) __SELECT(p)(p, v, __C26_op_add, mo)
#define atomic_store_sub_explicit(p, v, mo) __SELECT(p)(p, v, __C26_op_sub, mo)
#define atomic_store_and_explicit(p, v, mo) __SELECT(p)(p, v, __C26_op_and, mo)
#define atomic_store_or_explicit(p, v, mo) __SELECT(p)(p, v, __C26_op_or, mo)
#define atomic_store_xor_explicit(p, v, mo) __SELECT(p)(p, v, __C26_op_xor, mo)
#define atomic_store_min_explicit(p, v, mo) __SELECT(p)(p, v, __C26_op_min, mo)
#define atomic_store_max_explicit(p, v, mo) __SELECT(p)(p, v, __C26_op_max, mo)

#define atomic_store_add(p, v) __SELECT(p)(p, v, __C26_op_add, memory_order_seq_cst)
#define atomic_store_sub(p, v) __SELECT(p)(p, v, __C26_op_sub, memory_order_seq_cst)
#define atomic_store_and(p, v) __SELECT(p)(p, v, __C26_op_and, memory_order_seq_cst)
#define atomic_store_or(p, v) __SELECT(p)(p, v, __C26_op_or, memory_order_seq_cst)
#define atomic_store_xor(p, v) __SELECT(p)(p, v, __C26_op_xor, memory_order_seq_cst)
#define atomic_store_min(p, v) __SELECT(p)(p, v, __C26_op_min, memory_order_seq_cst)
#define atomic_store_max(p, v) __SELECT(p)(p, v, __C26_op_max, memory_order_seq_cst)