Skip to content

Stacked Borrows: Disabled has more effects than expected #274

Open
@RalfJung

Description

@RalfJung

Under some conditions, Stacked Borrows replaces Unique items by Disabled items -- see the docs or the paper for details. This was supposed to just emulate an "idealized" Stacked Borrows where we have sets of tags in an SharedRW item:

Real Stacked Borrows representation:

item := Unique(tg : tag) | SharedRO(tg : tag) | SharedRW(tg : tag) | Disabled
stack := list item

Idealized Stacked Borrows representation:

item := Unique(tg : tag) | SharedRO(tgs : gset tag) | SharedRW(tgs : gset tag)
stack := list item

However, as @ocecaco noticed (I hope this is the right GitHub handle^^), Disabled actually does not make real Stacked Borrows behave like idealized Stacked Borrows. The following two stacks are distinct in real Stacked Borrows, but
not in idealized Stacked Borrows:

..., Unique(0), Disabled, SharedRW(1)
..., Unique(0), SharedRW(1)

A SharedRW reborrow from the Unique(0) will create a new SharedRW group in
the first stack, but extend the existing group in the second stack.

Metadata

Metadata

Assignees

No one assigned

    Labels

    A-aliasing-modelTopic: Related to the aliasing model (e.g. Stacked/Tree Borrows)

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions