WG-Polonius meeting minutes 2019.06.11

WG-Polonius meeting minutes: 2019/06/11

Relevant links:

This week, we worked on — and discussed — the following topics:

1. Proposal: stop tracking subset relations along the CFG

Niko wrote up an issue with more details about the proposal: issue #107. We also discussed it more in the dedicated zulip thread, around this point.

We made an example where the new refinement would improve on Polonius' behaviour: it currently flags an unnecessary error on this example.

Niko later realized that the refinement as proposed could also be less precise than current Polonius (which accepts the example in the comment), and which could require making the equality-tracking flow-sensitive.

Some more exploratory work is planned around these refinements, and also around their interaction with other topics: for example “illegal subset relation errors” would likely need an approach similar to the “placeholder loans” we discussed around here, and prior to that, here.

To prepare for the call on this topic, Rémy tried implementing a quick prototype and examples. As of this writing, it seems to work on the simpler example datasets from the Polonius repository, but not on the more realisic use-case (clap) so more bugfixing will be needed. Rémy also wrote a short report about those quick explorations.

2. Call about subset relations, the proposal, Oxide

We had a recorded video call about the specifics of the subset relation, its role and why it was propagated along the CFG. We then talked in more detail about the proposal refinement(s), and finished with a comparison between the Polonius model and the Oxide model.

To follow along the video: the paper document we used to record notes and examples can be found here.

Huge thanks to everyone involved, it was super interesting and fun!

3. Profiling and performance

@lokalmatador has been successfully gathering early results :tada: (for example, this profiling data comes from some of examples in the Polonius repository). The next steps will then be to collect some data from the official rustc benchmarking suite.

4. Rustc test failures under Polonius

Rémy has (slowly) continued work on analyzing the ui test suite failures under Polonius. Now that Matthew’s PR #60171 has landed: the WIP branch was rebased into a more stable state.

New failures were unfortunately found, but most of the simpler differences were “taken care of”. The analysis will need to be double-checked, and the WIP report is here.

There are still a couple of simple cases left (differences in diagnostics only, for example) before looking at the remaining more complicated cases, but those seem to be actual “regressions” somewhere (probably divergences between the Polonius facts, NLL constraints, and assumptions about MIR).

5. Liveness

:tada: polonius#105 has landed :tada:

Now, to get the rustc changes landed, we were still wondering about the differences between the region_live_at facts computed by rustc, and the ones computed by Polonius. The liveness computation in rustc is taking initialization into account, while rustc PR #60266 only slightly (which is expected as move/initialization analysis is the next item Albin plans to tackle).

Niko and Albin discussed (around here) a way to remove the computation of the region_live_at relation without losing precision, as both a safety measure and an intermediary step towards handling moves/initialization.

With Niko being away at Mozilla All Hands next week, we mentioned that we might do short async updates instead of a sync meeting, but the plan was overall:

  • @lokalmatador will continue gathering profiling data.
  • Albin will look at the potential region_live_at intermediary step we mentioned.
  • Rémy will continue on the rustc test suite analysis, and the proposal prototype.