The goal is to mitigate the difficulty of writing and reasoning about code for global concerns such as application privacy. We want to allow the programmer to write high-level policies for global concerns that are automatically handled.
It is often difficult to implement global concerns that are intertwined with the core program. For instance, enforcing fine-grained privacy policies in social networks requires global reasoning about how seemingly unrelated interactions in the core program can leak information. We want to allow the programmer to reason about such concerns at a high level and automatically handles their enforcement.Programming model
Programming with delegation supports nondeterminism to unburden the programmer from having to specify certain behaviors but restricts the nondeterminism to allow for efficient execution. We have developed the Jeeves programming language, which extends an ML-like functional language with support for nondeterministic delegated expressions. Delegated expressions are evaluated according to the semantics of the program and programmer-specified constraints. The nondeterminism is preserved until the programmer requests a concrete expression, at which point the runtime produces a value lazily in the dynamic context.
The main differences between Jeeves and prior languages for programming with delegation are:
(1) Nondeterministic values can interact with the entire program rather than to designated parts of the program.(2) Jeeves has a specialized policy language that allows constraints on nondeterministic values to refer to contexts in which the resulting value will be determinized.
For the programs we target, having a restricted form of nondeterminism throughout the program can yield a more efficient execution strategy than having unbounded nondeterminism in restricted parts of the program. We have been developing an efficient interpreter implementation that executes symbolically while minimizing the size of the symbolic state and constraint environment. The interpreter performs eager simplifications to reduce the size of the symbolic environment but resolves constraints lazily when the program requests a deterministic value. This execution strategy takes advantage of the assumption that the program is mostly deterministic.
We have a semantics for the Jeeves language and a prototype interpreter written in OCaml, C++, and the Yices SMT solver. We are currently interested in looking at how delegation is useful in different domains.