Open
Description
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.