diff --git a/benchmarks/mixed/store-to-load-forwarding1.c b/benchmarks/mixed/store-to-load-forwarding1.c index f7700bae39..d310441d66 100644 --- a/benchmarks/mixed/store-to-load-forwarding1.c +++ b/benchmarks/mixed/store-to-load-forwarding1.c @@ -2,7 +2,8 @@ #include #include // Issue: Store-to-Load Forwarding may cause mixed-size atomic accesses to appear non-atomic. -// Expected: FAIL on ARMv8 +// Expected: PASS on ARMv8, but FAIL on older, unpatched version of ARMv8, see +// https://github.com/herd/herdtools7/commit/2b7921a union { atomic_ushort full; struct { atomic_uchar half0; atomic_uchar half1; }; } lock; diff --git a/cat/aarch64.cat b/cat/aarch64.cat index f5944bad5a..9f5d35c545 100644 --- a/cat/aarch64.cat +++ b/cat/aarch64.cat @@ -65,8 +65,8 @@ let dmb.st = DMB.ISHST | DMB.OSHST | DMB.ST | dsb.st (* Flag any use of shareability options, due to the restrictions above. *) (* flag ~empty (dmb.full | dmb.ld | dmb.st) \ - (DMB.SY | DMB.LD | DMB.ST | DSB.SY | DSB.LD | DSB.ST) - as Assuming-common-inner-shareable-domain + (DMB.SY | DMB.LD | DMB.ST | DSB.SY | DSB.LD | DSB.ST) + as Assuming-common-inner-shareable-domain *) (* Coherence-after *) @@ -83,29 +83,33 @@ let obs = rfe | fre | coe (* Dependency-ordered-before *) let dob = (addr | data) - | ctrl; [W] - | (ctrl | (addr; po)); [ISB]; po; [R] - | addr; po; [W] - | (addr | data); lrs + | ctrl; [W] + | (ctrl | (addr; po)); [ISB]; po; [R] + | addr; po; [W] + | (addr | data); lrs (* Atomic-ordered-before *) let aob = rmw - | [range(rmw)]; lrs; [A | Q] + | [range(rmw)]; lrs; [A | Q] (* Barrier-ordered-before *) let bob = po; [dmb.full]; po - | po; ([A];amo;[L]); po - | [L]; po; [A] - | [R]; po; [dmb.ld]; po - | [A | Q]; po - | [W]; po; [dmb.st]; po; [W] - | po; [L] + | po; ([A];amo;[L]); po + | [L]; po; [A] + | [R \ NoRet]; po; [dmb.ld]; po + | [A | Q]; po + | [W]; po; [dmb.st]; po; [W] + | po; [L] (* Locally-ordered-before *) let lob = lws; si | dob | aob | bob +(** Hazard-ordered-before **) +let haz-ob = + [R]; (po & loc); [R]; si?; [R]; (ca & ext); [W]; si?; [W] + (* Ordered-before *) -let ob = obs; si | lob +let ob = obs; si | lob | haz-ob (* Internal visibility requirement *) acyclic po-loc | ca | rf as internal diff --git a/dartagnan/src/main/antlr4/LitmusAArch64.g4 b/dartagnan/src/main/antlr4/LitmusAArch64.g4 index 1c8f2d4710..7dcafec5b3 100644 --- a/dartagnan/src/main/antlr4/LitmusAArch64.g4 +++ b/dartagnan/src/main/antlr4/LitmusAArch64.g4 @@ -63,7 +63,12 @@ instruction | store | storePair | storeExclusive + // AMOs + | loadOp + | storeOp | swap + | cas + // ----- | cmp | branch | branchRegister @@ -118,11 +123,26 @@ storeExclusive | storeExclusiveInstruction rS32 = register32 Comma rV64 = register64 Comma LBracket address RBracket ; +loadOp + : loadOpInstruction rS32 = register32 Comma rD32 = register32 Comma LBracket address RBracket + | loadOpInstruction rS64 = register64 Comma rD64 = register64 Comma LBracket address RBracket + ; + +storeOp + : storeOpInstruction rS32 = register32 Comma LBracket address RBracket + | storeOpInstruction rS64 = register64 Comma LBracket address RBracket + ; + swap : swapInstruction rS32 = register32 Comma rD32 = register32 Comma LBracket address RBracket | swapInstruction rS64 = register64 Comma rD64 = register64 Comma LBracket address RBracket ; +cas + : casInstruction rS32 = register32 Comma rT32 = register32 Comma LBracket address RBracket + | casInstruction rS64 = register64 Comma rT64 = register64 Comma LBracket address RBracket + ; + fence locals [String opt] : Fence {$opt = "SY";} | Fence FenceOpt {$opt = $FenceOpt.text;} @@ -167,6 +187,76 @@ loadExclusiveInstruction locals [boolean acquire, boolean byteSize, boolean half | LDAXRH {$acquire = true; $halfWordSize = true;} ; +loadOpInstruction + // ADD + : LDADD | LDADDA | LDADDL | LDADDAL + | LDADDH | LDADDAH | LDADDLH | LDADDALH + | LDADDB | LDADDAB | LDADDLB | LDADDALB + // EOR + | LDEOR | LDEORA | LDEORL | LDEORAL + | LDEORH | LDEORAH | LDEORLH | LDEORALH + | LDEORB | LDEORAB | LDEORLB | LDEORALB + // SET + | LDSET | LDSETA | LDSETL | LDSETAL + | LDSETH | LDSETAH | LDSETLH | LDSETALH + | LDSETB | LDSETAB | LDSETLB | LDSETALB + // CLR + | LDCLR | LDCLRA | LDCLRL | LDCLRAL + | LDCLRH | LDCLRAH | LDCLRLH | LDCLRALH + | LDCLRB | LDCLRAB | LDCLRLB | LDCLRALB + // SMIN + | LDSMIN | LDSMINA | LDSMINL | LDSMINAL + | LDSMINH | LDSMINAH | LDSMINLH | LDSMINALH + | LDSMINB | LDSMINAB | LDSMINLB | LDSMINALB + // UMIN + | LDUMIN | LDUMINA | LDUMINL | LDUMINAL + | LDUMINH | LDUMINAH | LDUMINLH | LDUMINALH + | LDUMINB | LDUMINAB | LDUMINLB | LDUMINALB + // SMAX + | LDSMAX | LDSMAXA | LDSMAXL | LDSMAXAL + | LDSMAXH | LDSMAXAH | LDSMAXLH | LDSMAXALH + | LDSMAXB | LDSMAXAB | LDSMAXLB | LDSMAXALB + // UMAX + | LDUMAX | LDUMAXA | LDUMAXL | LDUMAXAL + | LDUMAXH | LDUMAXAH | LDUMAXLH | LDUMAXALH + | LDUMAXB | LDUMAXAB | LDUMAXLB | LDUMAXALB + ; + +storeOpInstruction + // ADD + : STADD | STADDL + | STADDH | STADDLH + | STADDB | STADDLB + // EOR + | STEOR | STEORL + | STEORH | STEORLH + | STEORB | STEORLB + // SET + | STSET | STSETL + | STSETH | STSETLH + | STSETB | STSETLB + // CLR + | STCLR | STCLRL + | STCLRH | STCLRLH + | STCLRB | STCLRLB + // SMIN + | STSMIN | STSMINL + | STSMINH | STSMINLH + | STSMINB | STSMINLB + // UMIN + | STUMIN | STUMINL + | STUMINH | STUMINLH + | STUMINB | STUMINLB + // SMAX + | STSMAX | STSMAXL + | STSMAXH | STSMAXLH + | STSMAXB | STSMAXLB + // UMAX + | STUMAX | STUMAXL + | STUMAXH | STUMAXLH + | STUMAXB | STUMAXLB + ; + storeInstruction locals [boolean release, boolean byteSize, boolean halfWordSize] : STR | STRB {$byteSize = true;} @@ -200,6 +290,21 @@ swapInstruction locals [boolean acquire, boolean release, boolean byteSize, bool | SWPALH {$acquire = true; $release = true; $halfWordSize = true;} ; +casInstruction locals [boolean acquire, boolean release, boolean byteSize, boolean halfWordSize] + : CAS + | CASB {$byteSize = true;} + | CASH {$halfWordSize = true;} + | CASA {$acquire = true;} + | CASAB {$acquire = true; $byteSize = true;} + | CASAH {$acquire = true; $halfWordSize = true;} + | CASL {$release = true;} + | CASLB {$release = true; $byteSize = true;} + | CASLH {$release = true; $halfWordSize = true;} + | CASAL {$acquire = true; $release = true;} + | CASALB {$acquire = true; $release = true; $byteSize = true;} + | CASALH {$acquire = true; $release = true; $halfWordSize = true;} + ; + arithmeticInstruction locals [IntBinaryOp op] : ADD { $op = IntBinaryOp.ADD; } // | ADDS { throw new RuntimeException("Instruction ADDS is not implemented"); } @@ -300,6 +405,7 @@ register32 returns[String id] location : Identifier + | LBracket Identifier RBracket ; immediate @@ -381,6 +487,171 @@ STLXR : 'STLXR' ; STLXRB : 'STLXRB' ; STLXRH : 'STLXRH' ; +// Load Op instructions +// Add +LDADD : 'LDADD' ; +LDADDA : 'LDADDA' ; +LDADDL : 'LDADDL' ; +LDADDAL : 'LDADDAL' ; +LDADDH : 'LDADDH' ; +LDADDAH : 'LDADDAH' ; +LDADDLH : 'LDADDLH' ; +LDADDALH : 'LDADDALH' ; +LDADDB : 'LDADDB' ; +LDADDAB : 'LDADDAB' ; +LDADDLB : 'LDADDLB' ; +LDADDALB : 'LDADDALB' ; +// EOR (XOR) +LDEOR : 'LDEOR' ; +LDEORA : 'LDEORA' ; +LDEORL : 'LDEORL' ; +LDEORAL : 'LDEORAL' ; +LDEORH : 'LDEORH' ; +LDEORAH : 'LDEORAH' ; +LDEORLH : 'LDEORLH' ; +LDEORALH : 'LDEORALH' ; +LDEORB : 'LDEORB' ; +LDEORAB : 'LDEORAB' ; +LDEORLB : 'LDEORLB' ; +LDEORALB : 'LDEORALB' ; +// SET (OR) +LDSET : 'LDSET' ; +LDSETA : 'LDSETA' ; +LDSETL : 'LDSETL' ; +LDSETAL : 'LDSETAL' ; +LDSETH : 'LDSETH' ; +LDSETAH : 'LDSETAH' ; +LDSETLH : 'LDSETLH' ; +LDSETALH : 'LDSETALH' ; +LDSETB : 'LDSETB' ; +LDSETAB : 'LDSETAB' ; +LDSETLB : 'LDSETLB' ; +LDSETALB : 'LDSETALB' ; +// CLR (AND with complement) +LDCLR : 'LDCLR' ; +LDCLRA : 'LDCLRA' ; +LDCLRL : 'LDCLRL' ; +LDCLRAL : 'LDCLRAL' ; +LDCLRH : 'LDCLRH' ; +LDCLRAH : 'LDCLRAH' ; +LDCLRLH : 'LDCLRLH' ; +LDCLRALH : 'LDCLRALH' ; +LDCLRB : 'LDCLRB' ; +LDCLRAB : 'LDCLRAB' ; +LDCLRLB : 'LDCLRLB' ; +LDCLRALB : 'LDCLRALB' ; +// SMIN +LDSMIN : 'LDSMIN' ; +LDSMINA : 'LDSMINA' ; +LDSMINL : 'LDSMINL' ; +LDSMINAL : 'LDSMINAL' ; +LDSMINH : 'LDSMINH' ; +LDSMINAH : 'LDSMINAH' ; +LDSMINLH : 'LDSMINLH' ; +LDSMINALH : 'LDSMINALH' ; +LDSMINB : 'LDSMINB' ; +LDSMINAB : 'LDSMINAB' ; +LDSMINLB : 'LDSMINLB' ; +LDSMINALB : 'LDSMINALB' ; +// UMIN +LDUMIN : 'LDUMIN' ; +LDUMINA : 'LDUMINA' ; +LDUMINL : 'LDUMINL' ; +LDUMINAL : 'LDUMINAL' ; +LDUMINH : 'LDUMINH' ; +LDUMINAH : 'LDUMINAH' ; +LDUMINLH : 'LDUMINLH' ; +LDUMINALH : 'LDUMINALH' ; +LDUMINB : 'LDUMINB' ; +LDUMINAB : 'LDUMINAB' ; +LDUMINLB : 'LDUMINLB' ; +LDUMINALB : 'LDUMINALB' ; +// SMAX +LDSMAX : 'LDSMAX' ; +LDSMAXA : 'LDSMAXA' ; +LDSMAXL : 'LDSMAXL' ; +LDSMAXAL : 'LDSMAXAL' ; +LDSMAXH : 'LDSMAXH' ; +LDSMAXAH : 'LDSMAXAH' ; +LDSMAXLH : 'LDSMAXLH' ; +LDSMAXALH : 'LDSMAXALH' ; +LDSMAXB : 'LDSMAXB' ; +LDSMAXAB : 'LDSMAXAB' ; +LDSMAXLB : 'LDSMAXLB' ; +LDSMAXALB : 'LDSMAXALB' ; +// UMAX +LDUMAX : 'LDUMAX' ; +LDUMAXA : 'LDUMAXA' ; +LDUMAXL : 'LDUMAXL' ; +LDUMAXAL : 'LDUMAXAL' ; +LDUMAXH : 'LDUMAXH' ; +LDUMAXAH : 'LDUMAXAH' ; +LDUMAXLH : 'LDUMAXLH' ; +LDUMAXALH : 'LDUMAXALH' ; +LDUMAXB : 'LDUMAXB' ; +LDUMAXAB : 'LDUMAXAB' ; +LDUMAXLB : 'LDUMAXLB' ; +LDUMAXALB : 'LDUMAXALB' ; + +// Store Op instructions +// Add +STADD : 'STADD' ; +STADDL : 'STADDL' ; +STADDH : 'STADDH' ; +STADDLH : 'STADDLH' ; +STADDB : 'STADDB' ; +STADDLB : 'STADDLB' ; +// EOR (XOR) +STEOR : 'STEOR' ; +STEORL : 'STEORL' ; +STEORH : 'STEORH' ; +STEORLH : 'STEORLH' ; +STEORB : 'STEORB' ; +STEORLB : 'STEORLB' ; +// SET (OR) +STSET : 'STSET' ; +STSETL : 'STSETL' ; +STSETH : 'STSETH' ; +STSETLH : 'STSETLH' ; +STSETB : 'STSETB' ; +STSETLB : 'STSETLB' ; +// CLR (AND with complement) +STCLR : 'STCLR' ; +STCLRL : 'STCLRL' ; +STCLRH : 'STCLRH' ; +STCLRLH : 'STCLRLH' ; +STCLRB : 'STCLRB' ; +STCLRLB : 'STCLRLB' ; +// SMIN +STSMIN : 'STSMIN' ; +STSMINL : 'STSMINL' ; +STSMINH : 'STSMINH' ; +STSMINLH : 'STSMINLH' ; +STSMINB : 'STSMINB' ; +STSMINLB : 'STSMINLB' ; +// UMIN +STUMIN : 'STUMIN' ; +STUMINL : 'STUMINL' ; +STUMINH : 'STUMINH' ; +STUMINLH : 'STUMINLH' ; +STUMINB : 'STUMINB' ; +STUMINLB : 'STUMINLB' ; +// SMAX +STSMAX : 'STSMAX' ; +STSMAXL : 'STSMAXL' ; +STSMAXH : 'STSMAXH' ; +STSMAXLH : 'STSMAXLH' ; +STSMAXB : 'STSMAXB' ; +STSMAXLB : 'STSMAXLB' ; +// UMAX +STUMAX : 'STUMAX' ; +STUMAXL : 'STUMAXL' ; +STUMAXH : 'STUMAXH' ; +STUMAXLH : 'STUMAXLH' ; +STUMAXB : 'STUMAXB' ; +STUMAXLB : 'STUMAXLB' ; + + // Swap word instructions (~ Exchange) SWP : 'SWP' ; @@ -396,6 +667,21 @@ SWPAL : 'SWPAL' ; SWPALB : 'SWPALB' ; SWPALH : 'SWPALH' ; +// CAS instructions + +CAS : 'CAS' ; +CASB : 'CASB' ; +CASH : 'CASH' ; +CASA : 'CASA' ; +CASAB : 'CASAB' ; +CASAH : 'CASAH' ; +CASL : 'CASL' ; +CASLB : 'CASLB' ; +CASLH : 'CASLH' ; +CASAL : 'CASAL' ; +CASALB : 'CASALB' ; +CASALH : 'CASALH' ; + MovInstruction : 'MOV' ; @@ -429,7 +715,7 @@ FenceOpt | 'OSH' | 'osh' // Outer sharable domain only ; -// Bracnch conditions +// Branch conditions EQ : 'EQ'; // Equal NE : 'NE'; // Not equal @@ -437,7 +723,7 @@ CS : 'CS'; // Carry set HS : 'HS'; // Identical to CS CC : 'CC'; // Carry clear LO : 'LO'; // Identical to CC -MI : 'MI'; // Minus or negative result +MI : 'MI'; // Minus or negative result PL : 'PL'; // Positive or zero result VS : 'VS'; // Overflow VC : 'VC'; // No overflow diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionFactory.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionFactory.java index 8f0140f382..9856b693c8 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionFactory.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionFactory.java @@ -119,6 +119,10 @@ public Expression makeGTE(Expression leftOperand, Expression rightOperand, boole return makeIntCmp(leftOperand, signed ? IntCmpOp.GTE : IntCmpOp.UGTE, rightOperand); } + public Expression makeIntNot(Expression operand) { + return makeIntUnary(IntUnaryOp.NOT, operand); + } + public Expression makeNeg(Expression operand) { return makeIntUnary(IntUnaryOp.MINUS, operand); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java index 880eb08671..195bc738fc 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java @@ -9,8 +9,8 @@ import com.dat3m.dartagnan.expression.type.FunctionType; import com.dat3m.dartagnan.expression.type.TypeFactory; import com.dat3m.dartagnan.program.*; -import com.dat3m.dartagnan.program.Thread; import com.dat3m.dartagnan.program.Program.SourceLanguage; +import com.dat3m.dartagnan.program.Thread; import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventFactory; import com.dat3m.dartagnan.program.event.RegWriter; @@ -93,21 +93,25 @@ public static void processAfterParsing(Program program) { public static void replaceZeroRegisters(Program program, List zeroRegNames) { for (Function func : Iterables.concat(program.getThreads(), program.getFunctions())) { - if (func.hasBody()) { - for (String zeroRegName : zeroRegNames) { - Register zr = func.getRegister(zeroRegName); - if (zr != null) { - for (RegWriter rw : func.getEvents(RegWriter.class)) { - if (rw.getResultRegister().equals(zr)) { - Register dummy = rw.getThread().getOrNewRegister("__zeroRegDummy_" + zr.getName(), zr.getType()); - rw.setResultRegister(dummy); - } - } - // This comes after the loop to avoid the renaming in the initialization event - Event initToZero = EventFactory.newLocal(zr, expressions.makeGeneralZero(zr.getType())); - func.getEntry().insertAfter(initToZero); + if (!func.hasBody()) { + continue; + } + + for (String zeroRegName : zeroRegNames) { + Register zr = func.getRegister(zeroRegName); + if (zr == null) { + continue; + } + + for (RegWriter rw : func.getEvents(RegWriter.class)) { + if (rw.getResultRegister().equals(zr)) { + Register dummy = rw.getThread().getOrNewRegister("__zeroRegDummy_" + zr.getName(), zr.getType()); + rw.setResultRegister(dummy); } } + // This comes after the loop to avoid the renaming in the initialization event + Event initToZero = EventFactory.newLocal(zr, expressions.makeGeneralZero(zr.getType())); + func.getEntry().insertAfter(initToZero); } } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java index 3f743fee51..e0562829c7 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java @@ -4,7 +4,10 @@ import com.dat3m.dartagnan.exception.ParsingException; import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; +import com.dat3m.dartagnan.expression.Type; +import com.dat3m.dartagnan.expression.integers.IntBinaryOp; import com.dat3m.dartagnan.expression.integers.IntLiteral; +import com.dat3m.dartagnan.expression.integers.IntUnaryExpr; import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.expression.type.TypeFactory; import com.dat3m.dartagnan.parsers.LitmusAArch64BaseVisitor; @@ -14,9 +17,15 @@ import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventFactory; +import com.dat3m.dartagnan.program.event.MemoryEvent; +import com.dat3m.dartagnan.program.event.RegWriter; +import com.dat3m.dartagnan.program.event.arch.CAS; +import com.dat3m.dartagnan.program.event.arch.RMWFetchOp; +import com.dat3m.dartagnan.program.event.arch.RMWOp; import com.dat3m.dartagnan.program.event.arch.Xchg; import com.dat3m.dartagnan.program.event.core.Label; import com.dat3m.dartagnan.program.event.metadata.CustomPrinting; +import com.google.common.base.Preconditions; import org.antlr.v4.runtime.tree.TerminalNode; import java.math.BigInteger; @@ -55,10 +64,22 @@ public Object visitMain(MainContext ctx) { visitInstructionList(ctx.program().instructionList()); VisitorLitmusAssertions.parseAssertions(programBuilder, ctx.assertionList(), ctx.assertionFilter()); Program prog = programBuilder.build(); - replaceZeroRegisters(prog, Arrays.asList("XZR", "WZR")); + + final List zeroRegs = Arrays.asList("XZR", "WZR"); + markLoadsIntoZeroRegisters(prog, zeroRegs); + replaceZeroRegisters(prog, zeroRegs); return prog; } + private void markLoadsIntoZeroRegisters(Program prog, List zeroRegs) { + for (MemoryEvent memEvent : prog.getThreadEvents(MemoryEvent.class)) { + if (memEvent instanceof RegWriter writer && zeroRegs.contains(writer.getResultRegister().getName())) { + memEvent.addTags(NO_RET); + memEvent.removeTags(MO_ACQ, MO_ACQ_PC); + } + } + } + // ---------------------------------------------------------------------------------------------------------------- // Variable declarator list, e.g., { 0:EAX=0; 1:EAX=1; x=2; } @@ -263,8 +284,6 @@ public Object visitStoreExclusive(StoreExclusiveContext ctx) { return Optional.of(String.format("SWP%s%s %s, %s, [%s]", acq, rel, value, loadReg, address)); }; - // FIXME: SWP into a zero register (WZR or XZR) acts like a store, in particular SWPA(L) does not give - // acquire semantics then. @Override public Object visitSwap(SwapContext ctx) { final SwapInstructionContext inst = ctx.swapInstruction(); @@ -293,6 +312,169 @@ public Object visitSwap(SwapContext ctx) { return null; } + private static final CustomPrinting CAS_PRINTER = e -> { + if (!(e instanceof CAS cas)) { + return Optional.empty(); + } + final String acq = e.hasTag(MO_ACQ) ? "A" : ""; + final String rel = e.hasTag(MO_REL) ? "L" : ""; + final Expression value = cas.getStoreValue(); + final Register loadReg = cas.getResultRegister(); + final Expression address = cas.getAddress(); + + return Optional.of(String.format("CAS%s%s %s, %s, [%s]", acq, rel, loadReg, value, address)); + }; + + @Override + public Object visitCas(CasContext ctx) { + final CasInstructionContext inst = ctx.casInstruction(); + + final Register rs64 = parseRegister64(ctx.rS32, ctx.rS64); + final Register rt64 = parseRegister64(ctx.rT32, ctx.rT64); + + final Register rs = shrinkRegister(rs64, ctx.rS32, inst.halfWordSize, inst.byteSize); + final Expression cmpVal = expressions.makeCast(rs64, rs.getType(), false); + final Expression val = expressions.makeCast(rt64, rs.getType(), false); + final Expression address = parseAddress(ctx.address()); + + final List mo = new ArrayList<>(); + if (inst.acquire) { + mo.add(MO_ACQ); + } + if (inst.release) { + mo.add(MO_REL); + } + + final CAS cas = EventFactory.Common.newCAS(rs, address, cmpVal, val); + cas.addTags(mo); + cas.setMetadata(CAS_PRINTER); + + add(cas); + addRegister64Update(rs64, rs); + return null; + } + + + record LDSTAmoInfo(IntBinaryOp op, boolean isHalfSize, boolean isByteSize, boolean acquire, boolean release) {} + + // Used for LDXXX and STXXX instructions of shape + // ST/LD - XXX/XXXX - {A, L, AL}? - {H, B}? + // Instr - op code - memory order - access size + private LDSTAmoInfo getLDSTInfoFromInstructionName(String instrName) { + Preconditions.checkArgument(instrName.startsWith("LD") || instrName.startsWith("ST")); + String instr = instrName.substring(2); // Skip LD/ST + + // TODO: Maybe the following logic can be implemented in the grammar without + // an explicit case distinction over all 96 (or more?) variants of LD (and ST) + + // Access size + final boolean isHalfSize = instr.endsWith("H"); + final boolean isByteSize = instr.endsWith("B"); + if (isHalfSize || isByteSize) { + instr = instr.substring(0, instr.length() - 1); + } + + // Memory order + final boolean release = instr.endsWith("L"); + if (release) { + instr = instr.substring(0, instr.length() - 1); + } + final boolean acquire = instr.endsWith("A"); + if (acquire) { + instr = instr.substring(0, instr.length() - 1); + } + + // Only OpCode remains + assert 3 <= instr.length() && instr.length() <= 4; + // Operation + final String opCode = instr; + final IntBinaryOp op = switch (opCode) { + case "ADD" -> IntBinaryOp.ADD; + case "EOR" -> IntBinaryOp.XOR; + case "SET" -> IntBinaryOp.OR; + case "CLR" -> IntBinaryOp.AND; // Actually & with complement!!! + case "SMIN" -> IntBinaryOp.SMIN; + case "SMAX" -> IntBinaryOp.SMAX; + case "UMIN" -> IntBinaryOp.UMIN; + case "UMAX" -> IntBinaryOp.UMAX; + default -> throw new ParsingException("Invalid op " + opCode + " found in " + instrName); + }; + + return new LDSTAmoInfo(op, isHalfSize, isByteSize, acquire, release); + } + + private static final CustomPrinting LDOP_PRINTER = e -> { + if (!(e instanceof RMWFetchOp ldop)) { + return Optional.empty(); + } + final String acq = e.hasTag(MO_ACQ) ? "A" : ""; + final String rel = e.hasTag(MO_REL) ? "L" : ""; + final String op = opToArmOpCode(ldop.getOperator()); + final String size = getArmSizeSuffix(ldop.getAccessType()); + final Expression operand = ldop.getOperand() instanceof IntUnaryExpr expr ? expr.getOperand() : ldop.getOperand(); + final Register loadReg = ldop.getResultRegister(); + final Expression address = ldop.getAddress(); + + return Optional.of(String.format("LD%s%s%s%s %s, %s, [%s]", op, acq, rel, size, loadReg, operand, address)); + }; + private static final CustomPrinting STOP_PRINTER = e -> { + if (!(e instanceof RMWOp stop)) { + return Optional.empty(); + } + final String rel = e.hasTag(MO_REL) ? "L" : ""; + final String op = opToArmOpCode(stop.getOperator()); + final String size = getArmSizeSuffix(stop.getAccessType()); + final Expression operand = stop.getOperand() instanceof IntUnaryExpr expr ? expr.getOperand() : stop.getOperand(); + final Expression address = stop.getAddress(); + + return Optional.of(String.format("ST%s%s%s %s, [%s]", op, rel, size, operand, address)); + }; + + private static String opToArmOpCode(IntBinaryOp op) { + return switch (op) { + case ADD -> "ADD"; + case XOR -> "EOR"; + case OR -> "SET"; + case AND -> "CLR"; + case SMIN -> "SMIN"; + case SMAX -> "SMAX"; + case UMIN -> "UMIN"; + case UMAX -> "UMAX"; + default -> throw new RuntimeException("Invalid op: " + op); + }; + } + + @Override + public Object visitLoadOp(LoadOpContext ctx) { + final String instr = ctx.loadOpInstruction().getText(); + final LDSTAmoInfo info = getLDSTInfoFromInstructionName(instr); + + final Register rs64 = parseRegister64(ctx.rS32, ctx.rS64); + final Register rt64 = parseRegister64(ctx.rD32, ctx.rD64); + final Register rt = shrinkRegister(rt64, ctx.rD32, info.isHalfSize, info.isByteSize); + Expression operand = expressions.makeCast(rs64, rt.getType(), false); + if (info.op == IntBinaryOp.AND) { + // This was a CLR instruction + operand = expressions.makeIntNot(operand); + } + + final List mo = new ArrayList<>(); + if (info.acquire) { + mo.add(MO_ACQ); + } + if (info.release) { + mo.add(MO_REL); + } + + final Expression address = parseAddress(ctx.address()); + final RMWFetchOp ldOp = EventFactory.Common.newRmwFetchOp(rt, address, info.op, operand); + ldOp.addTags(mo); + ldOp.setMetadata(LDOP_PRINTER); + + add(ldOp); + addRegister64Update(rt64, rt); + return null; + } @Override public Object visitBranch(BranchContext ctx) { @@ -428,16 +610,18 @@ private IntLiteral parseValue(ConstantContext ctx, IntegerType type) { return expressions.parseValue(ctx.getText(), type); } - private Register shrinkRegister(Register other, Register32Context ctx, boolean halfWordSize, boolean byteSize) { - checkArgument(other.getType().equals(i64), "Non-64-bit %s", other); + private Register shrinkRegister(Register r64, Register32Context ctx, boolean halfWordSize, boolean byteSize) { + checkArgument(r64.getType().equals(i64), "Non-64-bit %s", r64); checkArgument(!byteSize | !halfWordSize, "Inconclusive access size"); if (byteSize) { - return programBuilder.getOrNewRegister(mainThread, "B" + other.getName().substring(1), i8); - } - if (halfWordSize) { - return programBuilder.getOrNewRegister(mainThread, "H" + other.getName().substring(1), i16); + return programBuilder.getOrNewRegister(mainThread, "B" + r64.getName().substring(1), i8); + } else if (halfWordSize) { + return programBuilder.getOrNewRegister(mainThread, "H" + r64.getName().substring(1), i16); + } else if (ctx != null) { + return programBuilder.getOrNewRegister(mainThread, "W" + r64.getName().substring(1), i32); + } else { + return r64; } - return ctx == null ? other : programBuilder.getOrNewRegister(mainThread, ctx.getText(), i32); } private void addRegister64Update(Register r64, Register value) { @@ -451,4 +635,37 @@ private Void add(Event event) { programBuilder.addChild(mainThread, event); return null; } + + @Override + public Object visitStoreOp(StoreOpContext ctx) { + final String instr = ctx.storeOpInstruction().getText(); + final LDSTAmoInfo info = getLDSTInfoFromInstructionName(instr); + + final Register rs64 = parseRegister64(ctx.rS32, ctx.rS64); + // TODO: We don't actually care about the smaller register, but only its type! + final Register rs = shrinkRegister(rs64, ctx.rS32, info.isHalfSize, info.isByteSize); + Expression operand = expressions.makeCast(rs64, rs.getType(), false); + if (info.op == IntBinaryOp.AND) { + // This was a CLR instruction + operand = expressions.makeIntNot(operand); + } + + final Expression address = parseAddress(ctx.address()); + final RMWOp stOp = EventFactory.Common.newRmwOp(address, info.op, operand); + if (info.release) { + stOp.addTags(MO_REL); + } + stOp.setMetadata(STOP_PRINTER); + + add(stOp); + return null; + } + + private static String getArmSizeSuffix(Type type) { + return switch (((IntegerType) type).getBitWidth()) { + case 16 -> "H"; + case 8 -> "B"; + default -> ""; + }; + } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java index 79b2b8ca5b..ba206223e2 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java @@ -11,8 +11,7 @@ import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.Thread; -import com.dat3m.dartagnan.program.event.arch.StoreExclusive; -import com.dat3m.dartagnan.program.event.arch.Xchg; +import com.dat3m.dartagnan.program.event.arch.*; import com.dat3m.dartagnan.program.event.arch.ptx.PTXAtomCAS; import com.dat3m.dartagnan.program.event.arch.ptx.PTXAtomExch; import com.dat3m.dartagnan.program.event.arch.ptx.PTXAtomOp; @@ -25,7 +24,6 @@ import com.dat3m.dartagnan.program.event.core.annotations.FunCallMarker; import com.dat3m.dartagnan.program.event.core.annotations.FunReturnMarker; import com.dat3m.dartagnan.program.event.core.annotations.StringAnnotation; -import com.dat3m.dartagnan.program.event.core.InstructionBoundary; import com.dat3m.dartagnan.program.event.core.special.StateSnapshot; import com.dat3m.dartagnan.program.event.core.threading.*; import com.dat3m.dartagnan.program.event.functions.AbortIf; @@ -403,6 +401,18 @@ public static StoreExclusive newExclusiveStore(Register register, Expression add public static Xchg newXchg(Register register, Expression address, Expression storeValue) { return new Xchg(register, address, storeValue); } + + public static CAS newCAS(Register srcReg, Expression address, Expression cmpVal, Expression storeValue) { + return new CAS(srcReg, address, cmpVal, storeValue); + } + + public static RMWFetchOp newRmwFetchOp(Register resultReg, Expression address, IntBinaryOp op, Expression operand) { + return new RMWFetchOp(resultReg, address, op, operand); + } + + public static RMWOp newRmwOp(Expression address, IntBinaryOp op, Expression operand) { + return new RMWOp(address, op, operand); + } } // ============================================================================================= diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventVisitor.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventVisitor.java index 598a97dc3e..1017197639 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventVisitor.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventVisitor.java @@ -1,7 +1,6 @@ package com.dat3m.dartagnan.program.event; -import com.dat3m.dartagnan.program.event.arch.StoreExclusive; -import com.dat3m.dartagnan.program.event.arch.Xchg; +import com.dat3m.dartagnan.program.event.arch.*; import com.dat3m.dartagnan.program.event.arch.ptx.PTXAtomCAS; import com.dat3m.dartagnan.program.event.arch.ptx.PTXAtomExch; import com.dat3m.dartagnan.program.event.arch.ptx.PTXAtomOp; @@ -53,7 +52,10 @@ public interface EventVisitor { // ------------------ Common Events ------------------ default T visitStoreExclusive(StoreExclusive e) { return visitMemEvent(e); } - default T visitXchg(Xchg xchg) { return visitMemEvent(xchg); }; + default T visitXchg(Xchg xchg) { return visitMemEvent(xchg); } + default T visitCas(CAS cas) { return visitMemEvent(cas); } + default T visitRMWOp(RMWOp rmwOp) { return visitMemEvent(rmwOp); }; + default T visitRMWFetchOp(RMWFetchOp rmwOp) { return visitMemEvent(rmwOp); }; // ------------------ Linux Events ------------------ default T visitLKMMAddUnless(LKMMAddUnless e) { return visitMemEvent(e); } 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 index 3f194e8dff..825c8e4642 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java @@ -51,6 +51,7 @@ private ARMv8() { public static final String MO_REL = "L"; public static final String MO_ACQ = "A"; public static final String MO_ACQ_PC = "Q"; + public static final String NO_RET = "NoRet"; public static String extractStoreMoFromCMo(String cMo) { return cMo.equals(C11.MO_SC) || cMo.equals(C11.MO_RELEASE) || cMo.equals(C11.MO_ACQUIRE_RELEASE) ? MO_REL : ""; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/CAS.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/CAS.java new file mode 100644 index 0000000000..219249196a --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/CAS.java @@ -0,0 +1,32 @@ +package com.dat3m.dartagnan.program.event.arch; + +import com.dat3m.dartagnan.expression.Expression; +import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.EventVisitor; +import com.dat3m.dartagnan.program.event.common.RMWCmpXchgBase; + +public class CAS extends RMWCmpXchgBase { + + public CAS(Register register, Expression address, Expression cmpVal, Expression value) { + super(register, address, cmpVal, value, true, ""); + } + + private CAS(CAS other){ + super(other); + } + + @Override + public String defaultString() { + return String.format("%s = cas(%s, %s, %s)", resultRegister, address, expectedValue, storeValue); + } + + @Override + public CAS getCopy(){ + return new CAS(this); + } + + @Override + public T accept(EventVisitor visitor) { + return visitor.visitCas(this); + } +} \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/RMWFetchOp.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/RMWFetchOp.java new file mode 100644 index 0000000000..81e1243722 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/RMWFetchOp.java @@ -0,0 +1,33 @@ +package com.dat3m.dartagnan.program.event.arch; + +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.RMWOpResultBase; + +public class RMWFetchOp extends RMWOpResultBase { + + public RMWFetchOp(Register result, Expression address, IntBinaryOp operator, Expression operand) { + super(result, address, operator, operand, ""); + } + + private RMWFetchOp(RMWFetchOp other) { + super(other); + } + + @Override + public String defaultString() { + return String.format("%s = rmw_fetch_%s(%s, %s)", resultRegister, operator.getName().toLowerCase(), operand, address); + } + + @Override + public RMWFetchOp getCopy(){ + return new RMWFetchOp(this); + } + + @Override + public T accept(EventVisitor visitor) { + return visitor.visitRMWFetchOp(this); + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/RMWOp.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/RMWOp.java new file mode 100644 index 0000000000..9c90da21f6 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/RMWOp.java @@ -0,0 +1,32 @@ +package com.dat3m.dartagnan.program.event.arch; + +import com.dat3m.dartagnan.expression.Expression; +import com.dat3m.dartagnan.expression.integers.IntBinaryOp; +import com.dat3m.dartagnan.program.event.EventVisitor; +import com.dat3m.dartagnan.program.event.common.RMWOpBase; + +public class RMWOp extends RMWOpBase { + + public RMWOp(Expression address, IntBinaryOp operator, Expression operand) { + super(address, operator, operand, ""); + } + + private RMWOp(RMWOp other) { + super(other); + } + + @Override + public String defaultString() { + return String.format("rmw_%s(%s, %s)", operator.getName().toLowerCase(), operand, address); + } + + @Override + public RMWOp getCopy(){ + return new RMWOp(this); + } + + @Override + public T accept(EventVisitor visitor) { + return visitor.visitRMWOp(this); + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java index f1603c7fd0..294d1ff093 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java @@ -9,12 +9,12 @@ import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.Tag.ARMv8; import com.dat3m.dartagnan.program.event.Tag.C11; -import com.dat3m.dartagnan.program.event.arch.StoreExclusive; -import com.dat3m.dartagnan.program.event.arch.Xchg; +import com.dat3m.dartagnan.program.event.arch.*; import com.dat3m.dartagnan.program.event.core.*; import com.dat3m.dartagnan.program.event.lang.catomic.*; import com.dat3m.dartagnan.program.event.lang.linux.*; import com.dat3m.dartagnan.program.event.lang.llvm.*; +import com.google.common.base.Preconditions; import java.util.List; @@ -34,7 +34,7 @@ protected VisitorArm8(boolean useRC11Scheme) { @Override public List visitStoreExclusive(StoreExclusive e) { - RMWStoreExclusive store = newRMWStoreExclusiveWithMo(e.getAddress(), e.getMemValue(), false, e.getMo()); + final RMWStoreExclusive store = newRMWStoreExclusiveWithMo(e.getAddress(), e.getMemValue(), false, e.getMo()); return eventSequence( store, @@ -44,17 +44,88 @@ public List visitStoreExclusive(StoreExclusive e) { @Override public List visitXchg(Xchg xchg) { - Register resultRegister = xchg.getResultRegister(); - Expression address = xchg.getAddress(); - String loadMo = xchg.hasTag(ARMv8.MO_ACQ) ? ARMv8.MO_ACQ : ""; - String storeMo = xchg.hasTag(ARMv8.MO_REL) ? ARMv8.MO_REL : ""; + final Register resultRegister = xchg.getResultRegister(); + final Expression address = xchg.getAddress(); + final String loadMo = xchg.hasTag(ARMv8.MO_ACQ) ? ARMv8.MO_ACQ : ""; + final String storeMo = xchg.hasTag(ARMv8.MO_REL) ? ARMv8.MO_REL : ""; + + final Register dummy = xchg.getFunction().newRegister(resultRegister.getType()); + + return eventSequence( + propagateNoRet(xchg, newRMWLoadExclusiveWithMo(dummy, address, loadMo)), + newRMWStoreExclusiveWithMo(address, xchg.getValue(), true, storeMo), + newLocal(resultRegister, dummy) + ); + } + + @Override + public List visitCas(CAS cas) { + final Register resultRegister = cas.getResultRegister(); + final Expression address = cas.getAddress(); + + final String loadMo = cas.hasTag(ARMv8.MO_ACQ) ? ARMv8.MO_ACQ : ""; + final String storeMo = cas.hasTag(ARMv8.MO_REL) ? ARMv8.MO_REL : ""; + + + final Register dummy = cas.getFunction().newRegister(resultRegister.getType()); + final Load load = propagateNoRet(cas, newRMWLoadWithMo(dummy, address, loadMo)); + final Store store = newRMWStoreWithMo(load, address, cas.getStoreValue(), storeMo); + final Expression cmp = expressions.makeEQ(dummy, cas.getExpectedValue()); + final Label casEnd = newLabel("CAS_end"); + final CondJump branchOnCasCmpResult = newJumpUnless(cmp, casEnd); + + return eventSequence( + load, + branchOnCasCmpResult, + store, + casEnd, + newLocal(resultRegister, dummy) + ); + } + + @Override + public List visitRMWOp(RMWOp rmwOp) { + Preconditions.checkArgument(!rmwOp.hasTag(ARMv8.MO_ACQ), "Unexpected MO_ACQ tag for RMWOp"); + + final Expression address = rmwOp.getAddress(); + final String storeMo = rmwOp.hasTag(ARMv8.MO_REL) ? ARMv8.MO_REL : ""; + + final Register dummy = rmwOp.getFunction().newRegister(rmwOp.getAccessType()); + final Load load = newRMWLoad(dummy, address); + load.addTags(Tag.ARMv8.NO_RET); + final Expression value = expressions.makeBinary(dummy, rmwOp.getOperator(), rmwOp.getOperand()); + + return eventSequence( + load, + newRMWStoreWithMo(load, address, value, storeMo) + ); + } + + @Override + public List visitRMWFetchOp(RMWFetchOp rmwOp) { + final Register resultRegister = rmwOp.getResultRegister(); + final Expression address = rmwOp.getAddress(); + final String loadMo = rmwOp.hasTag(ARMv8.MO_ACQ) ? ARMv8.MO_ACQ : ""; + final String storeMo = rmwOp.hasTag(ARMv8.MO_REL) ? ARMv8.MO_REL : ""; + + final Register dummy = rmwOp.getFunction().newRegister(resultRegister.getType()); + final Load load = propagateNoRet(rmwOp, newRMWLoadWithMo(dummy, address, loadMo)); + final Expression value = expressions.makeBinary(dummy, rmwOp.getOperator(), rmwOp.getOperand()); return eventSequence( - newRMWLoadExclusiveWithMo(resultRegister, address, loadMo), - newRMWStoreExclusiveWithMo(address, xchg.getValue(), true, storeMo) + propagateNoRet(rmwOp, load), + newRMWStoreWithMo(load, address, value, storeMo), + newLocal(resultRegister, dummy) ); } + private T propagateNoRet(Event orig, T newEv) { + if (orig.hasTag(ARMv8.NO_RET)) { + newEv.addTags(Tag.ARMv8.NO_RET); + } + return newEv; + } + // ============================================================================================= // =========================================== LLVM ============================================ // ============================================================================================= diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/llvm/MixedTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/llvm/MixedTest.java index f56693a775..e9c465887b 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/llvm/MixedTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/llvm/MixedTest.java @@ -66,7 +66,7 @@ public static Iterable data() throws IOException { {"memtrack3-pass", ARM8, PASS}, {"mixed-local1", ARM8, PASS}, {"mixed-local2", ARM8, FAIL}, - {"store-to-load-forwarding1", ARM8, FAIL}, + {"store-to-load-forwarding1", ARM8, PASS}, // FAIL on the older version of aarch64.cat {"floats_msa_1", ARM8, PASS}, {"floats_msa_2", ARM8, PASS}, }); diff --git a/dartagnan/src/test/resources/ARM8-expected.csv b/dartagnan/src/test/resources/ARM8-expected.csv index 604a66cb13..23255e1884 100644 --- a/dartagnan/src/test/resources/ARM8-expected.csv +++ b/dartagnan/src/test/resources/ARM8-expected.csv @@ -7863,3 +7863,18 @@ litmus/AARCH64/mixed/WW+R+dmb.sysw4w0+q0+BIS.litmus,0 litmus/AARCH64/mixed/WW+R+dmb.sysw4w0+q0.litmus,0 litmus/AARCH64/mixed/WW+R+posq0w0+q0+SIMPLE.litmus,0 litmus/AARCH64/mixed/WW+RR-variant.litmus,0 +litmus/AARCH64/mixed/CoRR+amo.swph0h0-posh0a.w0+w0.litmus,0 +litmus/AARCH64/mixed/CoRR+rmwh0h0-posh0a.w0+w0.litmus,0 +litmus/AARCH64/NoRet/MP+rel+CAS-ok-dmb.ld.litmus,0 +litmus/AARCH64/NoRet/MP+rel+CASnoret-ok-dmb.ld.litmus,1 +litmus/AARCH64/NoRet/MP+rel+CASacq-noret-ok.litmus,1 +litmus/AARCH64/NoRet/MP+rel+CASacq-ok.litmus,0 +litmus/AARCH64/NoRet/MP+rel+SWPacq.litmus,0 +litmus/AARCH64/NoRet/MP+rel+SWPacq-noret.litmus,1 +litmus/AARCH64/NoRet/MP+rel+SWP-dmb.ld.litmus,0 +litmus/AARCH64/NoRet/MP+rel+SWPnoret-dmb.ld.litmus,1 +litmus/AARCH64/NoRet/MP+rel+LDADD-dmb.ld.litmus,0 +litmus/AARCH64/NoRet/MP+rel+LDADDnoret-dmb.ld.litmus,1 +litmus/AARCH64/NoRet/MP+popl+amo.swpazrp-po.litmus,1 +litmus/AARCH64/NoRet/MP+popl+amo.swpzr-dmb.ld.litmus,1 +litmus/AARCH64/NoRet/MP+popl+amo.swpzr-dsb.ld.litmus,1 \ No newline at end of file diff --git a/litmus/AARCH64/NoRet/MP+popl+amo.swpazrp-po.litmus b/litmus/AARCH64/NoRet/MP+popl+amo.swpazrp-po.litmus new file mode 100644 index 0000000000..54e0722fd9 --- /dev/null +++ b/litmus/AARCH64/NoRet/MP+popl+amo.swpazrp-po.litmus @@ -0,0 +1,11 @@ +AArch64 MP+popl+amo.swpazrp-po +{ +0:X1=x; 0:X3=y; +1:X3=y; 1:X1=x; +} + P0 | P1 ; + MOV W0,#1 | MOV W2,#2 ; + STR W0,[X1] | SWPA W2,WZR,[X3] ; + MOV W2,#1 | LDR W4,[X1] ; + STLR W2,[X3] | ; +exists ([y]=2 /\ 1:X4=0) \ No newline at end of file diff --git a/litmus/AARCH64/NoRet/MP+popl+amo.swpzr-dmb.ld.litmus b/litmus/AARCH64/NoRet/MP+popl+amo.swpzr-dmb.ld.litmus new file mode 100644 index 0000000000..4d8c7ab2b0 --- /dev/null +++ b/litmus/AARCH64/NoRet/MP+popl+amo.swpzr-dmb.ld.litmus @@ -0,0 +1,11 @@ +AArch64 MP+popl+amo.swpzr-dmb.ld +{ +0:X1=x; 0:X3=y; +1:X3=y; 1:X1=x; +} + P0 | P1 ; + MOV W0,#1 | MOV W2,#2 ; + STR W0,[X1] | SWP W2,WZR,[X3] ; + MOV W2,#1 | DMB LD ; + STLR W2,[X3] | LDR W0,[X1] ; +exists ([y]=2 /\ 1:X0=0) \ No newline at end of file diff --git a/litmus/AARCH64/NoRet/MP+popl+amo.swpzr-dsb.ld.litmus b/litmus/AARCH64/NoRet/MP+popl+amo.swpzr-dsb.ld.litmus new file mode 100644 index 0000000000..54598fad17 --- /dev/null +++ b/litmus/AARCH64/NoRet/MP+popl+amo.swpzr-dsb.ld.litmus @@ -0,0 +1,11 @@ +AArch64 MP+popl+amo.swpzr-dsb.ld +{ +0:X1=x; 0:X3=y; +1:X3=y; 1:X1=x; +} + P0 | P1 ; + MOV W0,#1 | MOV W2,#2 ; + STR W0,[X1] | SWP W2,WZR,[X3] ; + MOV W2,#1 | DSB LD ; + STLR W2,[X3] | LDR W0,[X1] ; +exists ([y]=2 /\ 1:X0=0) \ No newline at end of file diff --git a/litmus/AARCH64/NoRet/MP+rel+CAS-ok-dmb.ld.litmus b/litmus/AARCH64/NoRet/MP+rel+CAS-ok-dmb.ld.litmus new file mode 100644 index 0000000000..edcee99c0c --- /dev/null +++ b/litmus/AARCH64/NoRet/MP+rel+CAS-ok-dmb.ld.litmus @@ -0,0 +1,13 @@ +AArch64 MP+rel+CAS-ok-dmb.ld +{ + y=2; + 0:X1=x; 0:X3=y; + 1:X1=x; 1:X3=y; +} + P0 | P1 ; + MOV W0,#1 | MOV W4,#1 ; + STR W0,[X1] | MOV W2,#0 ; + MOV W2,#0 | CAS W2,W4,[X3] ; + STLR W2,[X3] | DMB LD ; + | LDR W0,[X1] ; +exists (y=1 /\ 1:X0=0) diff --git a/litmus/AARCH64/NoRet/MP+rel+CASacq-noret-ok.litmus b/litmus/AARCH64/NoRet/MP+rel+CASacq-noret-ok.litmus new file mode 100644 index 0000000000..2a19c199d9 --- /dev/null +++ b/litmus/AARCH64/NoRet/MP+rel+CASacq-noret-ok.litmus @@ -0,0 +1,12 @@ +AArch64 MP+rel+CASacq-noret-ok +{ + y=2; + 0:X1=x; 0:X3=y; + 1:X1=x; 1:X3=y; +} + P0 | P1 ; + MOV W0,#1 | MOV W4,#1 ; + STR W0,[X1] | CASA WZR,W4,[X3] ; + MOV W2,#0 | LDR W0,[X1] ; + STLR W2,[X3] | ; +exists (y=1 /\ 1:X0=0) diff --git a/litmus/AARCH64/NoRet/MP+rel+CASacq-ok.litmus b/litmus/AARCH64/NoRet/MP+rel+CASacq-ok.litmus new file mode 100644 index 0000000000..2626620342 --- /dev/null +++ b/litmus/AARCH64/NoRet/MP+rel+CASacq-ok.litmus @@ -0,0 +1,12 @@ +AArch64 MP+rel+CASacq-ok +{ + y=2; + 0:X1=x; 0:X3=y; + 1:X1=x; 1:X3=y; +} + P0 | P1 ; + MOV W0,#1 | MOV W4,#1 ; + STR W0,[X1] | MOV W2,#0 ; + MOV W2,#0 | CASA W2,W4,[X3] ; + STLR W2,[X3] | LDR W0,[X1] ; +exists (y=1 /\ 1:X0=0) diff --git a/litmus/AARCH64/NoRet/MP+rel+CASnoret-ok-dmb.ld.litmus b/litmus/AARCH64/NoRet/MP+rel+CASnoret-ok-dmb.ld.litmus new file mode 100644 index 0000000000..4038d75332 --- /dev/null +++ b/litmus/AARCH64/NoRet/MP+rel+CASnoret-ok-dmb.ld.litmus @@ -0,0 +1,12 @@ +AArch64 MP+rel+CASnoret-ok-dmb.ld +{ + y=2; + 0:X1=x; 0:X3=y; + 1:X1=x; 1:X3=y; +} + P0 | P1 ; + MOV W0,#1 | MOV W4,#1 ; + STR W0,[X1] | CAS WZR,W4,[X3] ; + MOV W2,#0 | DMB LD ; + STLR W2,[X3] | LDR W0,[X1] ; +exists (y=1 /\ 1:X0=0) diff --git a/litmus/AARCH64/NoRet/MP+rel+LDADD-dmb.ld.litmus b/litmus/AARCH64/NoRet/MP+rel+LDADD-dmb.ld.litmus new file mode 100644 index 0000000000..34a9f6d0e7 --- /dev/null +++ b/litmus/AARCH64/NoRet/MP+rel+LDADD-dmb.ld.litmus @@ -0,0 +1,12 @@ +AArch64 MP+rel+LDADD-dmb.ld +{ + z=0; + 0:X1=x; 0:X3=y; + 1:X1=x; 1:X3=y; 1:X6=z; +} + P0 | P1 ; + MOV W0,#1 | MOV W4,#1 ; + STR W0,[X1] | LDADD W4,W2,[X3] ; + MOV W2,#1 | DMB LD ; + STLR W2,[X3] | LDR W0,[X1] ; +exists (y=2 /\ 1:X0=0) diff --git a/litmus/AARCH64/NoRet/MP+rel+LDADDnoret-dmb.ld.litmus b/litmus/AARCH64/NoRet/MP+rel+LDADDnoret-dmb.ld.litmus new file mode 100644 index 0000000000..468431aad5 --- /dev/null +++ b/litmus/AARCH64/NoRet/MP+rel+LDADDnoret-dmb.ld.litmus @@ -0,0 +1,11 @@ +AArch64 MP+rel+LDADDnoret-dmb.ld +{ + 0:X1=x; 0:X3=y; + 1:X1=x; 1:X3=y; +} + P0 | P1 ; + MOV W0,#1 | MOV W4,#1 ; + STR W0,[X1] | LDADD W4,WZR,[X3] ; + MOV W2,#1 | DMB LD ; + STLR W2,[X3] | LDR W0,[X1] ; +exists (y=2 /\ 1:X0=0) diff --git a/litmus/AARCH64/NoRet/MP+rel+SWP-dmb.ld.litmus b/litmus/AARCH64/NoRet/MP+rel+SWP-dmb.ld.litmus new file mode 100644 index 0000000000..fdaee81f64 --- /dev/null +++ b/litmus/AARCH64/NoRet/MP+rel+SWP-dmb.ld.litmus @@ -0,0 +1,12 @@ +AArch64 MP+rel+SWP-dmb.ld +{ + z=0; + 0:X1=x; 0:X3=y; + 1:X1=x; 1:X3=y; 1:X6=z; +} + P0 | P1 ; + MOV W0,#1 | MOV W4,#2 ; + STR W0,[X1] | SWP W4,W2,[X3] ; + MOV W2,#1 | DMB LD ; + STLR W2,[X3] | LDR W0,[X1] ; +exists (y=2 /\ 1:X0=0) diff --git a/litmus/AARCH64/NoRet/MP+rel+SWPacq-noret.litmus b/litmus/AARCH64/NoRet/MP+rel+SWPacq-noret.litmus new file mode 100644 index 0000000000..56b2c8e33f --- /dev/null +++ b/litmus/AARCH64/NoRet/MP+rel+SWPacq-noret.litmus @@ -0,0 +1,12 @@ +AArch64 MP+rel+SWPacq-noret +{ + z=0; + 0:X1=x; 0:X3=y; + 1:X1=x; 1:X3=y; +} + P0 | P1 ; + MOV W0,#1 | MOV W4,#2 ; + STR W0,[X1] | SWPA W4,WZR,[X3] ; + MOV W2,#1 | LDR W0,[X1] ; + STLR W2,[X3] | ; +exists (y=2 /\ 1:X0=0) diff --git a/litmus/AARCH64/NoRet/MP+rel+SWPacq.litmus b/litmus/AARCH64/NoRet/MP+rel+SWPacq.litmus new file mode 100644 index 0000000000..c80479d32b --- /dev/null +++ b/litmus/AARCH64/NoRet/MP+rel+SWPacq.litmus @@ -0,0 +1,12 @@ +AArch64 MP+rel+SWPacq +{ + z=0; + 0:X1=x; 0:X3=y; + 1:X1=x; 1:X3=y; 1:X6=z; +} + P0 | P1 ; + MOV W0,#1 | MOV W4,#2 ; + STR W0,[X1] | SWPA W4,W2,[X3] ; + MOV W2,#1 | LDR W0,[X1] ; + STLR W2,[X3] | ; +exists (y=2 /\ 1:X0=0) diff --git a/litmus/AARCH64/NoRet/MP+rel+SWPnoret-dmb.ld.litmus b/litmus/AARCH64/NoRet/MP+rel+SWPnoret-dmb.ld.litmus new file mode 100644 index 0000000000..12e4cfe888 --- /dev/null +++ b/litmus/AARCH64/NoRet/MP+rel+SWPnoret-dmb.ld.litmus @@ -0,0 +1,12 @@ +AArch64 MP+rel+SWPnoret-dmb.ld +{ + z=0; + 0:X1=x; 0:X3=y; + 1:X1=x; 1:X3=y; +} + P0 | P1 ; + MOV W0,#1 | MOV W4,#2 ; + STR W0,[X1] | SWP W4,WZR,[X3] ; + MOV W2,#1 | DMB LD ; + STLR W2,[X3] | LDR W0,[X1] ; +exists (y=2 /\ 1:X0=0) diff --git a/litmus/AARCH64/mixed/CoRR+amo.swph0h0-posh0a.w0+w0.litmus b/litmus/AARCH64/mixed/CoRR+amo.swph0h0-posh0a.w0+w0.litmus new file mode 100644 index 0000000000..ce88a41242 --- /dev/null +++ b/litmus/AARCH64/mixed/CoRR+amo.swph0h0-posh0a.w0+w0.litmus @@ -0,0 +1,14 @@ +AArch64 CoRR+amo.swph0h0-posh0a.w0+w0 +Variant=mixed +{ + uint32_t 0:X3; uint32_t 0:X2; + 0:X0=x; + uint32_t 1:X1=0xccddeeff; 1:X0=x; +} + P0 | P1 ; + MOV W2,#42 | STR W1,[X0] ; + SWPH W2,W1,[X0] | ; + LDAR W3,[X0] | ; +exists (0:X1=0xeeff /\ 0:X3=42) + +(* Linux's qspinlock for systems without FEAT_LSE requires that this is forbidden *) diff --git a/litmus/AARCH64/mixed/CoRR+rmwh0h0-posh0a.w0+w0.litmus b/litmus/AARCH64/mixed/CoRR+rmwh0h0-posh0a.w0+w0.litmus new file mode 100644 index 0000000000..92395cd3e1 --- /dev/null +++ b/litmus/AARCH64/mixed/CoRR+rmwh0h0-posh0a.w0+w0.litmus @@ -0,0 +1,15 @@ +AArch64 CoRR+rmwh0h0-posh0a.w0+w0 +Variant=mixed +{ + uint32_t 0:X3; uint32_t 0:X2; + 0:X0=x; + uint32_t 1:X1=0xccddeeff; 1:X0=x; +} + P0 | P1 ; + MOV W2,#42 | STR W1,[X0] ; + LDXRH W1,[X0] | ; + STXRH W4,W2,[X0] | ; + LDAR W3,[X0] | ; +exists (0:X1=0xeeff /\ 0:X3=42 /\ 0:X4=0) + +(* Linux's qspinlock for systems without FEAT_LSE requires that this is forbidden *)