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.as[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

@classifier trait Control extends Capability

that is a base class of control capability classes such as Label, CanThrow, or Async. (The @classifier
annotation can be ignored for now, it will be further explained below). With that structure in place, we could give the following signature to Try.apply:

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

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

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

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

What about the other combinations? When is c <: c.as[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.as[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.as[Control]}

Replacing op with the actual argument, we get {lbl.as[Control], m.as[Control]} as the capture set of the result. lbl.as[Control] should simplify to lbl by the reasoning we outlined before. m.as[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 subclasses of capability with the added annotation @classifier. In particular we would have:

@classifier trait SharedCapability extends Capability
@classifier trait Control extends SharedCapability
@classfiier trait Mutable extends Capability

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.as[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.as[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.as[D]} <: {}

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

So

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

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

[odersky]

What this mans for the implementation

• Ayntax and parsing rules for as-capabilities.
• A caps.classified annotation.
• Enforce restriction that a class cannot inherit two unrelated capability classes.
• A new capability class for as-capabilities.
• A new capability value for empty capabilities with an empty captureSetOfInfo.
• Well-formedness rules: as must refer to a @classified capability class.
• Normalization rules:
  - it's *, then .as, then .rd,
  - multiple .as normalize to the smallest one if the classes are related,
  - multiple .as 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.
• 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]

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]. This could be useful for instance to characterize the use set of a Try(body). It would be body.asNot[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?