From 0482274cda255a5159de3de947f64e6afd24325e Mon Sep 17 00:00:00 2001
From: Hernan Ponce de Leon <zeta96@gmail.com>
Date: Fri, 25 Oct 2024 17:39:30 +0800
Subject: [PATCH 1/8] Add exclusive load/store pairs to PPC litmus grammar and
visitor
Signed-off-by: Hernan Ponce de Leon <zeta96@gmail.com>
---
dartagnan/src/main/antlr4/LitmusPPC.g4 | 17 +++++++++++++++++
.../program/visitors/VisitorLitmusPPC.java | 16 ++++++++++++++++
2 files changed, 33 insertions(+)
diff --git a/dartagnan/src/main/antlr4/LitmusPPC.g4 b/dartagnan/src/main/antlr4/LitmusPPC.g4
index 385f2a818c..ff58574a40 100644
--- a/dartagnan/src/main/antlr4/LitmusPPC.g4
+++ b/dartagnan/src/main/antlr4/LitmusPPC.g4
@@ -63,8 +63,10 @@ instruction
| li
| lwz
| lwzx
+ | lwarx
| stw
| stwx
+ | stwcx
| mr
| addi
| xor
@@ -86,6 +88,10 @@ lwzx
: Lwzx register Comma register Comma register
;
+lwarx
+ : Lwarx register Comma register Comma register
+ ;
+
stw
: Stw register Comma offset LPar register RPar
;
@@ -94,6 +100,10 @@ stwx
: Stwx register Comma register Comma register
;
+stwcx
+ : Stwcx register Comma register Comma register
+ ;
+
mr
: Mr register Comma register
;
@@ -187,6 +197,9 @@ Bge
Li : 'li'
;
+Lwarx: 'lwarx'
+ ;
+
Lwzx: 'lwzx'
;
@@ -194,6 +207,10 @@ Lwz
: 'lwz'
;
+Stwcx
+ : 'stwcx'
+ ;
+
Stwx
: 'stwx'
;
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java
index a26bda4444..c76c45822e 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java
@@ -134,6 +134,14 @@ public Object visitLwzx(LitmusPPCParser.LwzxContext ctx) {
throw new ParsingException("lwzx is not implemented");
}
+ @Override
+ public Object visitLwarx(LitmusPPCParser.LwarxContext ctx) {
+ Register r1 = programBuilder.getOrNewRegister(mainThread, ctx.register(0).getText(), archType);
+ Register ra = programBuilder.getOrErrorRegister(mainThread, ctx.register(1).getText());
+ Register rb = programBuilder.getOrErrorRegister(mainThread, ctx.register(2).getText());
+ return programBuilder.addChild(mainThread, EventFactory.newRMWLoadExclusive(r1, expressions.makeAdd(ra, rb)));
+ }
+
@Override
public Object visitStw(LitmusPPCParser.StwContext ctx) {
Register r1 = programBuilder.getOrErrorRegister(mainThread, ctx.register(0).getText());
@@ -147,6 +155,14 @@ public Object visitStwx(LitmusPPCParser.StwxContext ctx) {
throw new ParsingException("stwx is not implemented");
}
+ @Override
+ public Object visitStwcx(LitmusPPCParser.StwcxContext ctx) {
+ Register r1 = programBuilder.getOrNewRegister(mainThread, ctx.register(0).getText(), archType);
+ Register ra = programBuilder.getOrErrorRegister(mainThread, ctx.register(1).getText());
+ Register rb = programBuilder.getOrErrorRegister(mainThread, ctx.register(2).getText());
+ return programBuilder.addChild(mainThread, EventFactory.Power.newRMWStoreConditional(expressions.makeAdd(ra, rb), r1, true));
+ }
+
@Override
public Object visitMr(LitmusPPCParser.MrContext ctx) {
Register r1 = programBuilder.getOrNewRegister(mainThread, ctx.register(0).getText(), archType);
From 7c787bc95b349c07b2585ee1c0d1ab20c6f9e1a3 Mon Sep 17 00:00:00 2001
From: Hernan Ponce de Leon <zeta96@gmail.com>
Date: Fri, 25 Oct 2024 23:01:43 +0800
Subject: [PATCH 2/8] Fix PPC instruction name
Signed-off-by: Hernan Ponce de Leon <zeta96@gmail.com>
---
dartagnan/src/main/antlr4/LitmusPPC.g4 | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/dartagnan/src/main/antlr4/LitmusPPC.g4 b/dartagnan/src/main/antlr4/LitmusPPC.g4
index ff58574a40..52c2eedd96 100644
--- a/dartagnan/src/main/antlr4/LitmusPPC.g4
+++ b/dartagnan/src/main/antlr4/LitmusPPC.g4
@@ -208,7 +208,7 @@ Lwz
;
Stwcx
- : 'stwcx'
+ : 'stwcx.'
;
Stwx
From cc8f2c527c055eea92a2435ef330ba0487be2837 Mon Sep 17 00:00:00 2001
From: Hernan Ponce de Leon <zeta96@gmail.com>
Date: Sat, 26 Oct 2024 03:23:59 +0800
Subject: [PATCH 3/8] More improvemes to PPC grammar
Signed-off-by: Hernan Ponce de Leon <zeta96@gmail.com>
---
dartagnan/src/main/antlr4/LitmusPPC.g4 | 3 ++-
.../parsers/program/visitors/VisitorLitmusPPC.java | 9 +++++----
2 files changed, 7 insertions(+), 5 deletions(-)
diff --git a/dartagnan/src/main/antlr4/LitmusPPC.g4 b/dartagnan/src/main/antlr4/LitmusPPC.g4
index 52c2eedd96..804264da81 100644
--- a/dartagnan/src/main/antlr4/LitmusPPC.g4
+++ b/dartagnan/src/main/antlr4/LitmusPPC.g4
@@ -134,6 +134,7 @@ fence
location
: Identifier
+ | LBracket Identifier RBracket
;
register
@@ -240,7 +241,7 @@ Register
;
Label
- : 'LC' DigitSequence
+ : 'L' Identifier
;
LitmusLanguage
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java
index c76c45822e..08b8c36703 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java
@@ -198,10 +198,11 @@ public Object visitCmpw(LitmusPPCParser.CmpwContext ctx) {
public Object visitBranchCond(LitmusPPCParser.BranchCondContext ctx) {
Label label = programBuilder.getOrCreateLabel(mainThread, ctx.Label().getText());
CmpInstruction cmp = lastCmpInstructionPerThread.put(mainThread, null);
- if(cmp == null){
- throw new ParsingException("Invalid syntax near " + ctx.getText());
- }
- Expression expr = expressions.makeIntCmp(cmp.left, ctx.cond().op, cmp.right);
+ Expression expr = cmp == null ?
+ // In PPC, when there is no previous comparison instruction,
+ // the value of r0 is used as the branching condition
+ expressions.makeBooleanCast(programBuilder.getOrNewRegister(mainThread, "r0")) :
+ expressions.makeIntCmp(cmp.left, ctx.cond().op, cmp.right);
return programBuilder.addChild(mainThread, EventFactory.newJump(expr, label));
}
From 95effa36247aae5701c7289fa9722c791201622f Mon Sep 17 00:00:00 2001
From: Hernan Ponce de Leon <zeta96@gmail.com>
Date: Sat, 26 Oct 2024 04:00:48 +0800
Subject: [PATCH 4/8] Add litmus test
Signed-off-by: Hernan Ponce de Leon <zeta96@gmail.com>
---
dartagnan/src/main/antlr4/LitmusAssertions.g4 | 1 +
.../dartagnan/litmus/LitmusOpenClTest.java | 2 --
dartagnan/src/test/resources/PPC-expected.csv | 1 +
litmus/PPC/R+lwsync+sync+excl+sync.litmus | 21 +++++++++++++++++++
4 files changed, 23 insertions(+), 2 deletions(-)
create mode 100644 litmus/PPC/R+lwsync+sync+excl+sync.litmus
diff --git a/dartagnan/src/main/antlr4/LitmusAssertions.g4 b/dartagnan/src/main/antlr4/LitmusAssertions.g4
index 8b3df0ccff..8086c2d3b5 100644
--- a/dartagnan/src/main/antlr4/LitmusAssertions.g4
+++ b/dartagnan/src/main/antlr4/LitmusAssertions.g4
@@ -28,6 +28,7 @@ assertion
assertionValue
: varName LBracket DigitSequence RBracket
| varName
+ | LBracket varName RBracket
| threadId Colon varName
| constant
;
diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/LitmusOpenClTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/LitmusOpenClTest.java
index ef686b6bb2..9ff8546ca0 100644
--- a/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/LitmusOpenClTest.java
+++ b/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/LitmusOpenClTest.java
@@ -1,7 +1,6 @@
package com.dat3m.dartagnan.litmus;
import com.dat3m.dartagnan.configuration.Arch;
-import com.dat3m.dartagnan.configuration.Property;
import com.dat3m.dartagnan.utils.Result;
import com.dat3m.dartagnan.utils.rules.Provider;
import com.dat3m.dartagnan.utils.rules.Providers;
@@ -10,7 +9,6 @@
import org.junit.runners.Parameterized;
import java.io.IOException;
-import java.util.EnumSet;
@RunWith(Parameterized.class)
public class LitmusOpenClTest extends AbstractLitmusTest {
diff --git a/dartagnan/src/test/resources/PPC-expected.csv b/dartagnan/src/test/resources/PPC-expected.csv
index 3f07bf8e36..cd5cc0b213 100644
--- a/dartagnan/src/test/resources/PPC-expected.csv
+++ b/dartagnan/src/test/resources/PPC-expected.csv
@@ -1334,6 +1334,7 @@ litmus/PPC/R+isyncs.litmus,1
litmus/PPC/R+lwsync+isync.litmus,1
litmus/PPC/R+lwsync+po.litmus,1
litmus/PPC/R+lwsync+sync.litmus,1
+litmus/PPC/R+lwsync+sync+excl+sync.litmus,1
litmus/PPC/R+lwsyncs.litmus,1
litmus/PPC/R+po+isync.litmus,1
litmus/PPC/R+po+lwsync.litmus,1
diff --git a/litmus/PPC/R+lwsync+sync+excl+sync.litmus b/litmus/PPC/R+lwsync+sync+excl+sync.litmus
new file mode 100644
index 0000000000..8dcba21d3c
--- /dev/null
+++ b/litmus/PPC/R+lwsync+sync+excl+sync.litmus
@@ -0,0 +1,21 @@
+PPC A
+"LwSyncdWW Coe SyncdWRNaA SyncdRRANa Fre"
+Generator=diyone7 (version 7.57+1)
+Prefetch=0:x=F,0:y=W,1:y=F,1:x=T
+Com=Co Fr
+Orig=LwSyncdWW Coe SyncdWRNaA SyncdRRANa Fre
+{
+0:r2=x; 0:r4=y;
+1:r2=y; 1:r3=z; 1:r6=x;
+}
+ P0 | P1 ;
+ li r1,1 | li r1,2 ;
+ stw r1,0(r2) | stw r1,0(r2) ;
+ lwsync | sync ;
+ li r3,1 | Loop00: ;
+ stw r3,0(r4) | lwarx r4,r0,r3 ;
+ | stwcx. r4,r0,r3 ;
+ | bne Loop00 ;
+ | sync ;
+ | lwz r5,0(r6) ;
+exists ([y]=2 /\ 1:r5=0)
\ No newline at end of file
From 3a8fa997d3651a65727b8af224428e0827a7b23a Mon Sep 17 00:00:00 2001
From: Hernan Ponce de Leon <zeta96@gmail.com>
Date: Sat, 26 Oct 2024 04:14:02 +0800
Subject: [PATCH 5/8] Support uninitilized registers
Signed-off-by: Hernan Ponce de Leon <zeta96@gmail.com>
---
.../program/visitors/VisitorLitmusPPC.java | 46 +++++++++++--------
1 file changed, 26 insertions(+), 20 deletions(-)
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java
index 08b8c36703..633611028e 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java
@@ -116,15 +116,15 @@ public Object visitInstructionRow(LitmusPPCParser.InstructionRowContext ctx) {
@Override
public Object visitLi(LitmusPPCParser.LiContext ctx) {
- Register register = programBuilder.getOrNewRegister(mainThread, ctx.register().getText(), archType);
+ Register register = (Register) ctx.register().accept(this);
IntLiteral constant = expressions.parseValue(ctx.constant().getText(), archType);
return programBuilder.addChild(mainThread, EventFactory.newLocal(register, constant));
}
@Override
public Object visitLwz(LitmusPPCParser.LwzContext ctx) {
- Register r1 = programBuilder.getOrNewRegister(mainThread, ctx.register(0).getText(), archType);
- Register ra = programBuilder.getOrErrorRegister(mainThread, ctx.register(1).getText());
+ Register r1 = (Register) ctx.register(0).accept(this);
+ Register ra = (Register) ctx.register(1).accept(this);
return programBuilder.addChild(mainThread, EventFactory.newLoad(r1, ra));
}
@@ -136,16 +136,16 @@ public Object visitLwzx(LitmusPPCParser.LwzxContext ctx) {
@Override
public Object visitLwarx(LitmusPPCParser.LwarxContext ctx) {
- Register r1 = programBuilder.getOrNewRegister(mainThread, ctx.register(0).getText(), archType);
- Register ra = programBuilder.getOrErrorRegister(mainThread, ctx.register(1).getText());
- Register rb = programBuilder.getOrErrorRegister(mainThread, ctx.register(2).getText());
+ Register r1 = (Register) ctx.register(0).accept(this);
+ Register ra = (Register) ctx.register(1).accept(this);
+ Register rb = (Register) ctx.register(2).accept(this);
return programBuilder.addChild(mainThread, EventFactory.newRMWLoadExclusive(r1, expressions.makeAdd(ra, rb)));
}
@Override
public Object visitStw(LitmusPPCParser.StwContext ctx) {
- Register r1 = programBuilder.getOrErrorRegister(mainThread, ctx.register(0).getText());
- Register ra = programBuilder.getOrErrorRegister(mainThread, ctx.register(1).getText());
+ Register r1 = (Register) ctx.register(0).accept(this);
+ Register ra = (Register) ctx.register(1).accept(this);
return programBuilder.addChild(mainThread, EventFactory.newStore(ra, r1));
}
@@ -157,39 +157,39 @@ public Object visitStwx(LitmusPPCParser.StwxContext ctx) {
@Override
public Object visitStwcx(LitmusPPCParser.StwcxContext ctx) {
- Register r1 = programBuilder.getOrNewRegister(mainThread, ctx.register(0).getText(), archType);
- Register ra = programBuilder.getOrErrorRegister(mainThread, ctx.register(1).getText());
- Register rb = programBuilder.getOrErrorRegister(mainThread, ctx.register(2).getText());
+ Register r1 = (Register) ctx.register(0).accept(this);
+ Register ra = (Register) ctx.register(1).accept(this);
+ Register rb = (Register) ctx.register(2).accept(this);
return programBuilder.addChild(mainThread, EventFactory.Power.newRMWStoreConditional(expressions.makeAdd(ra, rb), r1, true));
}
@Override
public Object visitMr(LitmusPPCParser.MrContext ctx) {
- Register r1 = programBuilder.getOrNewRegister(mainThread, ctx.register(0).getText(), archType);
- Register r2 = programBuilder.getOrErrorRegister(mainThread, ctx.register(1).getText());
+ Register r1 = (Register) ctx.register(0).accept(this);
+ Register r2 = (Register) ctx.register(1).accept(this);
return programBuilder.addChild(mainThread, EventFactory.newLocal(r1, r2));
}
@Override
public Object visitAddi(LitmusPPCParser.AddiContext ctx) {
- Register r1 = programBuilder.getOrNewRegister(mainThread, ctx.register(0).getText(), archType);
- Register r2 = programBuilder.getOrErrorRegister(mainThread, ctx.register(1).getText());
+ Register r1 = (Register) ctx.register(0).accept(this);
+ Register r2 = (Register) ctx.register(1).accept(this);
IntLiteral constant = expressions.parseValue(ctx.constant().getText(), archType);
return programBuilder.addChild(mainThread, EventFactory.newLocal(r1, expressions.makeAdd(r2, constant)));
}
@Override
public Object visitXor(LitmusPPCParser.XorContext ctx) {
- Register r1 = programBuilder.getOrNewRegister(mainThread, ctx.register(0).getText(), archType);
- Register r2 = programBuilder.getOrErrorRegister(mainThread, ctx.register(1).getText());
- Register r3 = programBuilder.getOrErrorRegister(mainThread, ctx.register(2).getText());
+ Register r1 = (Register) ctx.register(0).accept(this);
+ Register r2 = (Register) ctx.register(1).accept(this);
+ Register r3 = (Register) ctx.register(2).accept(this);
return programBuilder.addChild(mainThread, EventFactory.newLocal(r1, expressions.makeIntXor(r2, r3)));
}
@Override
public Object visitCmpw(LitmusPPCParser.CmpwContext ctx) {
- Register r1 = programBuilder.getOrErrorRegister(mainThread, ctx.register(0).getText());
- Register r2 = programBuilder.getOrErrorRegister(mainThread, ctx.register(1).getText());
+ Register r1 = (Register) ctx.register(0).accept(this);
+ Register r2 = (Register) ctx.register(1).accept(this);
lastCmpInstructionPerThread.put(mainThread, new CmpInstruction(r1, r2));
return null;
}
@@ -219,4 +219,10 @@ public Object visitFence(LitmusPPCParser.FenceContext ctx) {
}
throw new ParsingException("Unrecognised fence " + name);
}
+
+ @Override
+ public Register visitRegister(LitmusPPCParser.RegisterContext ctx) {
+ return programBuilder.getOrNewRegister(mainThread, ctx.getText(), archType);
+ }
+
}
From 2525f05f3f0ed36931212615fc0874baa407bea6 Mon Sep 17 00:00:00 2001
From: Hernan Ponce de Leon <zeta96@gmail.com>
Date: Sat, 26 Oct 2024 04:15:01 +0800
Subject: [PATCH 6/8] Format
Signed-off-by: Hernan Ponce de Leon <zeta96@gmail.com>
---
.../dartagnan/parsers/program/visitors/VisitorLitmusPPC.java | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java
index 633611028e..fd2d3edb22 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java
@@ -199,7 +199,7 @@ public Object visitBranchCond(LitmusPPCParser.BranchCondContext ctx) {
Label label = programBuilder.getOrCreateLabel(mainThread, ctx.Label().getText());
CmpInstruction cmp = lastCmpInstructionPerThread.put(mainThread, null);
Expression expr = cmp == null ?
- // In PPC, when there is no previous comparison instruction,
+ // In PPC, when there is no previous comparison instruction,
// the value of r0 is used as the branching condition
expressions.makeBooleanCast(programBuilder.getOrNewRegister(mainThread, "r0")) :
expressions.makeIntCmp(cmp.left, ctx.cond().op, cmp.right);
From 4d72f2e6aba071b82b917ccad3ff017c09ef3df6 Mon Sep 17 00:00:00 2001
From: Hernan Ponce de Leon <zeta96@gmail.com>
Date: Sun, 27 Oct 2024 02:16:01 +0800
Subject: [PATCH 7/8] Use newExclusiveStore for stwcx instruction
Signed-off-by: Hernan Ponce de Leon <zeta96@gmail.com>
---
.../program/visitors/VisitorLitmusPPC.java | 6 +++++-
.../processing/compilation/VisitorPower.java | 15 +++++++++++++++
2 files changed, 20 insertions(+), 1 deletion(-)
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java
index fd2d3edb22..11a8921282 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java
@@ -157,10 +157,14 @@ public Object visitStwx(LitmusPPCParser.StwxContext ctx) {
@Override
public Object visitStwcx(LitmusPPCParser.StwcxContext ctx) {
+ // This instruction is usually followed by a branch instruction.
+ // Thus, the execution status of the store is saved in r0
+ // (the default register for branch conditions).
+ Register rs = programBuilder.getOrNewRegister(mainThread, "r0", types.getBooleanType());
Register r1 = (Register) ctx.register(0).accept(this);
Register ra = (Register) ctx.register(1).accept(this);
Register rb = (Register) ctx.register(2).accept(this);
- return programBuilder.addChild(mainThread, EventFactory.Power.newRMWStoreConditional(expressions.makeAdd(ra, rb), r1, true));
+ return programBuilder.addChild(mainThread, EventFactory.Common.newExclusiveStore(rs, expressions.makeAdd(ra, rb), r1, ""));
}
@Override
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPower.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPower.java
index 7203312258..7f680aa8c9 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPower.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPower.java
@@ -8,6 +8,7 @@
import com.dat3m.dartagnan.program.event.Event;
import com.dat3m.dartagnan.program.event.Tag;
import com.dat3m.dartagnan.program.event.Tag.C11;
+import com.dat3m.dartagnan.program.event.arch.StoreExclusive;
import com.dat3m.dartagnan.program.event.core.*;
import com.dat3m.dartagnan.program.event.lang.catomic.*;
import com.dat3m.dartagnan.program.event.lang.linux.*;
@@ -40,6 +41,20 @@ protected VisitorPower(boolean useRC11Scheme, PowerScheme cToPowerScheme) {
this.cToPowerScheme = cToPowerScheme;
}
+ // =============================================================================================
+ // ========================================= Common ============================================
+ // =============================================================================================
+
+ @Override
+ public List<Event> visitStoreExclusive(StoreExclusive e) {
+ RMWStoreExclusive store = newRMWStoreExclusiveWithMo(e.getAddress(), e.getMemValue(), true, e.getMo());
+
+ return eventSequence(
+ store,
+ newExecutionStatus(e.getResultRegister(), store)
+ );
+ }
+
// =============================================================================================
// ========================================= PTHREAD ===========================================
// =============================================================================================
From a458619d09e70646ad17b1b674908c47687a7e3f Mon Sep 17 00:00:00 2001
From: Hernan Ponce de Leon <zeta96@gmail.com>
Date: Sun, 27 Oct 2024 15:06:38 +0800
Subject: [PATCH 8/8] Exclusive instructions can be compiled to PPC
Signed-off-by: Hernan Ponce de Leon <zeta96@gmail.com>
---
.../com/dat3m/dartagnan/exceptions/WrongTargetTest.java | 9 ---------
1 file changed, 9 deletions(-)
diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/exceptions/WrongTargetTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/exceptions/WrongTargetTest.java
index fa35c086e0..958f5216c9 100644
--- a/dartagnan/src/test/java/com/dat3m/dartagnan/exceptions/WrongTargetTest.java
+++ b/dartagnan/src/test/java/com/dat3m/dartagnan/exceptions/WrongTargetTest.java
@@ -57,13 +57,4 @@ public void ARMCompiledToTSO() throws Exception {
comp.setTarget(Arch.TSO);
comp.run(p);
}
-
- @Test(expected = IllegalArgumentException.class)
- public void ARMCompiledToPower() throws Exception {
- Program p = new ProgramParser().parse(new File(getRootPath("litmus/AARCH64/ATOM/2+2W+poxxs.litmus")));
- LoopUnrolling.newInstance().run(p);
- Compilation comp = Compilation.newInstance();
- comp.setTarget(Arch.POWER);
- comp.run(p);
- }
}