RFC: Single-entry / multiple-exit regions for borrows

[zwarich]

Rendered

[zwarich]

cc @nikomatsakis @pcwalton @pnkfelix

[lilyball]

This sounds tautological. "If [...] P is a path [...] that does not leave R [...], then every vertex of P is in R". Surely the condition "P is a path [...] that does not leave R" is identical to "P is a path where every vertex of P is in R", which makes this "If P is a path where every vertex of P is in R, then every vertex of P is in R".

[zwarich]

I first came up with the more technical definition below and then tried to make a plain English counterpart.

What I was attempting to capture was the part about reentering through Entry. For example, in a program fragment like

loop {
    [Entry]
    [Exit]
}

there is allowed to be a path from Entry to Exit, back around the outer loop that reenters Entry, without all of the vertices on that path being in the region. On second thought, it seems that this would be fine:

If V is in R and P is a path from Entry to V that does not contain Entry multiple times, then every vertex of P is in R.

[lilyball]

The idea of counting uses of Entry seems a little odd. Could you not use something like the following:

For every pair of vertices V and U in R, every path from V to U that contains vertices not in R also contains Entry.

[zwarich]

That seems equivalent and a bit simpler, so I'll go with that.

[lilyball]

Or the more general definition, which subsumes the first condition:

For all vertices V in R, for all vertices U not in R, every path from U to V contains Entry.

Instead of evaluating paths only from the CFG entry to V, evaluating from all nodes not in R allows you to avoid doing any counting.

[steveklabnik]

You shouldn't need indentation AND fences, just use fences.

[zwarich]

@steveklabnik You didn't leave a line comment, but if you're referring to what I think you're referring to then it was necessary to use both indentation and fences in order to keep the code block indented to the same level as the rest of the list item.

[lilyball]

On that note, line 29 is indented by a single space, which is a little confusing. It does seem to result in a paragraph within the list item, but it does make the following code block at line 33 appear to be incorrectly indented. Other paragraphs in these list items are also similarly indented by a single space. They should probably be indented by a standard amount; either 4 spaces, if that's truly necessary for the code block, or 3 spaces if that works, to line up with the first paragraph in the list item.

[zwarich]

@kballard As far as I can tell, the output looks correct, so I'm not really inclined to be overly pedantic regarding Markdown formatting when Markdown is so ill-defined to begin with.

[gulbanana]

Excellent idea, this extends checkability to some major cases with a sound foundation. I've got a few questions & will try to figure out how to do the line-comments thing

[gulbanana]

it's unclear to me what this fragment is demonstrating. q is an immutable binding, so it has to be initialised once-and-only-once subsequently, right? is the idea that MEME would allow the q= lines in each branch to borrowcheck because they're each an entry to the same region (and each of the drop(p) is an exit from the previous region?)

[zwarich]

Yes, that's the scenario I'm describing. It is initialized in two different program locations, but only once on every path through the program.

[gulbanana]

ok, that makes sense

[Ericson2314]

I imagine this would impact the static/dynamic drop debate?

[tikue]

Any status on this? Because this affects a lot of common code and could have a great impact on how beginners of Rust perceive the language, it seems prudent to introduce any required backwards-incompatible changes before 1.0.

[zwarich]

@Ericson2314 This shouldn't impact the static / dynamic drop debate. It will allow more moves due to borrow scopes being more precise, however.

@tikue I am no longer involved in Rust development, but it is my understanding that this is not going to happen for 1.0. To me it seems that the evaluation order issue is backwards incompatible, but @nikomatsakis has mentioned that he thinks he has a way to resolve this; I don't know what it is, but it might be along the lines of what @eddyb discusses above.

[pnkfelix]

We'd love to have this, but we do not think we can spend time working on it before the release.

Postponing