Skip to content

Commit e938d75

Browse files
lqdlqd
authored
Propose 2025h2 goal for polonius alpha (#341)
* Add 2025h2 goal for polonius alpha * expand axioms and motivation * add examples add code examples that the analysis accepts, and others that it still doesn't accept * fmt
1 parent 98926a9 commit e938d75

File tree

1 file changed

+313
-0
lines changed

1 file changed

+313
-0
lines changed

‎src/2025h2/polonius.md

Lines changed: 313 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,313 @@
1+
# Stabilizable Polonius support on nightly
2+
3+
| Metadata | |
4+
|:-----------------|------------------------------------|
5+
| Point of contact | @lqd |
6+
| Teams | <!-- TEAMS WITH ASKS --> |
7+
| Task owners | <!-- TASK OWNERS --> |
8+
| Status | Proposed |
9+
| Tracking issue | [rust-lang/rust-project-goals#118] |
10+
| Zulip channel | [#t-types/polonius][channel] |
11+
12+
[channel]: https://rust-lang.zulipchat.com/#narrow/channel/186049-t-types.2Fpolonius
13+
14+
15+
## Summary
16+
17+
Make a stabilizable version of the [polonius][pc3] next generation borrow checking "alpha" algorithm. This [revision of the analysis][alpha], while less powerful than we hoped, currently scales better than the previous [datalog] implementation, and accepts the main problem case we deferred from NLLs: it handles almost all our in-tree tests, passes perf runs (but is still too slow) and crater runs without issues. It's therefore a worthwhile step to ship to users, but needs more work to be properly usable on nightly.
18+
19+
This goal is a continuation of the [2025h1 goal](https://rust-lang.github.io/rust-project-goals/2025h1/Polonius.html).
20+
21+
[datalog]: https://github.com/rust-lang/polonius
22+
[alpha]: https://github.com/rust-lang/rust/pull/143093
23+
24+
## Motivation
25+
26+
Polonius is an improved version of the borrow checker that [resolves common limitations of the borrow checker][pc3] and which is needed to support future patterns such as "lending iterators" (see [#92985]). Its model also prepares us for further improvements in the future.
27+
28+
In the previous goal periods, we have landed prototypes of the analysis on nightly, and have a [functional version][alpha] that we think is worthwhile to stabilize, even if it's not the full version handling all issues related to flow-sensitivity during borrow-checking.
29+
30+
The key achievements from our past work are:
31+
* identifying this actionable subset
32+
* implementing and evaluating a functional prototype
33+
* identifying other phases we wish to explore later, to gradually improve the precision of the analysis
34+
35+
[pc3]: https://blog.rust-lang.org/inside-rust/2023/10/06/polonius-update.html#background-on-polonius
36+
[#92985]: https://github.com/rust-lang/rust/issues/92985
37+
38+
The design for the polonius $\alpha$ analysis (modulo SCCs) can be summarized as:
39+
40+
* with the CFG $\mathcal{C}$, and the subset graph
41+
* compute a "unified graph" $\mathcal{U}$ where
42+
* nodes are "region $r$ at point $p$"
43+
* add outlives edges from type-checking: subset edges between regions $r_0 \subseteq r_1$, at the point $p$ where the constraint occurs
44+
* add liveness edges: if there is an edge $p\rightarrow q \in \mathcal{C}$ and the region $r_1$ is live at $q$
45+
* make an edge $r_1$ at $p$ to $r_1$ at $q$
46+
* respecting variance (forward, backward, or bidirectional)
47+
* "liveness" of a variable is from standard compiler analysis
48+
* with subtleties about "use" liveness and "drop" liveness
49+
* "liveness" of a region $r$ at point $p$ is:
50+
* $r$ is in the type of a variable $v$ live at $p$
51+
* "liveness" of a loan $l$ at point $p$ is:
52+
* there exists a live region $r$ where the loan $l$ can reach $r$ in the "unified graph" $\mathcal{U}$ from its introduction region/point node.
53+
* then we do the usual loans-in-scope computation where a
54+
* GEN is the loan being introduced
55+
* KILL is the loan stops being live and/or the place is overwritten
56+
* and using these loans in scope when checking for place invalidations
57+
58+
The alpha version of the analysis uses reachability within the subset+cfg graph to approximate liveness, and uses the same loan-in-scope computation to handle kills as NLLs.
59+
60+
#### Examples that the alpha analysis accepts
61+
62+
The majority of open issues marked NLL-deferred, and fixed-by-polonius, would be fixed: their MCVEs are now being accepted by the alpha analysis.
63+
64+
The most impactful example is the "NLL problem case 3" and variations of it, that were deferred from the NLL implementation.
65+
66+
```rust
67+
use std::collections::HashMap;
68+
use std::hash::Hash;
69+
70+
fn from_the_nll_rfc<'r, K: Hash + Eq + Copy, V: Default>(
71+
map: &'r mut HashMap<K, V>,
72+
key: K,
73+
) -> &'r mut V {
74+
match map.get_mut(&key) {
75+
Some(value) => value,
76+
None => {
77+
map.insert(key, V::default());
78+
map.get_mut(&key).unwrap()
79+
}
80+
}
81+
}
82+
```
83+
84+
A similar variation is the filtering lending iterator.
85+
86+
```rust
87+
trait LendingIterator {
88+
type Item<'a>
89+
where
90+
Self: 'a;
91+
fn next(&mut self) -> Option<Self::Item<'_>>;
92+
93+
fn filter<P>(self, predicate: P) -> Filter<Self, P>
94+
where
95+
Self: Sized,
96+
P: FnMut(&Self::Item<'_>) -> bool,
97+
{
98+
Filter { iter: self, predicate }
99+
}
100+
}
101+
102+
pub struct Filter<I, P> {
103+
iter: I,
104+
predicate: P,
105+
}
106+
impl<I: LendingIterator, P> LendingIterator for Filter<I, P>
107+
where
108+
P: FnMut(&I::Item<'_>) -> bool,
109+
{
110+
type Item<'a>
111+
= I::Item<'a>
112+
where
113+
Self: 'a;
114+
115+
// This is now accepted
116+
fn next(&mut self) -> Option<I::Item<'_>> {
117+
while let Some(item) = self.iter.next() {
118+
if (self.predicate)(&item) {
119+
return Some(item);
120+
}
121+
}
122+
return None;
123+
}
124+
}
125+
```
126+
127+
(Note that this doesn't make lending iterators themselves easier to use, due to the unrelated limitations in GATs themselves.)
128+
129+
#### Examples that the alpha analysis does not accept
130+
131+
Some cases that require full flow-sensitivity are left for future improvements, and show the same imprecision as NLLs today. For example, some patterns of linked-list traversals with a cursor. There are a handful of open issues like these.
132+
133+
```rust
134+
struct X {
135+
next: Option<Box<X>>,
136+
}
137+
```
138+
139+
This is showing the same imprecision as NLLs discussed above:
140+
141+
```rust
142+
fn conditional() {
143+
let mut b = Some(Box::new(X { next: None }));
144+
let mut p = &mut b;
145+
while let Some(now) = p {
146+
// ^ ERROR: cannot use `*p` because it was mutably borrowed
147+
if true {
148+
p = &mut now.next;
149+
}
150+
}
151+
}
152+
```
153+
154+
While this is still accepted:
155+
156+
```rust
157+
fn no_control_flow() {
158+
let mut b = Some(Box::new(X { next: None }));
159+
let mut p = &mut b;
160+
while let Some(now) = p {
161+
p = &mut now.next;
162+
}
163+
}
164+
165+
fn conditional_with_indirection() {
166+
let mut b = Some(Box::new(X { next: None }));
167+
let mut p = &mut b;
168+
while let Some(now) = p {
169+
if true {
170+
p = &mut p.as_mut().unwrap().next;
171+
}
172+
}
173+
}
174+
```
175+
176+
Similarly,
177+
178+
```rust
179+
struct Node<T> {
180+
value: T,
181+
next: Option<Box<Self>>,
182+
}
183+
184+
type List<T> = Option<Box<Node<T>>>;
185+
186+
fn remove_last_node_recursive<T>(node_ref: &mut List<T>) {
187+
let next_ref = &mut node_ref.as_mut().unwrap().next;
188+
189+
if next_ref.is_some() {
190+
remove_last_node_recursive(next_ref);
191+
} else {
192+
*node_ref = None;
193+
}
194+
}
195+
196+
fn remove_last_node_iterative<T>(mut node_ref: &mut List<T>) {
197+
loop {
198+
let next_ref = &mut node_ref.as_mut().unwrap().next;
199+
200+
if next_ref.is_some() {
201+
node_ref = next_ref;
202+
} else {
203+
break;
204+
}
205+
}
206+
207+
*node_ref = None;
208+
// ^ ERROR cannot assign to `*node_ref` because it is borrowed
209+
}
210+
```
211+
212+
Or another pattern requiring full flow-sensitivity like the following
213+
214+
```rust
215+
use std::cell::Cell;
216+
217+
struct Invariant<'l>(Cell<&'l ()>);
218+
219+
fn create_invariant<'l>() -> Invariant<'l> {
220+
Invariant(Cell::new(&()))
221+
}
222+
223+
// Fails
224+
fn use_it<'a, 'b>(choice: bool) -> Result<Invariant<'a>, Invariant<'b>> {
225+
let returned_value = create_invariant();
226+
if choice { Ok(returned_value) } else { Err(returned_value) }
227+
}
228+
229+
// OK
230+
fn use_it2<'a: 'b, 'b: 'a>(choice: bool) -> Result<Invariant<'a>, Invariant<'b>> {
231+
let returned_value = create_invariant();
232+
if choice { Ok(returned_value) } else { Err(returned_value) }
233+
}
234+
```
235+
236+
### The next six months
237+
238+
* Complete the remaining features we need to support, like member constraints, and fix the last couple diagnostics differences with NLLs
239+
* Keep improving testing and validation
240+
* continue to expand our test coverage
241+
* validate and triage open issues marked as NLL-deferred and fixed-by-polonius for the alpha-version of the analysis
242+
* hopefully compare behavior with future formal works, e.g. in [`a-mir-formality`](https://github.com/rust-lang/a-mir-formality/)
243+
* maybe identify interesting benchmarks or stress tests
244+
* Refactor, or rewrite, the implementation to reduce overhead, for example by:
245+
* doing reachability analysis over the CFG + subset graph separately, versus building an entirely new graph like we do today
246+
* making the algorithm incremental, or lazy, so that more complicated walks only do a subset of the entire graph and incrementally build the same data for every place that is invalidated
247+
* reworking the analysis to use the region graph SCCs, which is also needed to support member constraints
248+
* Make that overhead visible in fewer cases
249+
* either by making NLLs itself more lazy, and reducing its own overhead,
250+
* or computing "possible errors" cheaply,
251+
* or having a good way to switch from one analysis to the other, e.g. only do the more expensive analysis if there's an NLL error (like the NLL migrate mode was used to transition away from AST borrowck)
252+
253+
### The "shiny future" we are working towards
254+
255+
Stable support for the polonius alpha analysis, before gradually improving expressiveness, by capitalizing on the insights gathered during the previous goal periods.
256+
257+
## Design axioms
258+
259+
The older datalog implementation can accept more exotic borrowing patterns, as it (slowly) elaborates all the data needed to handle full flow-sensitivity, but it also doesn't scale, has no path to stabilization and suffers from other shortcomings. In order to not let "perfect be the enemy of good", we've chosen to reduce the scope to a manageable subset that we can ship sooner rather than later.
260+
261+
NLL problem case 3, and the like, are a common issue encountered by users, and we believe handling these kinds of patterns is worthwhile, without needing to wait for a solution to handle even more cases. Especially as we think these cases are encountered more rarely than the new cases we'll accept.
262+
263+
## Ownership and team asks
264+
265+
**Owner:** lqd
266+
267+
Other support provided by @amandasystems as part of her PhD.
268+
269+
| Task | Owner(s) or team(s) | Notes |
270+
| ---------------- | -------------------- | ------------------------- |
271+
| Design review | @nikomatsakis | |
272+
| Implementation | @lqd, @amandasystems | |
273+
| Standard reviews | ![Team][] [types] | @jackh726, @matthewjasper |
274+
275+
### Support needed from the project
276+
277+
We expect most support to be needed from the types team, for design, reviews, interactions with the trait solver, and so on. We expect @nikomatsakis, leading the polonius working group and design, to provide guidance and design time, and @jackh726 and @matthewjasper to help with reviews.
278+
279+
## Outputs and milestones
280+
281+
### Outputs
282+
283+
Nightly implementation of polonius that passes [NLL problem case #3][pc3] and accepts lending iterators ([#92985]).
284+
285+
This implementation should be good enough to be stabilizable, both in features and performance, should pass the full test suite, do crater runs, and test it on CI.
286+
287+
As our model is a superset of NLLs, we expect little to no diagnostics regressions, but improvements would probably still be needed for the new errors.
288+
289+
### Milestones
290+
291+
Note: some of these are currently being worked on and close to being done, and could be completed before the 2025h2 period.
292+
293+
| Milestone | Owner | Notes |
294+
| ---------------------------------------------------------------------------------- | -------------- | ----------- |
295+
| Factoring out higher-ranked concerns from the main path | @amandasystems | |
296+
| ↳ [x] rewrite invalid universe constraints with outlives `'static` constraints | | |
297+
| ↳ [ ] completely remove placeholders | | in progress, PR [#130227](https://github.com/rust-lang/rust/pull/130227) |
298+
| Location-sensitive prototype on nightly | @lqd | |
299+
| ↳ [x] create structures for location-dependent outlives constraints | | |
300+
| ↳ [x] build new constraint graph from typeck constraints and liveness constraints | | |
301+
| ↳ [x] update NLLs for required changes to local & region liveness, loan liveness & loan scopes, (possibly unreachable) kills, bidirectional traversal & active loans | | |
302+
| ↳ [x] limit regressions about diagnostics when using the new constraints on diagnostics tailored to the old constraints | | |
303+
| ↳ [x] land on nightly | | |
304+
| [x] Debugging / dump tool for analysis of location-sensitive analysis | @lqd | |
305+
| Expand prototype into alpha version | @lqd | |
306+
| ↳ [ ] Handle member constraints, and SCCs | | |
307+
| ↳ [ ] Reduce overhead of the analysis | | |
308+
| ↳ [ ] Make the analysis incremental and/or lazy | | |
309+
| Tests and validation | @lqd | in progress |
310+
| ↳ [ ] make the full test suite pass | | in progress, PR [#143093] |
311+
| ↳ [x] do a crater run for assertions and backwards-compatibility | | |
312+
| ↳ [ ] expand test suite with tests about the new capabilities | | in progress, PR [#143093](https://github.com/rust-lang/rust/pull/143093) |
313+
| [ ] Alpha version on nightly, tested on CI | @lqd | |

0 commit comments

Comments
 (0)