Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Exclusive Capabilities #22577

Draft
wants to merge 23 commits into
base: main
Choose a base branch
from

Conversation

hamzaremmal
Copy link
Member

No description provided.

 - Add Mutable trait and mut modifier.
 - Add dedicated tests `isMutableVar` and `isMutableVarOrAccessor`
   so that update methods can share the same flag `Mutable` with mutable vars.
 - Disallow update methods overriding normal methods
 - Disallow update methods which are not members of classes extending Mutable
 - Add design document from papers repo to docs/internals
 - Add readOnly capabilities
 - Implement raeadOnly access
 - Check that update methods are only called on references with exclusive capture sets.
 - Use cap.rd as default capture set of Capability subtypes
 - Make Mutable a Capability, this means Mutable class references get {cap.rd} as
   default capture set.
 - Use {cap} as captu
….toCap

If existentials are mapped to fresh, it matters where they are opened. Pure or not
arguments don't have anything to do with that.
These are represented as Fresh.Cap(hidden) where hidden is the set of
capabilities subsumed by a fresh. The underlying representation is as
an annotated type `T @annotation.internal.freshCapability`.

Require -source `3.7` for caps to be converted to Fresh.Cap

Also:

 - Refacture and document CaputureSet
 - Make SimpleIdentitySets showable
 - Refactor VarState
    - Drop Frozen enum
    - Make VarState subclasses inner classes of companion object
    - Rename them
    - Give implicit parameter VarState of subCapture method a default value
 - Fix printing of capturesets containing cap and some other capability
 - Revise handing of @uncheckedAnnotation
Check separation from source 3.7 on.

We currently only check applications, other areas of separation checking
are still to be implemented.
Check that a capability that gets hidden in the (result-)type of some
definition is not used afterwards in the same or a nested scope.
When checking whether two items overlap we should always check their deep capture sets.
Buried aliases should count as well.
This is necessary since capability sets are IdentitySets.
TODO:

 - check that only @consume parameters flow to @consume parameters
Downgrade to -source 3.6 to turn it off.
Also: Fixes to computations of overlapWith and -- on Refs that take
account of pathss, where shorter paths cover deeper ones.
Use a coarser prediction of hidden sets. Any Fresh.Cap instance
in a  capture set means that we should do the hidden check. Previously
this was the case only if the Fresh.Cap instance hid something non maximal,
element, but only directly, not via another Cap. Another version searched for
non-maximal references deeply, but this one caused infinite looping in the CI.
But in any case it's fine to over-approximate and assume that any Fresh.Cap
hides something.
@hamzaremmal hamzaremmal self-assigned this Feb 10, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants