[analysis] Add a "Shared" lattice to represent shared state #6067

tlively · 2023-10-31T02:44:31Z

The analysis framework stores a separate lattice element for each basic block
being analyzed to represent the program state at the beginning of the block.
However, in many analyses a significant portion of program state is not
flow-sensitive, so does not benefit from having a separate copy per block. For
example, an analysis might track constraints on the types of locals that do not
vary across blocks, so it really only needs a single copy of the constrains for
each local. It would be correct to simply duplicate the state across blocks
anyway, but it would not be efficient.

To make it possible to share a single copy of a lattice element across basic
blocks, introduce a Shared<L> lattice. Mathematically, this lattice represents
a single ascending chain in the underlying lattice and its elements are ordered
according to sequence numbers corresponding to positions in that chain.
Concretely, though, the Shared<L> lattice only ever materializes a single,
monotonically increasing element of L and all of its elements provide access
to that shared underlying element.

Shared<L> will let us get the benefits of having mutable shared state in the
concrete implementation of analyses without losing the benefits of keeping those
analyses expressible purely in terms of the monotone framework.

tlively · 2023-10-31T02:44:49Z

Current dependencies on/for this PR:

main
- PR [analysis][NFC] Rename parameters to join and meet methods #6056
  - PR [analysis] Implement an array lattice #6057
    - PR [analysis] Implement a vector lattice #6058
      - PR [analysis] Add a tuple lattice #6062
        
        PR [analysis] Add a lattice for value types #6064
        
        PR [analysis][NFC] Refactor lattice unit tests #6065
        
        PR [analysis] Add a "Shared" lattice to represent shared state #6067 👈
        
        PR [analysis] Simplify the stack lattice #6069
        
        PR [analysis] Allow joining a single vector element efficiently #6071
        
        PR [analysis] Add a generic powerset lattice #6059

This stack of pull requests is managed by Graphite.

kripken · 2023-10-31T19:37:37Z

Mathematically, this lattice represents a single ascending chain in the underlying lattice

I followed up to here, and I got stuck.

Can you maybe give a concrete example of this?

As context, after reading the first paragraph I was expecting to see something like a "wrapper" for a lattice element that allows us to refer to an element without copying it. But I don't know why we need some new kind of structure here (the new chain) or even what that precisely means.

tlively · 2023-10-31T22:10:11Z

Unfortunately we can't just have a std::shared_ptr to a mutable underlying lattice element and call it a day, even though that's kind of what we would like to have. This new lattice needs to be a lattice so that it fits properly into the framework. This isn't just to make the compiler happy; it's important that join returns true to the analysis worklist algorithm when and only when a block needs to be re-analyzed because its input has changed since the last time it was analyzed.

To determine whether a block needs to be re-analyzed, we keep a sequence number alongside the pointer to the shared underlying element. When we propagate new results to the beginning of the block, we know the block needs to be re-analyzed if and only if the propagated sequence number is higher than the old sequence number. Every time the value of the shared underlying element increases, we increase the current sequence number so that any block that was analyzed based on a previous value will be re-analyzed.

The sequence numbers are an important part of getting the new lattice to do what we need it to do, but they're also mathematically interesting because each successive sequence number corresponds to a higher value that the shared underlying element has taken on at some point in time. The sequence of those values through time form an increasing chain in the underlying lattice and the sequence numbers are both timestamps and indices into that chain.

It's also nice to know that this Shared utility isn't just a hack to get shared, mutable state into the framework. It's actually a mathematically justifiable lattice. That gives me more confidence that it won't end up violating core assumptions and requiring hacky workarounds or special casing in the future.

The analysis framework stores a separate lattice element for each basic block being analyzed to represent the program state at the beginning of the block. However, in many analyses a significant portion of program state is not flow-sensitive, so does not benefit from having a separate copy per block. For example, an analysis might track constraints on the types of locals that do not vary across blocks, so it really only needs a single copy of the constrains for each local. It would be correct to simply duplicate the state across blocks anyway, but it would not be efficient. To make it possible to share a single copy of a lattice element across basic blocks, introduce a `Shared<L>` lattice. Mathematically, this lattice represents a single ascending chain in the underlying lattice and its elements are ordered according to sequence numbers corresponding to positions in that chain. Concretely, though, the `Shared<L>` lattice only ever materializes a single, monotonically increasing element of `L` and all of its elements provide access to that shared underlying element. `Shared<L>` will let us get the benefits of having mutable shared state in the concrete implementation of analyses without losing the benefits of keeping those analyses expressible purely in terms of the monotone framework.

kripken

Thanks, the idea now makes sense to me, and lgtm % comments

kripken · 2023-11-01T20:27:51Z

src/analysis/lattices/shared.h

+// Internally, there is only ever a single monotonically increasing element of L
+// materialized. Dereferencing any element of the Shared lattice will produce
+// the current value of that single element of L, which is generally safe
+// because the current value always overapproximates the value at the time of


What does "overapproximate" mean here? A "higher" value in the lattice L?

kripken · 2023-11-01T20:28:55Z

src/analysis/lattices/shared.h

+template<Lattice L> struct Shared {
+  class Element {
+    const typename L::Element* val;
+    uint32_t seq = 0;


It would be great to see some of the comments in the PR itself added as comments here, to explain what seq is etc.

kripken · 2023-11-01T20:33:31Z

src/analysis/lattices/shared.h

+  // sequence number. The sequence numbers monotonically increase along with
+  // `val` and serve to provide ordering between elements of this lattice.
+  mutable typename L::Element val;
+  mutable uint32_t seq = 0;


This will be the 2nd and 3rd time we use mutable in this entire codebase... can we avoid that?

If we can't please add a comment explaining why this dangerous pattern is necessary here.

kripken · 2023-11-01T20:36:54Z

src/analysis/lattices/shared.h

+template<Lattice L> struct Shared {
+  class Element {
+    const typename L::Element* val;
+    uint32_t seq = 0;


Suggested change

uint32_t seq = 0;

Index seq = 0;

Index seems appropriate as this number is tied to the number of basic blocks (and iterations on them), which is tied to maximum sizes in wasm files. That is, if wasm supports more then 32 bits here, we'd want this type to change, which Index will do for us.

This number is not tied to the number of basic blocks. It is the number of times the shared value is increased, which can be dramatically higher than the number of basic blocks. Since analysis continues to a fixed point, it can visit basic blocks an unbounded number of times and each visit to a basic block may potentially increase the value multiple times.

Since this isn't actually an index into anything that is ever materialized, I would prefer to keep it a uint32_t for now, or possibly make it a uint64_t right now.

sgtm. How about using a name for it for convenience later if we need to change it, using Seq = uint32_t; ?

kripken · 2023-11-01T20:47:01Z

test/gtest/lattices.cpp

+
+  auto zero = shared.getBottom();
+
+  auto one = zero;


I am having trouble reading a line that says literally 1 == 0...

(And later down I see 2 == 1. By induction, all natural numbers are apparently 0... 🤔 😆 )

How about a, b, c?

The only way to increase a shared value is via a join, so to create our one value we have to start from zero and add one via the join on the next line. I'll clarify this in the code.

kripken · 2023-11-01T20:49:55Z

test/gtest/lattices.cpp

+
+  EXPECT_EQ(shared.compare(one, zero), analysis::GREATER);
+  EXPECT_EQ(shared.compare(one, one), analysis::EQUAL);
+  EXPECT_EQ(shared.compare(one, uno), analysis::EQUAL);


To make sure I follow, uno had an extra join done on it, but it was of the same value as we had before, so the sequence number was not increased, hence it is equal to one?

That's right 👍

tlively · 2023-11-02T18:30:44Z

Merge activity

Nov 2, 2:30 PM: @tlively started a stack merge that includes this pull request via Graphite.
Nov 2, 2:31 PM: @tlively merged this pull request with Graphite.

…bly#6067) The analysis framework stores a separate lattice element for each basic block being analyzed to represent the program state at the beginning of the block. However, in many analyses a significant portion of program state is not flow-sensitive, so does not benefit from having a separate copy per block. For example, an analysis might track constraints on the types of locals that do not vary across blocks, so it really only needs a single copy of the constrains for each local. It would be correct to simply duplicate the state across blocks anyway, but it would not be efficient. To make it possible to share a single copy of a lattice element across basic blocks, introduce a `Shared<L>` lattice. Mathematically, this lattice represents a single ascending chain in the underlying lattice and its elements are ordered according to sequence numbers corresponding to positions in that chain. Concretely, though, the `Shared<L>` lattice only ever materializes a single, monotonically increasing element of `L` and all of its elements provide access to that shared underlying element. `Shared<L>` will let us get the benefits of having mutable shared state in the concrete implementation of analyses without losing the benefits of keeping those analyses expressible purely in terms of the monotone framework.

tlively requested review from ashleynh and kripken October 31, 2023 02:44

tlively force-pushed the refactor-lattice-gtest branch from 518957f to e8e0ab4 Compare October 31, 2023 17:39

tlively force-pushed the shared-lattice branch from 09b5289 to 5527cd0 Compare October 31, 2023 17:39

tlively force-pushed the refactor-lattice-gtest branch from e8e0ab4 to f65d8a0 Compare November 1, 2023 01:19

tlively force-pushed the shared-lattice branch from cc7fb30 to b30a19c Compare November 1, 2023 01:20

tlively mentioned this pull request Nov 1, 2023

[analysis] Simplify the stack lattice #6069

Merged

tlively force-pushed the refactor-lattice-gtest branch from f65d8a0 to 3e6b7dd Compare November 1, 2023 17:16

Base automatically changed from refactor-lattice-gtest to main November 1, 2023 18:09

tlively added 3 commits November 1, 2023 12:36

fix include for uint32_t

7946e15

include utility header to fix lint

bb58f6f

tlively force-pushed the shared-lattice branch from 9a4797e to bb58f6f Compare November 1, 2023 19:37

tlively mentioned this pull request Nov 1, 2023

[analysis] Allow joining a single vector element efficiently #6071

Merged

kripken reviewed Nov 1, 2023

View reviewed changes

address comments

abf9232

kripken approved these changes Nov 2, 2023

View reviewed changes

tlively merged commit bc88d5d into main Nov 2, 2023

tlively deleted the shared-lattice branch November 2, 2023 18:31

[analysis] Add a "Shared" lattice to represent shared state #6067

[analysis] Add a "Shared" lattice to represent shared state #6067

Uh oh!

Conversation

tlively commented Oct 31, 2023

Uh oh!

tlively commented Oct 31, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

kripken commented Oct 31, 2023

Uh oh!

tlively commented Oct 31, 2023

Uh oh!

kripken left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tlively commented Nov 2, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Merge activity

Uh oh!

Uh oh!

tlively commented Oct 31, 2023 •

edited

Loading

tlively commented Nov 2, 2023 •

edited

Loading