Backwards reaching definitions #726

xeren · 2024-09-04T11:50:49Z

This PR decouples an interface for Dependency and UseDefAnalysis, and adds an alternative implementation for it, BackwardsReachingDefinitionsAnalysis (BRDA). It takes into account, that readers on uninitialized registers are unlikely, while final writers are frequent, although rarely useful. This means, that the propagated data is smaller in BRDA, than in the existing forward-directed implementations.
The more noteworthy feature is, that I wrote it to support loops. This means that it, as well as the dependent alias analysis could potentially be done before unrolling.

ThomasHaas · 2024-09-04T11:56:27Z

UseDefAnalysis also supported loops. But I guess your new analysis might be more efficient?

xeren · 2024-09-04T11:59:13Z

Yes, it should have the capabilities of both implementations and be more efficient.

ThomasHaas · 2024-09-04T12:00:58Z

Also, why do you use BranchEquivalence rather than ExecutionAnalysis? I think the latter is more correct because it also considers that instructions may fail to execute.

ThomasHaas · 2024-09-04T12:05:48Z

@hernanponcedeleon Do you remember on which benchmark UseDefAnalysis ran out of memory? I think you had some huge benchmarks where this was a problem. If so, it would be interesting to test this new analysis for efficiency.

xeren · 2024-09-04T12:10:08Z

Also, why do you use BranchEquivalence rather than ExecutionAnalysis? I think the latter is more correct because it also considers that instructions may fail to execute.

Because the cfImpliesExec condition is only needed in the over approximation (the 'may' relation). BranchEquivalence on the other hand, more precisely the areMutuallyExclusive relation, is only needed in the under approximation (the 'conditionally-must' relation). Since the later is optional, BE is not mandatory.

xeren · 2024-09-04T12:12:43Z

By the way, using the analysis has the side effect, that final register encodings are omitted, if the register is not used by the spec. This could be a small issue fixed.

ThomasHaas · 2024-09-04T12:27:07Z

Also, why do you use BranchEquivalence rather than ExecutionAnalysis? I think the latter is more correct because it also considers that instructions may fail to execute.

Because the cfImpliesExec condition is only needed in the over approximation (the 'may' relation). BranchEquivalence on the other hand, more precisely the areMutuallyExclusive relation, is only needed in the under approximation (the 'conditionally-must' relation). Since the later is optional, BE is not mandatory.

I'm not sure I understand. It seems you could just use ExecutionAnalysis.areMutuallyExclusive in your code to both simplify it and be more accurate (in theory). Conceptually, when analysing dataflow you care about executed instructions rather than instructions in the control-flow.
It likely won't make a practical difference in your use-case, because the ExecutionAnalysis is based only on control-flow but I don't see why your analysis should be aware of that and "optimize" for it.

...src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java

hernanponcedeleon · 2024-09-05T08:44:35Z

@hernanponcedeleon Do you remember on which benchmark UseDefAnalysis ran out of memory? I think you had some huge benchmarks where this was a problem. If so, it would be interesting to test this new analysis for efficiency.

I don't really remember which benchmark that was. But I can try this in some of our larger ones.

Co-authored-by: Hernan Ponce de Leon <[email protected]>

hernanponcedeleon · 2024-09-06T18:17:59Z

This means, that the propagated data is smaller in BRDA, than in the existing forward-directed implementations.

Which part of our pipelines are (positively) affected by this? E.g., does the alias analysis potentially becomes more precise? Do we get smaller mayset in idd?

ThomasHaas · 2024-09-06T18:35:10Z

I think this statement is not about precision but just about memory consumption. The forward-directed implementation kept information about (last) register writes even if those registers were never going to get used again.

xeren · 2024-09-09T15:46:48Z

Which part of our pipelines are (positively) affected by this? E.g., does the alias analysis potentially becomes more precise? Do we get smaller mayset in idd?

Compared to UseDefAnalysis and Dependency, the results of BRDA for any RegReader should be exactly the same. So, any dependent analysis should be relatively unaffected, up until the encoder. idd stays the same. With propagated data, I just meant the internal updates of BRDA and Dependency. At best, there could be side effects on BRDA's querying performance, based on the data layout I chose, i.e. the time it needs to fetch a list of writers.

Since UseDefAnalysis and Dependency are unused now, I probably should add the following options, before merging.

program.processing.loopBounds.useDefAnalysis = {FORWARD, BACKWARD}
program.analysis.reachingDefinitions = {FORWARD, BACKWARD}

ThomasHaas · 2024-09-09T15:48:52Z

If the analysis work fine, I don't think we need to keep around the unused options.

…ackwards-reaching-definitions

hernanponcedeleon · 2024-09-10T07:42:16Z

Keeping two implementations of the analysis might be good: if we encounter any example where one is too slow, we can try another (similar to what happened with the alias analysis and wsq.c).

However, keeping options for each single pass making use of the analysis seems too fine-grained without much clear benefit. I would rather always use forward or always us backwards.

dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java

hernanponcedeleon · 2024-09-10T07:53:55Z

...src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java

+/**
+ * Collects all direct usage relationships between {@link RegWriter} and {@link RegReader}.
+ * <p>
+ * In contrast to a usual Reaching-Definitions-Analysis,
+ * this implementation analyzes the program from back to front,
+ * assigning each program point the set of readers,
+ * who may still require a register initialization.
+ * This means that it does not collect definitions for unused registers.
+ * Especially, it does not collect last writers for all registers.
+ * <p>
+ * This analysis is control-flow-sensitive;
+ * that is, {@link Label} splits the information among the jumps to it
+ * and {@link CondJump} merges the information.
+ * <p>
+ * This analysis supports loops;
+ * that is, backward jumps cause re-evaluation of the loop body until convergence.
+ * This results in a squared worst-case time complexity in terms of events being processed.
+ */


Can you somehow format the doc? It hurst my eyes that widths are so uneven XD

hernanponcedeleon · 2024-09-10T07:57:25Z

...src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java

+    public Writers getWriters(RegReader reader) {
+        Preconditions.checkNotNull(reader, "reader is null");
+        final ReaderInfo result = readerMap.get(reader);
+        Preconditions.checkArgument(result != null, "reader %s has not been analyzed.", reader);


probably it should be checkState

Valid, if reader.getFunction() had been analyzed by this. I considered more likely, that a user would try to query events of another function or program.

...src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java

hernanponcedeleon · 2024-09-10T08:00:33Z

...src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java

+    }
+
+    /**
+     * Analyzes an entire set of threads.


"an entire set of threads." -> "the entire program (after thread creation)" ... you are not passing any threads as parameter

hernanponcedeleon · 2024-09-10T08:23:17Z

...src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java

+        for (Event event : function.getEvents()) {
+            if (event instanceof RegWriter writer) {
+                writerMap.put(writer, new Readers());
+            }
+        }
+        writerMap.put(null, new Readers());
+        for (Event event : function.getEvents()) {
+            if (event instanceof RegReader reader) {
+                final Set<Register> usedRegisters = new HashSet<>();
+                for (Register.Read read : reader.getRegisterReads()) {
+                    usedRegisters.add(read.register());
+                }
+                readerMap.put(reader, new ReaderInfo(usedRegisters));
+            }
+        }
+        readerMap.put(null, new ReaderInfo(finalRegisters));


Why not process everything in the same loop iteration? I don't see any dependency from the second loop tot eh first one.

Also, what are these X.put(null, ...) representing?

The null entry is likely for reads from uninitialized registers.
I agree about the loop: either you merge them or you keep them and iterate over getEvents(RegWriter.class) resp. getEvents(RegReader.class) to skip the instanceof checks.

The null entry is likely for reads from uninitialized registers.

Whatever this is used for, it should be documented, I don't want someone reading the code to have to guess

Yep, since there are no dependencies, both versions are valid. I consider my version better in terms of cache optimization, but not by much.

In writerMap, null stands for the initial writer(s). In readerMap, it denotes the final reader(s). Both cases don't have actual Event instances. In this analysis, they behave as if they had. For readability, I added named null constants.

...src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java

dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java

dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java

ThomasHaas · 2024-09-10T09:42:40Z

...src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java

+            analysis.run(function, finalRegisters);
+        }
+        analysis.postProcess();
+        if (exec != null && program.isUnrolled()) {


The analysis can be run during processing where ExecutionAnalysis is not available, but it can also be run afterwards. In the former case it should subsume UseDefAnalysis and in the latter case Dependency.

...src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java

ThomasHaas · 2024-09-10T09:48:08Z

...src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java

+        for (Event event : function.getEvents()) {
+            if (event instanceof RegWriter writer) {
+                writerMap.put(writer, new Readers());
+            }
+        }
+        writerMap.put(null, new Readers());
+        for (Event event : function.getEvents()) {
+            if (event instanceof RegReader reader) {
+                final Set<Register> usedRegisters = new HashSet<>();
+                for (Register.Read read : reader.getRegisterReads()) {
+                    usedRegisters.add(read.register());
+                }
+                readerMap.put(reader, new ReaderInfo(usedRegisters));
+            }
+        }
+        readerMap.put(null, new ReaderInfo(finalRegisters));


The null entry is likely for reads from uninitialized registers.
I agree about the loop: either you merge them or you keep them and iterate over getEvents(RegWriter.class) resp. getEvents(RegReader.class) to skip the instanceof checks.

...src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java

ThomasHaas · 2024-09-13T12:03:27Z

Anything that needs to be done here? I have not checked the algorithmic details, but given that all tests pass it is likely working as intended.

hernanponcedeleon · 2024-09-13T12:05:40Z

Unless I missed something, not all comments were fixed. From the top of my head:

we still have fine grained options that I don't like
some of the preconditions / checks need to be streamlined

…ackwards-reaching-definitions # Conflicts: # dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java # dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java # dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java # dartagnan/src/main/java/com/dat3m/dartagnan/utils/options/BaseOptions.java # dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java # dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java # dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java # dartagnan/src/test/java/com/dat3m/dartagnan/utils/rules/Providers.java

… into backwards-reaching-definitions

Remove NaiveLoopBoundAnnotation.newInstance() Add NaiveLoopBoundAnnotation.fromConfig(Configuration) Add ReachingDefinitionsAnalysis.configure(Configuration) Set BackwardsReachingDefinitionsAnalysis package-private

hernanponcedeleon · 2024-09-20T18:27:56Z

I think all my comments have been solved. Unless @ThomasHaas has some more comments, I'll merge

ThomasHaas

LGTM

ThomasHaas and others added 7 commits September 3, 2024 21:12

Improved liveness detection for store exclusives (#722)

6326445

Renamed Location to FinalMemoryValue. (#725)

5e10cda

Add ReachingDefinitionsAnalysis

2d5695e

Add BackwardsReachingDefinitionsAnalysis

27cee4f

Replace Dependency with BackwardsReachingDefinitionsAnalysis

c12af07

Replace UseDefAnalysis with BackwardsReachingDefinitionsAnalysis

ae5c2bc

Add AnalysisTest.reachingDefinitionSupportsLoops

38bd709

xeren changed the base branch from master to development September 4, 2024 11:51

ThomasHaas reviewed Sep 4, 2024

View reviewed changes

...src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java Outdated Show resolved Hide resolved

Suggested changes

494ebb7

ThomasHaas and others added 5 commits September 5, 2024 10:46

Add support to CAAT for SyncBar, SyncFence and Vloc relations (#724)

7887589

Add unrolling bound to program spec encoding (#727)

1bd4bd0

Merge branch 'development' into backwards-reaching-definitions

ecd5d7e

Add option to dump encoding to smtlib2 file (#721)

3e6f247

Use correct smtlib2 syntax for push/pop (#728)

669e83a

Co-authored-by: Hernan Ponce de Leon <[email protected]>

xeren added enhancement performance ready-for-review labels Sep 9, 2024

xeren added 2 commits September 9, 2024 18:14

Add options to access previous implementations.

28bbd11

Merge remote-tracking branch 'refs/remotes/origin/development' into b…

78c0f90

…ackwards-reaching-definitions

hernanponcedeleon reviewed Sep 10, 2024

View reviewed changes

ThomasHaas reviewed Sep 10, 2024

View reviewed changes

Refactor

c0d8a38

ThomasHaas reviewed Sep 10, 2024

View reviewed changes

...src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java Outdated Show resolved Hide resolved

Refactor

bf0c691

hernanponcedeleon force-pushed the development branch from 479e85e to e04d77d Compare September 16, 2024 10:05

xeren added 4 commits September 20, 2024 17:47

fixup! Merge remote-tracking branch 'refs/remotes/origin/development'…

0db0bb7

… into backwards-reaching-definitions

Remove option program.processing.loopBounds.useDefAnalysis

b8f136f

Remove NaiveLoopBoundAnnotation.newInstance() Add NaiveLoopBoundAnnotation.fromConfig(Configuration) Add ReachingDefinitionsAnalysis.configure(Configuration) Set BackwardsReachingDefinitionsAnalysis package-private

Small reformat

e91f205

ThomasHaas approved these changes Sep 21, 2024

View reviewed changes

hernanponcedeleon merged commit 73ba96c into development Sep 21, 2024
1 check passed

hernanponcedeleon deleted the backwards-reaching-definitions branch September 21, 2024 06:55

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Backwards reaching definitions #726

Backwards reaching definitions #726

xeren commented Sep 4, 2024

ThomasHaas commented Sep 4, 2024

xeren commented Sep 4, 2024

ThomasHaas commented Sep 4, 2024

ThomasHaas commented Sep 4, 2024

xeren commented Sep 4, 2024

xeren commented Sep 4, 2024

ThomasHaas commented Sep 4, 2024

hernanponcedeleon commented Sep 5, 2024

hernanponcedeleon commented Sep 6, 2024

ThomasHaas commented Sep 6, 2024

xeren commented Sep 9, 2024

ThomasHaas commented Sep 9, 2024

hernanponcedeleon commented Sep 10, 2024

hernanponcedeleon Sep 10, 2024

hernanponcedeleon Sep 10, 2024

xeren Sep 10, 2024

hernanponcedeleon Sep 10, 2024

hernanponcedeleon Sep 10, 2024

ThomasHaas Sep 10, 2024

hernanponcedeleon Sep 10, 2024

xeren Sep 10, 2024

ThomasHaas Sep 10, 2024

ThomasHaas Sep 10, 2024

ThomasHaas commented Sep 13, 2024

hernanponcedeleon commented Sep 13, 2024

hernanponcedeleon commented Sep 20, 2024

ThomasHaas left a comment

Backwards reaching definitions #726

Backwards reaching definitions #726

Conversation

xeren commented Sep 4, 2024

ThomasHaas commented Sep 4, 2024

xeren commented Sep 4, 2024

ThomasHaas commented Sep 4, 2024

ThomasHaas commented Sep 4, 2024

xeren commented Sep 4, 2024

xeren commented Sep 4, 2024

ThomasHaas commented Sep 4, 2024

hernanponcedeleon commented Sep 5, 2024

hernanponcedeleon commented Sep 6, 2024

ThomasHaas commented Sep 6, 2024

xeren commented Sep 9, 2024

ThomasHaas commented Sep 9, 2024

hernanponcedeleon commented Sep 10, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ThomasHaas commented Sep 13, 2024

hernanponcedeleon commented Sep 13, 2024

hernanponcedeleon commented Sep 20, 2024

ThomasHaas left a comment

Choose a reason for hiding this comment