From 0d32a251c573c2ef9e011c819cffee9a649f65cf Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Fri, 22 Nov 2024 14:37:13 +0100 Subject: [PATCH 1/3] Improve DynamicSpinLoopDetection --- .../expression/ExpressionFactory.java | 2 +- .../expression/aggregates/ConstructExpr.java | 2 +- .../processing/DynamicSpinLoopDetection.java | 189 ++++++------------ 3 files changed, 65 insertions(+), 128 deletions(-) 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 ffe20ffc1d..d26b80bc30 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionFactory.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionFactory.java @@ -259,7 +259,7 @@ public Expression makeFloatCast(Expression operand, FloatType targetType, boolea // ----------------------------------------------------------------------------------------------------------------- // Aggregates - public Expression makeConstruct(Type type, List arguments) { + public Expression makeConstruct(Type type, List arguments) { return new ConstructExpr(type, arguments); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/aggregates/ConstructExpr.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/aggregates/ConstructExpr.java index cfd75acb90..051de92aaf 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/aggregates/ConstructExpr.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/aggregates/ConstructExpr.java @@ -16,7 +16,7 @@ public final class ConstructExpr extends NaryExpressionBase { - public ConstructExpr(Type type, List arguments) { + public ConstructExpr(Type type, List arguments) { super(type, ExpressionKind.Other.CONSTRUCT, List.copyOf(arguments)); checkArgument(type instanceof AggregateType || type instanceof ArrayType, "Non-constructible type %s.", type); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicSpinLoopDetection.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicSpinLoopDetection.java index 1a002d6b52..6ecd748c77 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicSpinLoopDetection.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicSpinLoopDetection.java @@ -2,22 +2,24 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; +import com.dat3m.dartagnan.expression.type.AggregateType; import com.dat3m.dartagnan.expression.type.TypeFactory; import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.Thread; -import com.dat3m.dartagnan.program.analysis.DominatorAnalysis; +import com.dat3m.dartagnan.program.analysis.LiveRegistersAnalysis; import com.dat3m.dartagnan.program.analysis.LoopAnalysis; -import com.dat3m.dartagnan.program.event.*; +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.program.event.EventFactory; +import com.dat3m.dartagnan.program.event.RegWriter; +import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.core.Label; import com.dat3m.dartagnan.program.event.functions.FunctionCall; -import com.dat3m.dartagnan.program.event.lang.svcomp.SpinStart; -import com.dat3m.dartagnan.utils.DominatorTree; import com.google.common.base.Preconditions; import com.google.common.collect.Iterables; +import com.google.common.collect.Lists; import com.google.common.collect.Sets; -import com.google.common.collect.Streams; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; import org.sosy_lab.common.configuration.Configuration; @@ -26,8 +28,6 @@ import java.util.HashSet; import java.util.List; import java.util.Set; -import java.util.function.Predicate; -import java.util.stream.Collectors; /* This pass instruments loops that do not cause a side effect in an iteration to terminate, i.e., to avoid spinning. @@ -49,19 +49,17 @@ public void run(Program program) { "DynamicSpinLoopDetection cannot be run on already unrolled programs."); final LoopAnalysis loopAnalysis = LoopAnalysis.newInstance(program); - AnalysisStats stats = new AnalysisStats(0, 0); + AnalysisStats stats = new AnalysisStats(0); for (Function func : Iterables.concat(program.getFunctions(), program.getThreads())) { final List loops = computeLoopData(func, loopAnalysis); - loops.forEach(this::collectSideEffects); - loops.forEach(this::reduceToDominatingSideEffects); + final LiveRegistersAnalysis liveRegsAna = LiveRegistersAnalysis.forFunction(func); + loops.forEach(loop -> this.collectSideEffects(loop, liveRegsAna)); loops.forEach(this::instrumentLoop); stats = stats.add(collectStats(loops)); } IdReassignment.newInstance().run(program); // Reassign ids for the instrumented code. - // NOTE: We log "potential spin loops" as only those that are not also "static". - logger.info("Found {} static spin loops and {} potential spin loops.", - stats.numStaticSpinLoops, (stats.numPotentialSpinLoops - stats.numStaticSpinLoops)); + logger.info("Found {} static spin loops.", stats.numStaticSpinLoops()); } // ================================================================================================== @@ -72,158 +70,94 @@ private List computeLoopData(Function func, LoopAnalysis loopAnalysis) return loops.stream().map(LoopData::new).toList(); } - private void collectSideEffects(LoopData loop) { - // Loop shape is: loopStart -> Calling intrinsic __VERIFIER_spin_start -> #__VERIFIER_spin_start - if (loop.getStart().getSuccessor().getSuccessor() instanceof SpinStart) { - // A user-placed annotation guarantees absence of side effects. - - // This checks assumes the following implementation of await_while - // #define await_while(cond) \ - // for (int tmp = (__VERIFIER_loop_begin(), 0); __VERIFIER_spin_start(), \ - // tmp = cond, __VERIFIER_spin_end(!tmp), tmp;) - return; - } - - // FIXME: The reasoning about safe/unsafe registers is not correct because - // we do not traverse the control-flow but naively go top-down through the loop. - // We need to use proper dominator reasoning! - - // Unsafe means the loop reads from the registers before writing to them. - Set unsafeRegisters = new HashSet<>(); - // Safe means the loop wrote to these register before using them - Set safeRegisters = new HashSet<>(); - + private void collectSideEffects(LoopData loop, LiveRegistersAnalysis liveRegsAna) { + final Set writtenRegisters = new HashSet<>(); Event cur = loop.getStart(); do { + if (cur instanceof RegWriter writer) { + writtenRegisters.add(writer.getResultRegister()); + } if (cur.hasTag(Tag.WRITE) || (cur instanceof FunctionCall call && (!call.isDirectCall() || !call.getCalledFunction().isIntrinsic() || call.getCalledFunction().getIntrinsicInfo().writesMemory()))) { // We assume side effects for all writes, writing intrinsics, and non-intrinsic function calls. - loop.sideEffects.add(cur); - continue; - } - - if (cur instanceof RegReader regReader) { - final Set dataRegs = regReader.getRegisterReads().stream() - .map(Register.Read::register).collect(Collectors.toSet()); - unsafeRegisters.addAll(Sets.difference(dataRegs, safeRegisters)); - } - - if (cur instanceof RegWriter writer) { - if (unsafeRegisters.contains(writer.getResultRegister())) { - // The loop writes to a register it previously read from. - // This means the next loop iteration will observe the newly written value, - // hence the loop is not side effect free. - loop.sideEffects.add(cur); - } else { - safeRegisters.add(writer.getResultRegister()); - } + loop.globalSideEffects.add(cur); } } while ((cur = cur.getSuccessor()) != loop.getEnd().getSuccessor()); - } - - private void reduceToDominatingSideEffects(LoopData loop) { - if (loop.sideEffects.isEmpty()) { - return; - } - - final List sideEffects = loop.sideEffects; - final Event start = loop.getStart(); - final Event end = loop.getEnd(); - final Predicate isAlwaysSideEffectful = (e -> e.cfImpliesExec() && sideEffects.contains(e)); - - final DominatorTree preDominatorTree = DominatorAnalysis.computePreDominatorTree(start, end); - final DominatorTree postDominatorTree = DominatorAnalysis.computePostDominatorTree(start, end); - - // (1) Delete all side effects that are on exit paths (those have no dominator in the post-dominator tree - // because they are no predecessor of the end of the loop body). - final Predicate isOnExitPath = (e -> postDominatorTree.getImmediateDominator(e) == null); - sideEffects.removeIf(isOnExitPath); - - // (2) Check if always side-effect-full at the end of an iteration directly before entering the next one. - // This is an approximation: If the end of the iteration is predominated by some side effect - // then we always observe side effects. - loop.isAlwaysSideEffectful = Streams.stream(preDominatorTree.getDominators(end)).anyMatch(isAlwaysSideEffectful); - if (loop.isAlwaysSideEffectful) { - return; - } - - // (3) Delete all side effects that are dominated by another one - // NOTE: This can be implemented more efficiently, but maybe we don't need to. - for (int i = sideEffects.size() - 1; i >= 0; i--) { - final Event sideEffect = sideEffects.get(i); - final Iterable dominators = Iterables.concat( - preDominatorTree.getStrictDominators(sideEffect), - postDominatorTree.getStrictDominators(sideEffect) - ); - final boolean isDominated = Iterables.tryFind(dominators, isAlwaysSideEffectful::test).isPresent(); - if (isDominated) { - sideEffects.remove(i); - } - } + loop.writtenLiveRegisters.addAll(Sets.intersection( + writtenRegisters, + liveRegsAna.getLiveRegistersAt(loop.getStart()) + )); } private void instrumentLoop(LoopData loop) { - if (loop.isAlwaysSideEffectful) { - return; - } - final TypeFactory types = TypeFactory.getInstance(); final ExpressionFactory expressions = ExpressionFactory.getInstance(); + final Function func = loop.loopInfo.function(); final int loopNum = loop.loopInfo.loopNumber(); + + final AggregateType liveRegsType = types.getAggregateType(Lists.transform(loop.writtenLiveRegisters, Register::getType)); + final Expression liveRegistersVector = expressions.makeConstruct(liveRegsType, loop.writtenLiveRegisters); + final Register entryLiveStateRegister = func.newRegister("__localLiveSnapshot#" + loopNum, liveRegsType); final Register tempReg = func.newRegister("__possiblySideEffectless#" + loopNum, types.getBooleanType()); - final Register trackingReg = func.newRegister("__sideEffect#" + loopNum, types.getBooleanType()); + final Register globalSideEffectReg = func.newRegister("__globalSideEffect#" + loopNum, types.getBooleanType()); + + // ---------------- Instrumentation ---------------- + // Init tracking registers + loop.getStart().insertAfter(List.of( + EventFactory.newLocal(entryLiveStateRegister, liveRegistersVector), + EventFactory.newLocal(globalSideEffectReg, expressions.makeFalse()) + )); - final Event init = EventFactory.newLocal(trackingReg, expressions.makeFalse()); - loop.getStart().insertAfter(init); - for (Event sideEffect : loop.sideEffects) { + // Track global side effects + for (Event sideEffect : loop.globalSideEffects) { final List updateSideEffect = new ArrayList<>(); if (sideEffect.cfImpliesExec()) { - updateSideEffect.add(EventFactory.newLocal(trackingReg, expressions.makeTrue())); + updateSideEffect.add(EventFactory.newLocal(globalSideEffectReg, expressions.makeTrue())); } else { updateSideEffect.addAll(List.of( EventFactory.newExecutionStatus(tempReg, sideEffect), - EventFactory.newLocal(trackingReg, expressions.makeOr(trackingReg, expressions.makeNot(tempReg))) + EventFactory.newLocal(globalSideEffectReg, expressions.makeOr(globalSideEffectReg, expressions.makeNot(tempReg))) )); } sideEffect.getPredecessor().insertAfter(updateSideEffect); } - final Event assumeSideEffect = newSpinTerminator(expressions.makeNot(trackingReg), func); - assumeSideEffect.copyAllMetadataFrom(loop.getStart()); - loop.getEnd().getPredecessor().insertAfter(assumeSideEffect); + // Check if any local or global side effects occurred. If not, spin! + final Register localSideEffectReg = func.newRegister("__localSideEffect#" + loopNum, types.getBooleanType()); + final Expression hasSideEffect = expressions.makeOr(localSideEffectReg, globalSideEffectReg); + + final Event assignLocalSideEffectReg = EventFactory.newLocal(localSideEffectReg, expressions.makeNEQ(entryLiveStateRegister, liveRegistersVector)); + final Event assumeSideEffect = newSpinTerminator(expressions.makeNot(hasSideEffect), loop); + loop.getEnd().getPredecessor().insertAfter(List.of( + assignLocalSideEffectReg, + assumeSideEffect + )); // Special case: If the loop is fully side-effect-free, we can set its unrolling bound to 1. - if (loop.sideEffects.isEmpty()) { + if (loop.isSideEffectFree()) { final Event loopBound = EventFactory.Svcomp.newLoopBound(expressions.makeValue(1, types.getArchType())); loop.getStart().getPredecessor().insertAfter(loopBound); } } - private Event newSpinTerminator(Expression guard, Function func) { + private Event newSpinTerminator(Expression guard, LoopData loop) { + final Function func = loop.getStart().getFunction(); final Event terminator = func instanceof Thread thread ? EventFactory.newJump(guard, (Label) thread.getExit()) : EventFactory.newAbortIf(guard); - terminator.addTags(Tag.SPINLOOP, Tag.NONTERMINATION, Tag.NOOPT); + terminator.addTags(Tag.SPINLOOP, Tag.NONTERMINATION); + terminator.copyAllMetadataFrom(loop.getStart()); return terminator; } private AnalysisStats collectStats(List loops) { - int numPotentialSpinLoops = 0; - int numStaticSpinLoops = 0; - for (LoopData loop : loops) { - if (!loop.isAlwaysSideEffectful) { - numPotentialSpinLoops++; - if (loop.sideEffects.isEmpty()) { - numStaticSpinLoops++; - } - } - } - return new AnalysisStats(numPotentialSpinLoops, numStaticSpinLoops); + int numStaticSpinLoops = Math.toIntExact(loops.stream().filter(LoopData::isSideEffectFree).count()); + return new AnalysisStats( numStaticSpinLoops); } // ================================================================================================== @@ -231,8 +165,12 @@ private AnalysisStats collectStats(List loops) { private static class LoopData { private final LoopAnalysis.LoopInfo loopInfo; - private final List sideEffects = new ArrayList<>(); - private boolean isAlwaysSideEffectful = false; + private final List globalSideEffects = new ArrayList<>(); + private final List writtenLiveRegisters = new ArrayList<>(); + + public boolean isSideEffectFree() { + return writtenLiveRegisters.isEmpty() && globalSideEffects.isEmpty(); + } private LoopData(LoopAnalysis.LoopInfo loopInfo) { this.loopInfo = loopInfo; @@ -248,11 +186,10 @@ public String toString() { } } - private record AnalysisStats(int numPotentialSpinLoops, int numStaticSpinLoops) { + private record AnalysisStats(int numStaticSpinLoops) { private AnalysisStats add(AnalysisStats stats) { - return new AnalysisStats(this.numPotentialSpinLoops + stats.numPotentialSpinLoops, - this.numStaticSpinLoops + stats.numStaticSpinLoops); + return new AnalysisStats(this.numStaticSpinLoops + stats.numStaticSpinLoops); } } } \ No newline at end of file From a8805c755a234631003b71e5166a9f4dcea699b1 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Fri, 22 Nov 2024 17:16:43 +0100 Subject: [PATCH 2/3] Add comment Updated verdict of VMMLocksTest --- .../program/processing/DynamicSpinLoopDetection.java | 1 + .../src/test/java/com/dat3m/dartagnan/c/VMMLocksTest.java | 4 ++-- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicSpinLoopDetection.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicSpinLoopDetection.java index 6ecd748c77..4b58f5d2a3 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicSpinLoopDetection.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicSpinLoopDetection.java @@ -86,6 +86,7 @@ private void collectSideEffects(LoopData loop, LiveRegistersAnalysis liveRegsAna } } while ((cur = cur.getSuccessor()) != loop.getEnd().getSuccessor()); + // Every live register that is written to is a potential local side effect. loop.writtenLiveRegisters.addAll(Sets.intersection( writtenRegisters, liveRegsAna.getLiveRegistersAt(loop.getStart()) diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/VMMLocksTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/VMMLocksTest.java index 271971133e..ce9682ba6c 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/c/VMMLocksTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/c/VMMLocksTest.java @@ -16,10 +16,10 @@ import java.util.EnumSet; import static com.dat3m.dartagnan.configuration.Arch.C11; +import static com.dat3m.dartagnan.configuration.Property.*; import static com.dat3m.dartagnan.utils.ResourceHelper.getTestResourcePath; import static com.dat3m.dartagnan.utils.Result.*; import static org.junit.Assert.assertEquals; -import static com.dat3m.dartagnan.configuration.Property.*; @RunWith(Parameterized.class) public class VMMLocksTest extends AbstractCTest { @@ -82,7 +82,7 @@ public static Iterable data() throws IOException { {"mutex_musl-rel2rx_futex", C11, FAIL}, {"mutex_musl-rel2rx_unlock", C11, FAIL}, {"seqlock", C11, PASS}, - {"clh_mutex", C11, UNKNOWN}, + {"clh_mutex", C11, PASS}, {"clh_mutex-acq2rx", C11, FAIL}, {"ticket_awnsb_mutex", C11, PASS}, {"ticket_awnsb_mutex-acq2rx", C11, FAIL}, From 2f74f61a25033dc8bcba37cb2a80cd6f6576fa49 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Mon, 25 Nov 2024 11:37:24 +0100 Subject: [PATCH 3/3] Added instrumentation description to DynamicSpinLoopDetection --- .../processing/DynamicSpinLoopDetection.java | 22 ++++++++++++++++++- 1 file changed, 21 insertions(+), 1 deletion(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicSpinLoopDetection.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicSpinLoopDetection.java index 4b58f5d2a3..16e787d345 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicSpinLoopDetection.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicSpinLoopDetection.java @@ -33,6 +33,26 @@ This pass instruments loops that do not cause a side effect in an iteration to terminate, i.e., to avoid spinning. In other words, only the last loop iteration is allowed to be side-effect free. + Instrumentation: + loop_header: + __localLiveSnapshot <- ( ) // To track local side effects + __globalSideEffect <- false // To track global side effects + // ---------- Loop body ---------- + ... + __globalSideEffect <- true // Store is a guaranteed global effect + store(...) + ... + // ---------- Backjump ---------- + // Local side effect if value of any live register changed. + __localSideEffect <- __localLiveSnapshot != ( ) + if (!(__localSideEffect || __globalSideEffect)) goto END_OF_T ### SPINLOOP + goto loop_header + + NOTE: "" refers to those registers + (1) that are live inside or after the loop + and (2) that are potentially written to inside the loop (i.e. are not invariant). + + NOTE: This pass is required to detect liveness violations. */ public class DynamicSpinLoopDetection implements ProgramProcessor { @@ -158,7 +178,7 @@ private Event newSpinTerminator(Expression guard, LoopData loop) { private AnalysisStats collectStats(List loops) { int numStaticSpinLoops = Math.toIntExact(loops.stream().filter(LoopData::isSideEffectFree).count()); - return new AnalysisStats( numStaticSpinLoops); + return new AnalysisStats(numStaticSpinLoops); } // ==================================================================================================