Skip to content

Commit c865598

Browse files
committed
Update language reference
Splits the more advanced cc examples into its own hidden page.
1 parent 4a40cd7 commit c865598

File tree

3 files changed

+82
-65
lines changed

3 files changed

+82
-65
lines changed
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,78 @@
1+
---
2+
layout: doc-page
3+
title: "Capture Checking -- Advanced Use Cases"
4+
nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/cc-advanced.html
5+
---
6+
7+
8+
## Access Control
9+
Analogously to type parameters, we can lower- and upper-bound capability parameters where the bounds consist of concrete capture sets:
10+
```scala
11+
def main() =
12+
// We can close over anything branded by the 'trusted' capability, but nothing else
13+
def runSecure[C^ >: {trusted} <: {trusted}](block: () ->{C} Unit): Unit = ...
14+
15+
// This is a 'brand" capability to mark what can be mentioned in trusted code
16+
object trusted extends caps.Capability
17+
18+
// These capabilities are trusted:
19+
val trustedLogger: Logger^{trusted}
20+
val trustedChannel: Channel[String]^{trusted}
21+
// These aren't:
22+
val untrustedLogger: Logger^
23+
val untrustedChannel: Channel[String]^
24+
25+
runSecure: () =>
26+
trustedLogger.log("Hello from trusted code") // ok
27+
28+
runSecure: () =>
29+
trustedChannel.send("I can send") // ok
30+
trustedLogger.log(trustedChannel.recv()) // ok
31+
32+
runSecure: () => "I am pure and that's ok" // ok
33+
34+
runSecure: () =>
35+
untrustedLogger.log("I can't be used") // error
36+
untrustedChannel.send("I can't be used") // error
37+
```
38+
The idea is that every capability derived from the marker capability `trusted` (and only those) are eligible to be used in the `block` closure
39+
passed to `runSecure`. We can enforce this by an explicit capability parameter `C` constraining the possible captures of `block` to the interval `>: {trusted} <: {trusted}`.
40+
41+
Note that since capabilities of function types are covariant, we could have equivalently specified `runSecure`'s signature using implicit capture polymorphism to achieve the same behavior:
42+
```scala
43+
def runSecure(block: () ->{trusted} Unit): Unit
44+
```
45+
46+
## Capture-safe Lexical Control
47+
48+
Capability members and paths to these members can prevent leakage
49+
of labels for lexically-delimited control operators:
50+
```scala
51+
trait Label extends Capability:
52+
type Fv^ // the capability set occurring freely in the `block` passed to `boundary` below.
53+
54+
def boundary[T, C^](block: Label{type Fv = {C} } ->{C} T): T = ??? // ensure free caps of label and block match
55+
def suspend[U](label: Label)[D^ <: {label.Fv}](handler: () ->{D} U): U = ??? // may only capture the free capabilities of label
56+
57+
def test =
58+
val x = 1
59+
boundary: outer =>
60+
val y = 2
61+
boundary: inner =>
62+
val z = 3
63+
val w = suspend(outer) {() => z} // ok
64+
val v = suspend(inner) {() => y} // ok
65+
val u = suspend(inner): () =>
66+
suspend(outer) {() => w + v} // ok
67+
y
68+
suspend(outer): () =>
69+
println(inner) // error (would leak the inner label)
70+
x + y + z
71+
```
72+
A key property is that `suspend` (think `shift` from delimited continuations) targeting a specific label (such as `outer`) should not accidentally close over labels from a nested `boundary` (such as `inner`), because they would escape their defining scope this way.
73+
By leveraging capability polymorphism, capability members, and path-dependent capabilities, we can prevent such leaks from occurring at compile time:
74+
75+
* `Label`s store the free capabilities `C` of the `block` passed to `boundary` in their capability member `Fv`.
76+
* When suspending on a given label, the suspension handler can capture at most the capabilities that occur freely at the `boundary` that introduced the label. That prevents mentioning nested bound labels.
77+
78+
[Back to Capture Checking](cc.md)

docs/_docs/reference/experimental/cc.md

+2-65
Original file line numberDiff line numberDiff line change
@@ -784,42 +784,6 @@ In such a scenario, we also should ensure that any pre-existing alias of a `Conc
784784
inaccessible after invoking its `concat` method. This is achieved with mutation and separation tracking which are
785785
currently in development.
786786

787-
Finally, analogously to type parameters, we can lower- and upper-bound capability parameters where the bounds consist of concrete capture sets:
788-
```scala
789-
def main() =
790-
// We can close over anything branded by the 'trusted' capability, but nothing else
791-
def runSecure[C^ >: {trusted} <: {trusted}](block: () ->{C} Unit): Unit = ...
792-
793-
// This is a 'brand" capability to mark what can be mentioned in trusted code
794-
object trusted extends caps.Capability
795-
796-
// These capabilities are trusted:
797-
val trustedLogger: Logger^{trusted}
798-
val trustedChannel: Channel[String]^{trusted}
799-
// These aren't:
800-
val untrustedLogger: Logger^
801-
val untrustedChannel: Channel[String]^
802-
803-
runSecure: () =>
804-
trustedLogger.log("Hello from trusted code") // ok
805-
806-
runSecure: () =>
807-
trustedChannel.send("I can send") // ok
808-
trustedLogger.log(trustedChannel.recv()) // ok
809-
810-
runSecure: () => "I am pure and that's ok" // ok
811-
812-
runSecure: () =>
813-
untrustedLogger.log("I can't be used") // error
814-
untrustedChannel.send("I can't be used") // error
815-
```
816-
The idea is that every capability derived from the marker capability `trusted` (and only those) are eligible to be used in the `block` closure
817-
passed to `runSecure`. We can enforce this by an explicit capability parameter `C` constraining the possible captures of `block` to the interval `>: {trusted} <: {trusted}`.
818-
819-
Note that since capabilities of function types are covariant, we could have equivalently specified `runSecure`'s signature using implicit capture polymorphism to achieve the same behavior:
820-
```scala
821-
def runSecure(block: () ->{trusted} Unit): Unit
822-
```
823787

824788
## Capability Members
825789

@@ -844,35 +808,8 @@ trait GPUThread extends Thread:
844808
Since `caps.cap` is the top element for subcapturing, we could have also left out the
845809
upper bound: `type Cap^ >: {cudaMalloc, cudaFree}`.
846810

847-
We conclude with a more advanced example, showing how capability members and paths to these members can prevent leakage
848-
of labels for lexically-delimited control operators:
849-
```scala
850-
trait Label extends Capability:
851-
type Fv^ // the capability set occurring freely in the `block` passed to `boundary` below.
852-
853-
def boundary[T, C^](block: Label{type Fv = {C} } ->{C} T): T = ??? // ensure free caps of label and block match
854-
def suspend[U](label: Label)[D^ <: {label.Fv}](handler: () ->{D} U): U = ??? // may only capture the free capabilities of label
855-
856-
def test =
857-
val x = 1
858-
boundary: outer =>
859-
val y = 2
860-
boundary: inner =>
861-
val z = 3
862-
val w = suspend(outer) {() => z} // ok
863-
val v = suspend(inner) {() => y} // ok
864-
val u = suspend(inner): () =>
865-
suspend(outer) {() => w + v} // ok
866-
y
867-
suspend(outer): () =>
868-
println(inner) // error (would leak the inner label)
869-
x + y + z
870-
```
871-
A key property is that `suspend` (think `shift` from delimited continuations) targeting a specific label (such as `outer`) should not accidentally close over labels from a nested `boundary` (such as `inner`), because they would escape their defining scope this way.
872-
By leveraging capability polymorphism, capability members, and path-dependent capabilities, we can prevent such leaks from occurring at compile time:
873-
874-
* `Label`s store the free capabilities `C` of the `block` passed to `boundary` in their capability member `Fv`.
875-
* When suspending on a given label, the suspension handler can capture at most the capabilities that occur freely at the `boundary` that introduced the label. That prevents mentioning nested bound labels.
811+
812+
[More Advanced Use Cases](cc-advanced.md)
876813

877814
## Compilation Options
878815

docs/sidebar.yml

+2
Original file line numberDiff line numberDiff line change
@@ -162,6 +162,8 @@ subsection:
162162
- page: reference/experimental/main-annotation.md
163163
- page: reference/experimental/into-modifier.md
164164
- page: reference/experimental/cc.md
165+
- page: reference/experimental/cc-advanced.md
166+
hidden: true
165167
- page: reference/experimental/purefuns.md
166168
- page: reference/experimental/tupled-function.md
167169
- page: reference/experimental/modularity.md

0 commit comments

Comments
 (0)