Exclusive capabilities #22218
Merged
Exclusive capabilities #22218
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
|
odersky
force-pushed
the
exclusive-capabilities
branch
2 times, most recently
from
8cbc022 to
0a73a26
Compare
|
The earliest European representation of a capybara from "A Relation of a voyage" (1698)
|
odersky
force-pushed
the
exclusive-capabilities
branch
from
0da66e2 to
eae9c07
Compare
odersky
force-pushed
the
exclusive-capabilities
branch
2 times, most recently
from
498f43d to
af23b3f
Compare
|
I squashed commits and arranged them in a more logical order. Ready for review now. |
|
A soundness hole: import caps.cap
import language.future
import language.experimental.captureChecking
def par(op1: () => Unit)(op2: () => Unit): Unit = ()
def bad(io: Object^): () => Unit =
val x: () => Unit = () => println(io)
x
def test(io: Object^): Unit =
par(() => println(io))(() => println(io)) // error // (1)
val f = bad(io)
par(f)(() => println(io)) // no error, but it is equivalent to (1) and should failThe problem is with To properly handle these things I think it is necessary to support |
|
@Linyxus This is still a work in progress. Separation checking for parameters and returns is not yet implemented. But we'll get back to the test case once it lands. |
bracevac
approved these changes
Jan 18, 2025
|
|
||
| /** If true, turn on separation checking */ | ||
| def useFresh(using Context): Boolean = |
There was a problem hiding this comment.
Let it have a more descriptive name? E.g. useSeparationChecking
|
|
||
| /** A trait for references in CaptureSets. These can be NamedTypes, ThisTypes or ParamRefs, | ||
| * as well as two kinds of AnnotatedTypes representing reach and maybe capabilities. | ||
| * as well as three kinds of AnnotatedTypes representing readOnly, reach, and maybe capabilities. | ||
| * If there are several annotations they come with an orderL |
| @@ -976,8 +1051,7 @@ object CaptureSet: | |||
| def getElems(v: Var): Option[Refs] = elemsMap.get(v) | |||
|
|
|||
| /** Record elements, return whether this was allowed. | |||
| * By default, recording is allowed but the special state FrozenState | |||
| * overrides this. | |||
| * By default, recording is allowed in regular both not in frozen states. | |||
There was a problem hiding this comment.
Suggested change
| * By default, recording is allowed in regular both not in frozen states. | |
| * By default, recording is allowed in regular but not in frozen states. |
| @@ -988,58 +1062,104 @@ object CaptureSet: | |||
| def getDeps(v: Var): Option[Deps] = depsMap.get(v) | |||
|
|
|||
| /** Record dependent sets, return whether this was allowed. | |||
| * By default, recording is allowed but the special state FrozenState | |||
| * overrides this. | |||
| * By default, recording is allowed in regular both not in frozen states. | |||
There was a problem hiding this comment.
Suggested change
| * By default, recording is allowed in regular both not in frozen states. | |
| * By default, recording is allowed in regular but not in frozen states. |
| * The unboxed condition ensures that the expected is not a type variable | ||
| * that's upper bounded by a read-only type. In this case it would not be sound | ||
| * to narrow to the read-only set, since that set can be propagated | ||
| * by the type variable instantiatiin. |
There was a problem hiding this comment.
Suggested change
| * by the type variable instantiatiin. | |
| * by the type variable instantiation. |
|
|
||
| var reach = false | ||
|
|
||
| private def initHidden = |
There was a problem hiding this comment.
This appears to be a duplicate of ownerToHidden above. Consolidate?
| private def transformTT(tree: TypeTree, boxed: Boolean)(using Context): Unit = | ||
| private val paramSigChange = util.EqHashSet[Tree]() | ||
|
|
||
| /** Transform type of tree, and remember the transformed type as the type the tree |
There was a problem hiding this comment.
Suggested change
| /** Transform type of tree, and remember the transformed type as the type the tree | |
| /** Transform type of tree, and remember the transformed type as the type of the tree |
library/src/scala/caps.scala
Outdated
| @@ -41,6 +43,12 @@ import annotation.{experimental, compileTimeOnly, retainsCap} | |||
| */ | |||
| extension (x: Any) def reachCapability: Any = x | |||
|
|
|||
| /** Unique capabilities x! which appear as terms in @retains annotations are encoded | |||
| * as `caps.uniqueCapability(x)`. When converted to CaptureRef types in capture sets | |||
| * they are represented as `x.type @annotation.internal.uniqueCapability`. | |||
There was a problem hiding this comment.
Do you mean freshCapability? I don't see uniqueCapability anywhere.
There was a problem hiding this comment.
Also, the extension this comment is attached is named readOnlyCapability. Is there something missing perhaps?
bracevac
approved these changes
Jan 19, 2025
odersky
force-pushed
the
exclusive-capabilities
branch
2 times, most recently
from
718e03d to
ab4d96a
Compare
When printing a type `C^` where `C` extends `Capability`, don't show the `^`. This is overridden under -Yprint-debug.
- 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.
Downgrade to -source 3.6 to turn it off.
Allow them only in @consume methods
Also: Fixes to computations of overlapWith and -- on Refs that take account of pathss, where shorter paths cover deeper ones.
odersky
force-pushed
the
exclusive-capabilities
branch
from
5ed779c to
65a1301
Compare
|
@bracevac Ready for review. I still want to document Fresh.scala and SepChecks.scala better, but otherwise all my changes are done for now. |
odersky
force-pushed
the
exclusive-capabilities
branch
from
f3c59cc to
813c585
Compare
bracevac
approved these changes
Feb 4, 2025
| case _ => | ||
| ReadOnlyCapability(tp) | ||
|
|
||
| /** If `x` is a capture ref, replacxe all no-flip covariant occurrences of `cap` |
There was a problem hiding this comment.
Suggested change
| /** If `x` is a capture ref, replacxe all no-flip covariant occurrences of `cap` | |
| /** If `x` is a capture ref, replace all no-flip covariant occurrences of `cap` |
| protected def unwrappable(using Context) = Set() | ||
|
|
||
| /** An extractor for `ref @readOnlyCapability`, which is used to express | ||
| * the rad-only capability `ref.rd` as a type. |
There was a problem hiding this comment.
Suggested change
| * the rad-only capability `ref.rd` as a type. | |
| * the read-only capability `ref.rd` as a type. |
| case _ => false | ||
|
|
||
| /** An exclusive capability is a capability that derives | ||
| * indirectly from a maximal capability without goinh through |
There was a problem hiding this comment.
Suggested change
| * indirectly from a maximal capability without goinh through | |
| * indirectly from a maximal capability without going through |
| */ | ||
| final def isExclusive(using Context): Boolean = | ||
| !isReadOnly && (isMaxCapability || captureSetOfInfo.isExclusive) | ||
|
|
||
| // With the support of pathes, we don't need to normalize the `TermRef`s anymore. |
There was a problem hiding this comment.
Suggested change
| // With the support of pathes, we don't need to normalize the `TermRef`s anymore. | |
| // With the support of paths, we don't need to normalize the `TermRef`s anymore. |
| @@ -180,6 +242,53 @@ trait CaptureRef extends TypeProxy, ValueType: | |||
| case _ => false | |||
| end subsumes | |||
|
|
|||
| /** This is a maximal capabaility that subsumes `y` in given context and VarState. | |||
There was a problem hiding this comment.
Suggested change
| /** This is a maximal capabaility that subsumes `y` in given context and VarState. | |
| /** This is a maximal capability that subsumes `y` in given context and VarState. |
| @@ -364,7 +407,7 @@ object CaptureSet: | |||
| /** If set to `true`, capture stack traces that tell us where sets are created */ | |||
| private final val debugSets = false | |||
|
|
|||
| private val emptySet = SimpleIdentitySet.empty | |||
| val emptySet = SimpleIdentitySet.empty | |||
There was a problem hiding this comment.
Might be misleading/confused compared to val empty below. Does this really have to be in object CaptureSet?
There was a problem hiding this comment.
It's convenient to have it in SepCheck also. I renamed to emptyRefs and pinned the type to Refs.
| extends Var(initialElems = initialHidden): | ||
|
|
||
| /** Apply function `f` to `elems` while setting `elems` to empty for the | ||
| * duration. This is used to escape infinite recursions if two Frash.Caps |
There was a problem hiding this comment.
Suggested change
| * duration. This is used to escape infinite recursions if two Frash.Caps | |
| * duration. This is used to escape infinite recursions if two Fresh.Caps |
| /** The current VarState, as passed by the implicit context */ | ||
| def varState(using state: VarState): VarState = state | ||
|
|
||
| /** Maps `x` to `x?` */ | ||
| private class MaybeMap(using Context) extends BiTypeMap: | ||
| /** A template for maps on capabilities where f(c) <: c and f(f(c)) = c */ |
There was a problem hiding this comment.
Should this not be an IdempotentCaptRefMap as well then?
There was a problem hiding this comment.
It's always one or the other. BiTypeMaps are better for type inference.
| @@ -573,6 +621,15 @@ class CheckCaptures extends Recheck, SymTransformer: | |||
| } | |||
| case _ => denot | |||
|
|
|||
| // Don't allow update methods to be called unless the qualifier captures | |||
| // contain an exclusive referenece. TODO This should probabkly rolled into | |||
There was a problem hiding this comment.
Suggested change
| // contain an exclusive referenece. TODO This should probabkly rolled into | |
| // contains an exclusive referenec. TODO This should probably be rolled into |
| @@ -573,6 +621,15 @@ class CheckCaptures extends Recheck, SymTransformer: | |||
| } | |||
| case _ => denot | |||
|
|
|||
| // Don't allow update methods to be called unless the qualifier captures | |||
There was a problem hiding this comment.
Suggested change
| // Don't allow update methods to be called unless the qualifier captures | |
| // Don't allow update methods to be called unless the qualifier |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
implement capybara-like mutation checking
x.rdMutableandSharedCapabilityas subclasses ofCapability.Mutabletypes - exclusive if they can invoke an update method, read-only otherwise.Fresh.Capas a family of new top-types that keep track of references that were widened to themFresh.Capdon't appear as aliases@consume@consume.To be done in a separate PR: Add qualifiers to capture sets so that we can talk of the read-only part of a
Mutabletype.