Classifying capabilities

[odersky]

The motivation for this is to come up with a type for Try.apply or Future.apply that reflects the capability structure. Try.apply would have a type like this one:

object Try:
  def apply[T](body: => T): Try[T]^{???}

The ??? should capture all control capabilities of body (such as Labels or CanThrows). After the apply exits, the capabilities owned by body are spent, except for those control capabilities. These are retained in the failure part of a Try since they will be re-thrown when the Try is accessed by a get or a pattern match.

The problem is we are lacking a way to express those control capability slices, nor do we have a way to reason about them (i.e. know which ones subsume which other ones, or which ones can be discarded).

The idea is to add a new kind of capability acting as a filter. If c is a capability, then c.only[C] would stand for all capabilities implied by c that have a type deriving from class C. Specialized to control, we could introduce a new trait

trait Control extends ClassifierCapability

that is a base class of control capability classes such as Label, CanThrow, or Async. With that structure in place, we could give the following signature to Try.apply:

object Try:
  def apply[T](body: => T): Try[T]^{body.only[Control]}

c.only[C] is called a filtered capability. Generally, c.only[C] is a new capability qualifier, alongside c.rd and c*. If multiple qualifiers are given then .only comes after * but before .rd, i.e. c*.only[C].rd would be in the correct order. There can only be a single only-qualifier on a capability.

We now need to develop subsumption rules for filtered-capabilities. We clearly should have

    c.only[C]  <:  c
    c1.only[C1]  <:  c2.only[C2]       if c1 <: c2, C1 <: C2

What about the other combinations? When is c <: c.only[C]? We do want this to hold sometimes. For instance if async: Async where Async derives from Control then it would be nice to be able to conclude that async <: async.only[Control].

Another issue is how to detect disjointness. For instance, a particular operation op might capture a Label lbl and a mutable matrix m.

   op: () ->{lbl, m} Unit

What is the type of Try.apply(op())? Consulting the signature of Try.apply we get

   Try[Unit]^{op.only[Control]}

Replacing op with the actual argument, we get {lbl.only[Control], m.only[Control]} as the capture set of the result. lbl.only[Control] should simplify to lbl by the reasoning we outlined before. m.only[Control] should ideally simplify to nothing, since a mutable matrix would not expected to capture a control capability. So, ideally

Try.apply(op()): Try[Unit]^{lbl}

To get there, we introduce classifier capability classes. These are classes (or traits) that declare ClassifierCapability as a direct parent class. In particular we would have:

trait SharedCapability extends ClassifierCapability
trait Control extends ClassifierCapability, SharedCapability
trait Mutable extends ClassifierCapability

A class can not directly or indirectly extend two unrelated classifier capability classes.

Now, looking at subsumption rules, we first need this one:

     c <: c.only[D]

if D is a classifier capability class and c is classified as D.

Definition
A capability c is classified as a classifier capability class D if the
transitive capture set of c only contains capabilities that derive from D.

Definition The transitive capture set tcs(c) of an object capability c consists of c itself plus the transitive capture sets of all capabilities captured by the type of c. The transitive capture set of a root capability c is just {c}. The transitive
capture set of c.rd is {x.rd | x in tcs(c)}

Definition A capability c derives from a classifier class D if one of the following applies:

• c is an object capability of type T and T <: D (alternatively, T has D in its parent classes),
• c is a root capability cap which originated from a type C^{cap, ...} where C <: D.
• c is a read capability c1.rd and c1 derives from D.
• c is a capture set variable X and all elements in the alias or upper bound of X derive from D.

To make this sound, we have to restrict possible values of FreshCap capabilities. If a FreshCap starts life in the capture set of a class C that extends a classifier class D then the FreshCap instance can subsume only capabilities classified as D. So FreshCap instances now carry restrictions for disjointness (in separation checking), levels, as well as classifiers.

Example

   lbl <: lbl.only[Control]

because the tcs(lbl) = {lbl, cap} where the cap is a root capability associated with Label which is a subclass of the classifier class Control.

Furthermore, we have

   {c.only[D]} <: {}

if D is a classifier capability class and tcs(c) only contains capabilities that derive from classifier class unrelated to C.

So

   {m.only[Control]} <: {}

because m is classified as Mutable, which is unrelated to Control.

[odersky]

What this mans for the implementation

• Syntax and parsing rules for only-capabilities.
• A ClassifiedCapability base trait.
• Enforce restriction that a class cannot inherit two unrelated capability classes.
• A new capability class for only-capabilities.
• Implement captureSetOfInfo for only capabilities.
• The empty capability is x.only[Nothing]. It should have empty captureSetOfInfo.
• Well-formedness rules: only must refer to a classified capability class or to Nothing.
• Normalization rules:
  - it's *, then .only, then .rd,
  - multiple .only normalize to the smallest one if the classes are related,
  - multiple .only normalize to the empty capability if the classes are not related.
• define transitive capture set and cache it in a capability. The tcs does not exist if a capture set in the hierarchy is still an unsolved capture set variable.
• Add a classifier field to FreshCap and ResultCap.
• Modify capToFresh and toResultInResults so that the classifier field is correctly set.
• Using tcs, define when a capability is classified as a classifier class.
• A FreshCap with a classifier C can subsume only capabilities that are classified as C.
• Implement subsumption rules:
  - c.as[C] <: d if c <: d or c.as[D] <: empty
  - c.as[C] <: d.as[D] if c <: d and C derives from D
  - c <: d.as[D] if c <: d and c is classified as D
  - c.as[D] <: empty if tcs(c) consists of capabilities that all derive from classifier classes unrelated to D.

[odersky]

WIP PR is #23485

[odersky]

This looks like a lot of machinery to typecheck Try and Future. I there a simpler way? I have not found one yet. Can we ignore the problem? Then it seems we have to type Try(body) as T^{body}, which would ruin separation checking because then we cannot tell that body no longer can change anything because it has executed.

[odersky]

One possible generalization would be to have besides .as[C] also .asNot[C], or, with a different syntax: .as[!C]. This could be useful for instance to characterize the use set of a Try(body). It would be body.as[!Control] since all control capabilities have been caught by the Try.

[odersky]

One possible simplification is to specialize the treatment to control capabilites:

• Instead of @classifier traits have just two subtraits of Capability: Control and NonControl.
• Instead of c.as[C], have c.ctrl and c.nonctrl.
• Specialize the remaining rules accordingly.

This would make sense if we can convince ourselves that the only capability masking operations we envision mask specifically control capabilities. Can we?

[odersky]

One observation: .as can also be used to implement a new kind of capture set constraint:

  [C <: {cap.as[Mutable]}]    // all elements of the set must be transitively `Mutable`.
  [C <: {cap.as[Sharable]}    // all elements of the set must be transitively `Sharable`.
  [C <: {cap.as[Control]}     // all elements of the set must be transitively `Control` capabilties.

[odersky]

And it is convenient to restrict capabilities of function types. For instance, when doing separation checking we might want to accept only functions over sharable capabilities. This can now be expressed:

A ->{cap.as[Sharable]} B

We could probably make this nicer by defining capture set aliases:

type sharable^ = {cap.as[Sharable]}

A ->{sharable} B

@bracevac Do you think this would work?

Overall I am coming to believe that this is a fundamental addition to capture checking that solves multiple expressiveness problems we had so far. So I tend to think we should do a trial implementation.

[odersky]

Maybe we need a more expressive language for what can go into an .as[...]. I mentioned already complement. We could also allow unions. Maybe we could write .as[Mutable, IOCapability], or .except[Control, Mutable]

[bracevac]

This is a mechanism that enables limiting what can be closed over up to a certain threshold, which is very useful.

Without it, the next best thing one could do in the current system is using some form of branding through a variable in context (like we tried with the sub-regions example), but it's quite awkward and I don't think it scales well.

Classifiers seem to be less ad hoc, and it'd be good if we allowed users to extend the classifier hierarchy. I think classifiers subsume the advanced use cases from the 2nd-class values works. With finer-grained closure up to, we can emulate, e.g., Fig. 7 in the paper I linked:

@classifier trait Read extends Capability
@classifier trait ReadWrite extends Capability

trait File extends Capability:
  type R  <: Read
  type RW <: ReadWrite
  given r: R
  given rw: RW
  // operations guarded by capability members
  def read(using this.R): Byte
  def write(using this.RW)(b: Byte): Unit
   

def withFile[U](block: File^ => U): U // unrestricted use of files & other capabilities
def parReduce[U](xs: Seq[U])(op: U ->{cap.only[Read]} U): U // only Read-classified allowed

withFile("foo.txt"): f =>
  parReduce(1 to 1000): (a, b) =>
    f.write(a) // error ReadWrite is excluded
    a + b + f.read() // ok
  f.write(0x42) // ok access unrestricted

We can understand the proposed forms in terms of set operations involving transitive capture closure, only being some kind of intersection (is there a connection to separation checking?),
and except as some kind of set difference, or intersection with a complement.

However, the .except form, as discussed offline, needs to be carefully restricted, especially if we permit user-defined extensions of the classifier hierarchy and separate compilation:

E.g.,

// File1.scala:
// Here, the universe of classifiers consists of the standard ones: Shareable, Mutable, Control
def mkPure(f: () ->{cap.except[Shareable,Mutable,Control] Unit): () ->{} Unit = 
  f // everything except all the known classifiers means nothing, so we are "pure"

can be subverted if we extend the classifiers elsewhere:

// File2.scala
@classifier Sneaky extends Capability
val s: Sneaky = ...

val fakePure: () -> Unit = 
  File1.mkPure(() => s.boom()) // ok!, since {s}.except[Shareable,Mutable,Control] = {s}