Exclusive capabilities #22218

odersky · 2024-12-16T12:47:30Z

A draft PR to implement Capybara-like mutation checking

Linyxus · 2024-12-16T21:03:37Z

odersky · 2024-12-21T23:07:46Z

The earliest European representation of a capybara from "A Relation of a voyage" (1698)

odersky · 2025-01-15T12:06:49Z

I squashed commits and arranged them in a more logical order. Ready for review now.

Linyxus · 2025-01-16T08:12:33Z

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 fail

The problem is with bad: it seems to "mutably borrow" the parameter io but in the body it widens {io} to {cap} (which should only be contextual) and returns it.

To properly handle these things I think it is necessary to support consume (or dropping). So maybe it can be addressed by a future PR.

odersky · 2025-01-16T17:47:48Z

@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

LGTM! Just left some minor comments

bracevac · 2025-01-18T17:48:33Z

compiler/src/dotty/tools/dotc/cc/CaptureOps.scala


+  /** If true, turn on separation checking */
+  def useFresh(using Context): Boolean =


Let it have a more descriptive name? E.g. useSeparationChecking

bracevac · 2025-01-18T18:14:57Z

compiler/src/dotty/tools/dotc/cc/CaptureRef.scala


 /** 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


Is orderL a typo?

bracevac · 2025-01-18T19:05:21Z

compiler/src/dotty/tools/dotc/cc/CaptureSet.scala

@@ -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.


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.

bracevac · 2025-01-18T19:06:17Z

compiler/src/dotty/tools/dotc/cc/CaptureSet.scala

@@ -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.


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.

bracevac · 2025-01-18T19:09:33Z

compiler/src/dotty/tools/dotc/cc/CaptureSet.scala

+      if seen.add(ref) then
+        try pred finally seen -= ref
+      else false
+


Suggested change

end VarState

I leave out the end VarState if the next line is object VarState. That way, we need only one end. IN a sense object VarState is that static part of class VarState.

bracevac · 2025-01-18T19:19:31Z

compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala

+     *  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.


Suggested change

* by the type variable instantiatiin.

* by the type variable instantiation.

bracevac · 2025-01-18T19:49:12Z

compiler/src/dotty/tools/dotc/cc/Fresh.scala

+
+    var reach = false
+
+    private def initHidden =


This appears to be a duplicate of ownerToHidden above. Consolidate?

bracevac · 2025-01-18T20:13:57Z

compiler/src/dotty/tools/dotc/cc/Setup.scala

-    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


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

bracevac · 2025-01-18T20:29:00Z

library/src/scala/annotation/internal/freshCapability.scala

+package internal
+
+/** An annotation used internally for fresh capability wrappers of `cap`
+ */


Show example just as in readOnlyCapability.scala

bracevac · 2025-01-18T20:31:37Z

library/src/scala/caps.scala

@@ -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`.


Do you mean freshCapability? I don't see uniqueCapability anywhere.

Also, the extension this comment is attached is named readOnlyCapability. Is there something missing perhaps?

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.

3.7 is already on us, so bump by one. Two new tests for separation checking. One i15749a required a change in SepCheck: We need to be able to declare reach capabilities in dependencies. The reach is imply dropped. But we can't sometimes use a normal capability since its capture set might be empty.

odersky force-pushed the exclusive-capabilities branch 2 times, most recently from 8cbc022 to 0a73a26 Compare December 21, 2024 14:01

odersky force-pushed the exclusive-capabilities branch from 0da66e2 to eae9c07 Compare December 31, 2024 17:29

odersky force-pushed the exclusive-capabilities branch 2 times, most recently from 498f43d to af23b3f Compare January 15, 2025 12:04

odersky marked this pull request as ready for review January 15, 2025 12:06

odersky mentioned this pull request Jan 15, 2025

Exclusive capabilities V2 #22338

Closed

Linyxus self-requested a review January 16, 2025 07:52

bracevac self-requested a review January 16, 2025 11:53

bracevac approved these changes Jan 18, 2025

View reviewed changes

bracevac approved these changes Jan 19, 2025

View reviewed changes

odersky added 12 commits January 21, 2025 21:23

Elide capabilities implied by Capability subtypes when printing

dadcc54

When printing a type `C^` where `C` extends `Capability`, don't show the `^`. This is overridden under -Yprint-debug.

Drop special handling of functions with pure arguments in Existential…

282d4e2

….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.

Separation checking for applications

7fe68d8

Check separation from source 3.7 on. We currently only check applications, other areas of separation checking are still to be implemented.

Separation checking for blocks

84bb2df

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.

Address review comments

4511a64

Use deep capturesets for separation checking.

87d2a25

When checking whether two items overlap we should always check their deep capture sets. Buried aliases should count as well.

Cache derived reach, readOnly, and maybe capabilities

d8f1423

This is necessary since capability sets are IdentitySets.

Check separation of different parts of a declared type.

f03b5b6

Avoid forming intersections of capture sets on refined type lookup

b114ada

odersky force-pushed the exclusive-capabilities branch from 79f8ef1 to 0b9acb3 Compare January 21, 2025 21:19

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Exclusive capabilities #22218

Exclusive capabilities #22218

odersky commented Dec 16, 2024

Linyxus commented Dec 16, 2024

odersky commented Dec 21, 2024

odersky commented Jan 15, 2025

Linyxus commented Jan 16, 2025 •

edited

Loading

odersky commented Jan 16, 2025

bracevac left a comment

bracevac Jan 18, 2025

bracevac Jan 18, 2025

bracevac Jan 18, 2025

bracevac Jan 18, 2025

bracevac Jan 18, 2025

odersky Jan 19, 2025

bracevac Jan 18, 2025

bracevac Jan 18, 2025

bracevac Jan 18, 2025

bracevac Jan 18, 2025

bracevac Jan 18, 2025

bracevac Jan 18, 2025


		/** If true, turn on separation checking */
		def useFresh(using Context): Boolean =

	* By default, recording is allowed in regular both not in frozen states.
	* By default, recording is allowed in regular but not in frozen states.

	* by the type variable instantiatiin.
	* by the type variable instantiation.

	/** 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

Exclusive capabilities #22218

Are you sure you want to change the base?

Exclusive capabilities #22218

Conversation

odersky commented Dec 16, 2024

Linyxus commented Dec 16, 2024

odersky commented Dec 21, 2024

odersky commented Jan 15, 2025

Linyxus commented Jan 16, 2025 • edited Loading

odersky commented Jan 16, 2025

bracevac left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Linyxus commented Jan 16, 2025 •

edited

Loading