Feature proposal: Parametric permissions

[bgamari]

Currently permissions are merely names. However, Ward could be made significantly more powerful by extending the permission language with some notion of parameterisation on source program identifiers. To make this concrete, let's say we have some datastructure (call it Capability, drawing on the concept from GHC) which embeds a lock:

struct Capability {
  Mutex lock;
  int some_state;
};

We want to expose a function which can change some_state of a Capability yet only if the caller holds its lock. To do this we might define the following:

#define WARD(...) __attribute__((__VA_ARGS__))

WARD(need(may_take_capability_lock(cap), grant(holds_capablity_lock(cap)))
void acquire_capability_lock(Capability *cap) {
  ACQUIRE_MUTEX(&cap->lock);
}

WARD(need(holds_capability_lock(cap), revoke(holds_capablity_lock(cap)))
void release_capability_lock(Capability *cap) {
  RELEASE_MUTEX(&cap->lock);
}

WARD(need(holds_capability_lock(cap))
void set_state(Capability *cap, int new_state) {
  cap->state = new_state;
}

Here we have extended the permission language as follows:

permission_name := string
permission := permission_name ['(' arg_list ')']
arg_list := argument [',' arg_list]
argument := c_identifier

Where argument must be either a global variable or an identifier bound in the function's argument list. For simplicity, call sites of functions with such permissions would be restricted to only "trivial" parameters (e.g. just identifiers). This would allow permissions to be easily propagated from the call-site to the definition site. For instance,

WARD(need(may_take_capability_lock(cap))
void set_state_to_zero(Capability *the_cap) {
  acquire_capability_lock(the_cap);
  // We now have holds_capability_lock(the_cap) in our context
  set_state(the_cap, 0);
  // By the definition given above, the above call requires that we
  // have holds_capability_lock(the_cap), which we indeed have.
  release_capability_lock(the_cap);
}

The arity of a capability is fixed in the configuration. For instance the Ward configuration for the above might look like:

holds_capability_lock(cap) "The given capability's lock is held";
may_take_capability_lock(cap) "The may take the given capability's lock";

Note that under this proposal arguments are untyped. That is, one is free to write seemingly nonsensical things like,

WARD(grant(may_take_capability_lock(n)))
void do_something(int n) {  /* ... */ }

Additionally, the fact that permissions may take multiple arguments allows to represent relations between runtime values. For instance in GHC Tasks can "own" Capability's, allowing us to do some things in a lock-free manner,

__thread struct Task my_task; // the current thread's task

WARD(need(task_owns_capability(my_task, cap)))
void do_something(Capability *cap) { /* ... */ }

Limitations

There are, of course, many cases that this minimal proposal is not able to cover. For instance,

void set_all_to_zero(int n, Capabilities *caps[n]) {
  for (int i=0; i < n; i++)
    set_state_to_zero(caps[i]);
}

We sadly have no way to express the permission requirements of this function. To handle this we need the ability to embed permission actions in function bodies:

void set_all_to_zero(int n, Capability *caps[n]) {
  for (int i=0; i < n; i++) {
    Capability *cap = caps[i];
    WARD(grant(may_take_capability_lock(cap)));
    set_state_to_zero(cap);
  }
}

This of course makes set_all_to_zero part of the trusted codebase.

Extensions

Return terms

We could do slightly better on the above case by extending our permission syntax with:

argument := c_identifier
          | 'return'

Where the return keyword denotes the return value of the function. This allows us to write:

WARD(need(may_take_capability_lock(caps), grant(may_take_capability_lock(return)))
Capability *get_capability(int i, Capability *caps[i]) {
  return caps[i];
}

Allowing indexing

One could imagine further extending the permission syntax with:

argument := term [ '[' integer_literal ']' ]
term := c_identifier
      | 'return'

which would allow a few more patterns to be captured. For instance, output parameters:

WARD(grant(may_take_capability_lock(cap[0])))
void get_a_capability(Capability **cap) {  /* cap is an output */
  *cap = ...;
}

Implementation

My suspicion is that nothing of the above should be particularly difficult to implement. The only non-trivial aspect the proposal is the argument renaming necessary at call-sites but this is a simple mechanical rewrite.

[evincarofautumn]

Sounds good to me. IIRC I had this in mind to support the “domain locks” in Mono, where each MonoDomain has its own associated global lock. It’s just a matter of getting around to it…

I like the idea of supporting return to annotate the result value of a function, although it might be kinda fiddly to propagate that info up the call tree.

Have to check if this is allowed, but for annotations pertaining to parameters, I wonder if we could support attributes on the parameters themselves, e.g.:

WARD(grant(may_take_capability_lock(return)))
Capability *get_capability(
  int i,
  Capability *caps[i] WARD(need(may_take_capability_lock))
) {
  return caps[i];
}

[bgamari]

Have to check if this is allowed, but for annotations pertaining to parameters, I wonder if we could support attributes on the parameters themselves, e.g.:

I think I would actually prefer to keep the annotation on the function. Afterall, a permission may in fact have more than one parameter, allowing one to represent relations between multiple terms in the source program (e.g. the Task/Capability example given in the description).