WG-Polonius meeting minutes 2019.05.28

WG-Polonius meeting minutes: 2019/05/28


Relevant links:


This week, we discussed the following topics:

1. Profiling and fact generation

@lokalmatador has made some progress on the profiling tasks: WIP branch is here gathering timing data for parts of NLLs and Polonius using rustc’s -Z self-profile API.

The granularity of profiling was discussed, especially regarding fact generation and the separation between NLLs and Polonius. While fact generation would be useful to measure globally, as part of this process is somewhat shared between existing NLL solver uses and Polonius fact generation, separating the two wouldn’t be easy. We clarified that separating fact generation as a distinct timing “activity” would be sufficient, without needing to also isolate between NLLs and Polonius constraints/facts generation.

It was also deemed “nice to have” but not high priority compared to the rest of the profiling information. A list of “ideal” data was described, broken down by function/test (and possibly correlating it with the size of the input facts): - overall MIR borrowck time - fact generation - polonius execution

A bug in measureme’s summarize tool seemed to be blocking progress, but was later found to be a problem in data gathering, and which has since been fixed. Complete discussion available in the dedicated Zulip thread around this point.

2. Liveness

Albin has been putting the finishing touches on the liveness work, which is ready to review and land.

The Polonius liveness PR #105 was updated to bump versions, so that rustc’s liveness PR #60266 can use the appropriate polonius-engine version supporting the new liveness Atoms and relations.

In order to help visualization and debugging, Albin has also continued working on graphviz output for liveness. More details, and screenshots of the example outputs, are available in the dedicated Zulip thread around this point.

Most of the tasks mentioned in a previous meeting, and this summary github comment have been completed.

A summary of the liveness work is “it works but does not produce exactly the same region_live_at facts as rustc does today” (and this is also one of the last tasks in the list). This is because rustc also takes initialization into account, while the Polonius liveness work does not do so yet. This is indeed the next step in Polonius’ roadmap, and a nice segue into the last topic discussed in this meeting.

3. Move/overwrite analysis

As this is the next item to tackle, Niko and Albin will schedule a recorded video chat session next week, about how the current borrow checker tracks moves and initialization, and how to move this over to Polonius.