From b43a52c2e61c1f57cccdcaba5fe7891bc09138a6 Mon Sep 17 00:00:00 2001 From: Natalia Gavrilenko Date: Tue, 19 Nov 2024 15:52:10 +0100 Subject: [PATCH] tmp --- .../compilation/VisitorSpirvVulkan.java | 28 ++- .../compilation/VisitorSpirvVulkanTest.java | 196 +++++++----------- 2 files changed, 97 insertions(+), 127 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorSpirvVulkan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorSpirvVulkan.java index 73b276886a..ba93b2a842 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorSpirvVulkan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorSpirvVulkan.java @@ -1,5 +1,6 @@ package com.dat3m.dartagnan.program.processing.compilation; +import com.dat3m.dartagnan.exception.ParsingException; import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventFactory; import com.dat3m.dartagnan.program.event.Tag; @@ -46,6 +47,7 @@ public List visitSpirvLoad(SpirvLoad e) { load.addTags(Tag.Vulkan.ATOM); load.addTags(toVulkanTags(e.getTags())); replaceAcqRelTag(load, Tag.Vulkan.ACQUIRE); + validateSemanticsTags(load.getTags()); return eventSequence(load); } @@ -58,6 +60,7 @@ public List visitSpirvStore(SpirvStore e) { store.addTags(Tag.Vulkan.ATOM); store.addTags(toVulkanTags(e.getTags())); replaceAcqRelTag(store, Tag.Vulkan.RELEASE); + validateSemanticsTags(store.getTags()); return eventSequence(store); } @@ -70,6 +73,7 @@ public List visitSpirvXchg(SpirvXchg e) { e.getValue(), mo, scope); rmw.addTags(toVulkanTags(e.getTags())); replaceAcqRelTag(rmw, Tag.Vulkan.ACQUIRE, Tag.Vulkan.RELEASE); + validateSemanticsTags(rmw.getTags()); rmw.setFunction(e.getFunction()); return visitVulkanRMW(rmw); } @@ -81,9 +85,10 @@ public List visitSpirvRMW(SpirvRmw e) { String scope = toVulkanTag(Tag.Spirv.getScopeTag(e.getTags())); VulkanRMWOp rmwOp = EventFactory.Vulkan.newRMWOp(e.getAddress(), e.getResultRegister(), e.getOperand(), e.getOperator(), mo, scope); - rmwOp.setFunction(e.getFunction()); rmwOp.addTags(toVulkanTags(e.getTags())); replaceAcqRelTag(rmwOp, Tag.Vulkan.ACQUIRE, Tag.Vulkan.RELEASE); + validateSemanticsTags(rmwOp.getTags()); + rmwOp.setFunction(e.getFunction()); return visitVulkanRMWOp(rmwOp); } @@ -108,6 +113,7 @@ public List visitSpirvCmpXchg(SpirvCmpXchg e) { cmpXchg.setFunction(e.getFunction()); cmpXchg.addTags(toVulkanTags(eqTags)); replaceAcqRelTag(cmpXchg, Tag.Vulkan.ACQUIRE, Tag.Vulkan.RELEASE); + validateSemanticsTags(cmpXchg.getTags()); return visitVulkanCmpXchg(cmpXchg); } @@ -122,6 +128,7 @@ public List visitSpirvRmwExtremum(SpirvRmwExtremum e) { rmw.setFunction(e.getFunction()); rmw.addTags(toVulkanTags(e.getTags())); replaceAcqRelTag(rmw, Tag.Vulkan.ACQUIRE, Tag.Vulkan.RELEASE); + validateSemanticsTags(rmw.getTags()); return visitVulkanRMWExtremum(rmw); } @@ -131,6 +138,7 @@ public List visitGenericVisibleEvent(GenericVisibleEvent e) { fence.removeTags(fence.getTags()); fence.addTags(toVulkanTags(e.getTags())); replaceAcqRelTag(fence, Tag.Vulkan.ACQUIRE, Tag.Vulkan.RELEASE); + validateSemanticsTags(fence.getTags()); return eventSequence(fence); } @@ -140,6 +148,7 @@ public List visitControlBarrier(ControlBarrier e) { barrier.removeTags(barrier.getTags()); barrier.addTags(toVulkanTags(e.getTags())); replaceAcqRelTag(barrier, Tag.Vulkan.ACQUIRE, Tag.Vulkan.RELEASE); + validateSemanticsTags(barrier.getTags()); return eventSequence(barrier); } @@ -158,6 +167,23 @@ private Set toVulkanTags(Set tags) { return vTags; } + private void validateSemanticsTags(Set tags) { + boolean hasMoTags = tags.contains(Tag.Vulkan.ACQUIRE) || tags.contains(Tag.Vulkan.RELEASE) || tags.contains(Tag.Vulkan.ACQ_REL); + boolean hasSemScTags = tags.contains(Tag.Vulkan.SEMSC0) || tags.contains(Tag.Vulkan.SEMSC1); + if (hasMoTags && !hasSemScTags) { + throw new ParsingException("Non-relaxed semantics must have storage class semantics tags"); + } + if (hasSemScTags && !hasMoTags) { + throw new ParsingException("Storage class semantics requires memory order tags"); + } + if (tags.contains(Tag.Vulkan.SEM_AVAILABLE) && !tags.contains(Tag.Vulkan.RELEASE) && !tags.contains(Tag.Vulkan.ACQ_REL)) { + throw new ParsingException("Available semantics must have release tag"); + } + if (tags.contains(Tag.Vulkan.SEM_VISIBLE) && !tags.contains(Tag.Vulkan.ACQUIRE) && !tags.contains(Tag.Vulkan.ACQ_REL)) { + throw new ParsingException("Visible semantics must have acquire tag"); + } + } + private void replaceAcqRelTag(Event e, String... tags) { if (e.getTags().contains(Tag.Vulkan.ACQ_REL)) { e.addTags(tags); diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/program/processing/compilation/VisitorSpirvVulkanTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/program/processing/compilation/VisitorSpirvVulkanTest.java index c40d6bbefc..61ccfeb5bc 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/program/processing/compilation/VisitorSpirvVulkanTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/program/processing/compilation/VisitorSpirvVulkanTest.java @@ -43,8 +43,8 @@ public void testLoad() { Set.of(Tag.Vulkan.SC1) ); doTestLoad( - Set.of(Tag.Spirv.MEM_VISIBLE, Tag.Spirv.DEVICE, Tag.Spirv.SC_UNIFORM), - Set.of(Tag.Vulkan.VISIBLE, Tag.Vulkan.DEVICE, Tag.Vulkan.SC0) + Set.of(Tag.Spirv.MEM_NON_PRIVATE, Tag.Spirv.DEVICE), + Set.of(Tag.Vulkan.NON_PRIVATE, Tag.Vulkan.DEVICE) ); doTestLoad( Set.of(Tag.Spirv.MEM_NON_PRIVATE, Tag.Spirv.MEM_VISIBLE, Tag.Spirv.DEVICE, Tag.Spirv.SC_UNIFORM), @@ -80,8 +80,8 @@ public void testStore() { Set.of(Tag.Vulkan.SC1) ); doTestStore( - Set.of(Tag.Spirv.MEM_AVAILABLE, Tag.Spirv.DEVICE, Tag.Spirv.SC_UNIFORM), - Set.of(Tag.Vulkan.AVAILABLE, Tag.Vulkan.DEVICE, Tag.Vulkan.SC0) + Set.of(Tag.Spirv.MEM_NON_PRIVATE, Tag.Spirv.DEVICE), + Set.of(Tag.Vulkan.NON_PRIVATE, Tag.Vulkan.DEVICE) ); doTestStore( Set.of(Tag.Spirv.MEM_NON_PRIVATE, Tag.Spirv.MEM_AVAILABLE, Tag.Spirv.DEVICE, Tag.Spirv.SC_UNIFORM), @@ -109,24 +109,16 @@ private void doTestStore(Set spvTags, Set vulTags) { @Test public void testSpirvLoad() { doTestSpirvLoad( - Set.of(Tag.Spirv.RELAXED, Tag.Spirv.SUBGROUP, Tag.Spirv.SC_WORKGROUP), - Set.of(Tag.Vulkan.SUB_GROUP, Tag.Vulkan.SC1, Tag.Vulkan.NON_PRIVATE) + Set.of(Tag.Spirv.SC_WORKGROUP, Tag.Spirv.SUBGROUP, Tag.Spirv.RELAXED), + Set.of(Tag.Vulkan.SC1, Tag.Vulkan.SUB_GROUP) ); doTestSpirvLoad( - Set.of(Tag.Spirv.SEQ_CST, Tag.Spirv.SUBGROUP, Tag.Spirv.SC_WORKGROUP), - Set.of(Tag.Vulkan.ACQUIRE, Tag.Vulkan.SUB_GROUP, Tag.Vulkan.SC1, Tag.Vulkan.NON_PRIVATE) + Set.of(Tag.Spirv.SC_WORKGROUP, Tag.Spirv.WORKGROUP, Tag.Spirv.ACQUIRE, Tag.Spirv.SEM_WORKGROUP), + Set.of(Tag.Vulkan.SC1, Tag.Vulkan.WORK_GROUP, Tag.Vulkan.ACQUIRE, Tag.Vulkan.SEMSC1) ); doTestSpirvLoad( - Set.of(Tag.Spirv.ACQUIRE, Tag.Spirv.WORKGROUP, Tag.Spirv.SC_WORKGROUP), - Set.of(Tag.Vulkan.ACQUIRE, Tag.Vulkan.WORK_GROUP, Tag.Vulkan.SC1, Tag.Vulkan.NON_PRIVATE) - ); - doTestSpirvLoad( - Set.of(Tag.Spirv.ACQUIRE, Tag.Spirv.WORKGROUP, Tag.Spirv.SEM_UNIFORM, Tag.Spirv.SEM_VISIBLE, Tag.Spirv.SC_UNIFORM), - Set.of(Tag.Vulkan.ACQUIRE, Tag.Vulkan.WORK_GROUP, Tag.Vulkan.SEMSC0, Tag.Vulkan.SEM_VISIBLE, Tag.Vulkan.SC0, Tag.Vulkan.NON_PRIVATE) - ); - doTestSpirvLoad( - Set.of(Tag.Spirv.RELAXED, Tag.Spirv.DEVICE, Tag.Spirv.SC_UNIFORM), - Set.of(Tag.Vulkan.DEVICE, Tag.Vulkan.SC0, Tag.Vulkan.NON_PRIVATE) + Set.of(Tag.Spirv.SC_UNIFORM, Tag.Spirv.WORKGROUP, Tag.Spirv.ACQUIRE, Tag.Spirv.SEM_UNIFORM, Tag.Spirv.SEM_VISIBLE), + Set.of(Tag.Vulkan.SC0, Tag.Vulkan.WORK_GROUP, Tag.Vulkan.ACQUIRE, Tag.Vulkan.SEMSC0, Tag.Vulkan.SEM_VISIBLE) ); } @@ -152,24 +144,16 @@ private void doTestSpirvLoad(Set spvTags, Set vulTags) { @Test public void testSpirvStore() { doTestSpirvStore( - Set.of(Tag.Spirv.RELAXED, Tag.Spirv.SUBGROUP, Tag.Spirv.SC_WORKGROUP), - Set.of(Tag.Vulkan.SUB_GROUP, Tag.Vulkan.SC1, Tag.Vulkan.NON_PRIVATE) + Set.of(Tag.Spirv.SC_WORKGROUP, Tag.Spirv.SUBGROUP, Tag.Spirv.RELAXED), + Set.of(Tag.Vulkan.SC1, Tag.Vulkan.SUB_GROUP) ); doTestSpirvStore( - Set.of(Tag.Spirv.SEQ_CST, Tag.Spirv.SUBGROUP, Tag.Spirv.SC_WORKGROUP), - Set.of(Tag.Vulkan.RELEASE, Tag.Vulkan.SUB_GROUP, Tag.Vulkan.SC1, Tag.Vulkan.NON_PRIVATE) + Set.of(Tag.Spirv.SC_WORKGROUP, Tag.Spirv.WORKGROUP, Tag.Spirv.RELEASE, Tag.Spirv.SEM_WORKGROUP), + Set.of(Tag.Vulkan.SC1, Tag.Vulkan.WORK_GROUP, Tag.Vulkan.RELEASE, Tag.Vulkan.SEMSC1) ); doTestSpirvStore( - Set.of(Tag.Spirv.RELEASE, Tag.Spirv.WORKGROUP, Tag.Spirv.SC_WORKGROUP), - Set.of(Tag.Vulkan.RELEASE, Tag.Vulkan.WORK_GROUP, Tag.Vulkan.SC1, Tag.Vulkan.NON_PRIVATE) - ); - doTestSpirvStore( - Set.of(Tag.Spirv.RELEASE, Tag.Spirv.WORKGROUP, Tag.Spirv.SEM_UNIFORM, Tag.Spirv.SEM_AVAILABLE, Tag.Spirv.SC_UNIFORM), - Set.of(Tag.Vulkan.RELEASE, Tag.Vulkan.WORK_GROUP, Tag.Vulkan.SEMSC0, Tag.Vulkan.SEM_AVAILABLE, Tag.Vulkan.SC0, Tag.Vulkan.NON_PRIVATE) - ); - doTestSpirvStore( - Set.of(Tag.Spirv.RELAXED, Tag.Spirv.DEVICE, Tag.Spirv.SC_UNIFORM), - Set.of(Tag.Vulkan.DEVICE, Tag.Vulkan.SC0, Tag.Vulkan.NON_PRIVATE) + Set.of(Tag.Spirv.SC_UNIFORM, Tag.Spirv.WORKGROUP, Tag.Spirv.RELEASE, Tag.Spirv.SEM_UNIFORM, Tag.Spirv.SEM_AVAILABLE), + Set.of(Tag.Vulkan.SC0, Tag.Vulkan.WORK_GROUP, Tag.Vulkan.RELEASE, Tag.Vulkan.SEMSC0, Tag.Vulkan.SEM_AVAILABLE) ); } @@ -195,34 +179,24 @@ private void doTestSpirvStore(Set spvTags, Set vulTags) { @Test public void testSpirvXchg() { doTestSpirvXchg( - Set.of(Tag.Spirv.RELAXED, Tag.Spirv.SUBGROUP, Tag.Spirv.SC_WORKGROUP), - Set.of(Tag.Vulkan.SUB_GROUP, Tag.Vulkan.SC1, Tag.Vulkan.NON_PRIVATE), - Set.of(Tag.Vulkan.SUB_GROUP, Tag.Vulkan.SC1, Tag.Vulkan.NON_PRIVATE) - ); - doTestSpirvXchg( - Set.of(Tag.Spirv.ACQUIRE, Tag.Spirv.WORKGROUP, Tag.Spirv.SC_WORKGROUP), - Set.of(Tag.Vulkan.ACQUIRE, Tag.Vulkan.WORK_GROUP, Tag.Vulkan.SC1, Tag.Vulkan.NON_PRIVATE), - Set.of(Tag.Vulkan.WORK_GROUP, Tag.Vulkan.SC1, Tag.Vulkan.NON_PRIVATE) + Set.of(Tag.Spirv.SC_WORKGROUP, Tag.Spirv.SUBGROUP, Tag.Spirv.RELAXED), + Set.of(Tag.Vulkan.SC1, Tag.Vulkan.SUB_GROUP), + Set.of(Tag.Vulkan.SC1, Tag.Vulkan.SUB_GROUP) ); doTestSpirvXchg( - Set.of(Tag.Spirv.RELEASE, Tag.Spirv.WORKGROUP, Tag.Spirv.SC_WORKGROUP), - Set.of(Tag.Vulkan.WORK_GROUP, Tag.Vulkan.SC1, Tag.Vulkan.NON_PRIVATE), - Set.of(Tag.Vulkan.RELEASE, Tag.Vulkan.WORK_GROUP, Tag.Vulkan.SC1, Tag.Vulkan.NON_PRIVATE) + Set.of(Tag.Spirv.SC_WORKGROUP, Tag.Spirv.WORKGROUP, Tag.Spirv.ACQUIRE, Tag.Spirv.SEM_WORKGROUP), + Set.of(Tag.Vulkan.SC1, Tag.Vulkan.WORK_GROUP, Tag.Vulkan.ACQUIRE, Tag.Vulkan.SEMSC1), + Set.of(Tag.Vulkan.SC1, Tag.Vulkan.WORK_GROUP) ); doTestSpirvXchg( - Set.of(Tag.Spirv.ACQ_REL, Tag.Spirv.WORKGROUP, Tag.Spirv.SC_WORKGROUP), - Set.of(Tag.Vulkan.ACQUIRE, Tag.Vulkan.WORK_GROUP, Tag.Vulkan.SC1, Tag.Vulkan.NON_PRIVATE), - Set.of(Tag.Vulkan.RELEASE, Tag.Vulkan.WORK_GROUP, Tag.Vulkan.SC1, Tag.Vulkan.NON_PRIVATE) + Set.of(Tag.Spirv.SC_WORKGROUP, Tag.Spirv.WORKGROUP, Tag.Spirv.RELEASE, Tag.Spirv.SEM_WORKGROUP), + Set.of(Tag.Vulkan.SC1, Tag.Vulkan.WORK_GROUP), + Set.of(Tag.Vulkan.SC1, Tag.Vulkan.WORK_GROUP, Tag.Vulkan.RELEASE, Tag.Vulkan.SEMSC1) ); doTestSpirvXchg( - Set.of(Tag.Spirv.SEQ_CST, Tag.Spirv.WORKGROUP, Tag.Spirv.SC_WORKGROUP), - Set.of(Tag.Vulkan.ACQUIRE, Tag.Vulkan.WORK_GROUP, Tag.Vulkan.SC1, Tag.Vulkan.NON_PRIVATE), - Set.of(Tag.Vulkan.RELEASE, Tag.Vulkan.WORK_GROUP, Tag.Vulkan.SC1, Tag.Vulkan.NON_PRIVATE) - ); - doTestSpirvXchg( - Set.of(Tag.Spirv.RELAXED, Tag.Spirv.DEVICE, Tag.Spirv.SC_WORKGROUP), - Set.of(Tag.Vulkan.DEVICE, Tag.Vulkan.SC1, Tag.Vulkan.NON_PRIVATE), - Set.of(Tag.Vulkan.DEVICE, Tag.Vulkan.SC1, Tag.Vulkan.NON_PRIVATE) + Set.of(Tag.Spirv.SC_WORKGROUP, Tag.Spirv.WORKGROUP, Tag.Spirv.ACQ_REL, Tag.Spirv.SEM_WORKGROUP), + Set.of(Tag.Vulkan.SC1, Tag.Vulkan.WORK_GROUP, Tag.Vulkan.ACQUIRE, Tag.Vulkan.SEMSC1), + Set.of(Tag.Vulkan.SC1, Tag.Vulkan.WORK_GROUP, Tag.Vulkan.RELEASE, Tag.Vulkan.SEMSC1) ); } @@ -256,34 +230,24 @@ private void doTestSpirvXchg(Set spvTags, Set loadTags, Set spvTags, Set loadTags, Set eqTags, Set neqTags, Set loadTags, Set storeTags) { @@ -423,24 +375,20 @@ private void doTestSpirvCmpXchgIllegal(Set eqTags, Set neqTags, @Test public void testSpirvMemoryBarrier() { doTestSpirvMemoryBarrier( - Set.of(Tag.Spirv.RELAXED, Tag.Spirv.SUBGROUP), + Set.of(Tag.Spirv.SUBGROUP, Tag.Spirv.RELAXED), Set.of(Tag.Vulkan.SUB_GROUP) ); doTestSpirvMemoryBarrier( - Set.of(Tag.Spirv.ACQUIRE, Tag.Spirv.SUBGROUP), - Set.of(Tag.Vulkan.ACQUIRE, Tag.Vulkan.SUB_GROUP) - ); - doTestSpirvMemoryBarrier( - Set.of(Tag.Spirv.RELEASE, Tag.Spirv.SUBGROUP), - Set.of(Tag.Vulkan.RELEASE, Tag.Vulkan.SUB_GROUP) + Set.of(Tag.Spirv.SUBGROUP, Tag.Spirv.ACQUIRE, Tag.Spirv.SEM_WORKGROUP), + Set.of(Tag.Vulkan.SUB_GROUP, Tag.Vulkan.ACQUIRE, Tag.Vulkan.SEMSC1) ); doTestSpirvMemoryBarrier( - Set.of(Tag.Spirv.ACQ_REL, Tag.Spirv.SUBGROUP), - Set.of(Tag.Vulkan.ACQUIRE, Tag.Vulkan.RELEASE, Tag.Vulkan.SUB_GROUP) + Set.of(Tag.Spirv.SUBGROUP, Tag.Spirv.RELEASE, Tag.Spirv.SEM_WORKGROUP), + Set.of(Tag.Vulkan.SUB_GROUP, Tag.Vulkan.RELEASE, Tag.Vulkan.SEMSC1) ); doTestSpirvMemoryBarrier( - Set.of(Tag.Spirv.SEQ_CST, Tag.Spirv.SUBGROUP), - Set.of(Tag.Vulkan.ACQUIRE, Tag.Vulkan.RELEASE, Tag.Vulkan.SUB_GROUP) + Set.of(Tag.Spirv.SUBGROUP, Tag.Spirv.ACQ_REL, Tag.Spirv.SEM_WORKGROUP), + Set.of(Tag.Vulkan.SUB_GROUP, Tag.Vulkan.ACQUIRE, Tag.Vulkan.RELEASE, Tag.Vulkan.SEMSC1) ); } @@ -466,24 +414,20 @@ public void testSpirvControlBarrier() { Set.of() ); doTestSpirvControlBarrier( - Set.of(Tag.Spirv.RELAXED, Tag.Spirv.SUBGROUP), + Set.of(Tag.Spirv.SUBGROUP, Tag.Spirv.RELAXED), Set.of(Tag.FENCE, Tag.Vulkan.SUB_GROUP) ); doTestSpirvControlBarrier( - Set.of(Tag.Spirv.ACQUIRE, Tag.Spirv.SUBGROUP), - Set.of(Tag.FENCE, Tag.Vulkan.ACQUIRE, Tag.Vulkan.SUB_GROUP) - ); - doTestSpirvControlBarrier( - Set.of(Tag.Spirv.RELEASE, Tag.Spirv.SUBGROUP), - Set.of(Tag.FENCE, Tag.Vulkan.RELEASE, Tag.Vulkan.SUB_GROUP) + Set.of(Tag.Spirv.SUBGROUP, Tag.Spirv.ACQUIRE, Tag.Spirv.SEM_WORKGROUP), + Set.of(Tag.FENCE, Tag.Vulkan.SUB_GROUP, Tag.Vulkan.ACQUIRE, Tag.Vulkan.SEMSC1) ); doTestSpirvControlBarrier( - Set.of(Tag.Spirv.ACQ_REL, Tag.Spirv.SUBGROUP), - Set.of(Tag.FENCE, Tag.Vulkan.ACQUIRE, Tag.Vulkan.RELEASE, Tag.Vulkan.SUB_GROUP) + Set.of(Tag.Spirv.SUBGROUP, Tag.Spirv.RELEASE, Tag.Spirv.SEM_WORKGROUP), + Set.of(Tag.FENCE, Tag.Vulkan.SUB_GROUP, Tag.Vulkan.RELEASE, Tag.Vulkan.SEMSC1) ); doTestSpirvControlBarrier( - Set.of(Tag.Spirv.SEQ_CST, Tag.Spirv.SUBGROUP), - Set.of(Tag.FENCE, Tag.Vulkan.ACQUIRE, Tag.Vulkan.RELEASE, Tag.Vulkan.SUB_GROUP) + Set.of(Tag.Spirv.SUBGROUP, Tag.Spirv.ACQ_REL, Tag.Spirv.SEM_WORKGROUP), + Set.of(Tag.FENCE, Tag.Vulkan.SUB_GROUP, Tag.Vulkan.ACQUIRE, Tag.Vulkan.RELEASE, Tag.Vulkan.SEMSC1) ); }