Splitting linear * read without jailing type checks #450
Assignees
Labels
Comments
|
Fixed by 9989f4d |
kikofernandez
pushed a commit
that referenced
this issue
Apr 5, 2017
* Beta support for Kappa
Commit history below:
Experimental support for linear capabilities
This commit lets the programmer annotate traits with modes. An included
trait must have a mode, either given at inclusion time, or given in the
trait header (this works as a default). There are currently two modes;
`linear` whose references must be treated linearly, and `unsafe` which
works just like a regular type (no restrictions on aliasing). A value of
class type may be cast into a trait type (like in `master`) or
a (composite) capability type. All modes must match exactly. Here is a
small example program to show what is currently possible:
```
-- Foo defaults to unsafe
unsafe trait Foo<t>
require f : t
def foo() : void
print "Foo!"
-- Inclusion of Bar requires specifying a mode
trait Bar
-- C can be aliased freely
passive class C<t> : Foo<t> + unsafe Bar
f : t
-- D must be treated linearly unless upcast to Foo<int>
passive class D : Foo<int> + linear Bar
f : int
class Main
def main() : void
let x = new D
y = consume x : linear Bar + unsafe Foo<int>
z = consume y : Foo<int>
w = z
in
w.foo()
```
The checking that linearity is preserved is done using an additional
pass, implemented in the file `src/typechecker/Capturechecker.hs`. This
keeps the changes made to `Typechecker.hs` to a minimum, which is nice.
Basically, the capturechecker figures out where references are captured
and when a linear reference is safe to capture.
The linear references **should** be interoperable with all the features
currently in Encore, but testing is very welcome! It should be noted
that consumes are currently not atomic (the value is read and nullified
sequentially), but this shouldn't matter in a race-free program. Linear
streams are possible but not very useful, since both `get` and `getNext`
require you to consume the stream. For any useful patterns we would need
a way to `get` and move the stream forward in one go (maybe `consume s`
should be the way to do this?).
Experimental support for borrowing
This commit adds support for declaring parameters as
stackbound (`S(Foo)`). A linear reference can be passed as a stack bound
parameter without consuming, as the linear alias is buried for the
duration of the call (borrowing requires a synchronous call). A
stackbound may be locally aliased (but not returned from functions or
methods), but cannot be used in parallel (so far this means that it may
not be passed to an active object). The following program exemplifies
most uses of borrowing:
```
-- Stackbounds cannot be returned from functions or methods
-- def steal(x : S(Token)) : S(Token)
-- x
def borrow(x : S(Token)) : void{
let thief = new Thief<Token>
y = x -- Stackbounds can be locally aliased
in{
-- thief.steal(x); -- Stackbounds cannot be passed to active objects
borrowAgain(y); -- Stackbounds can be passed to other borrowing functions/methods
}
}
def borrowAgain(x : S(Token)) : void{
x.foo(); -- You can call methods and access fields on stackbound objects
}
class Main
-- f : S(Foo<int>) -- Fields cannot be stackbound
def borrow(x : S(Token)) : void
borrow(x.f) -- Fields of linear objects can be borrowed as long as each node in the path is linear
def main() : void
let x = new Token
thief = new Thief<Token>
in{
-- thief.steal(x); -- Linear values cannot be borrowed by active objects
x.f = new Token;
this.borrow(x); -- Synchronous method calls can borrow linear values
}
trait Foo
def foo() : void
print "Foo!"
passive class Token : linear Foo
f : Token
class Thief<t>
def steal(x : S(t)) : void
()
```
Borrowing should interplay nicely with arrays and most other programming
constructs, but please do report anomalies of any kind.
made embeds free
Support for read mode
This was actually implemented before, but was lost in a git related
accident...
A trait with the `read` mode can only require `val` fields of safe
types. The safe types are active objects, primitives and passive objects
with a safe mode (currently only `read` itself).
Support for subordinate mode
Types containing a capability type with the `subord` mode cannot be
returned from its surrounding aggregate. This is checked by controlling
the target of a method call or field access and throwing an error unless
the target is `this` or is fully encapsulated itself (i.e. is a
capability type with *only* subordinate capabilities). Traits without
manifest modes are typechecked as if they were subordinate, but they
still need to be given an explicit mode at inclusion.
A known issue is that subordinate state can be leaked via closures.
Support for thread mode
Capabilities with the thread mode may not leave the active object that
created it. This is checked when calling methods on active objects; if
an argument is thread or the return type is thread, the target must
either be this, or itself be thread. This also means that fields with
the thread mode can only be declared in traits that are manifestly
thread.
Experimental splitting support
A let expression can now have several variables *per expression*, and
each variable can optionally have a type annotation:
```
let i, f : float = 42;
print i; -- 42
print f; -- 42.000000
```
If the types of the variables are linear, these are checked to be in
conjunction in the type of the right hand side:
```
let p = new Person();
let a : Aged, n : Named = consume p;
```
If the types are not linear any splitting is allowed. Not giving a type
to a variable defaults to the type of the right hand side (meaning any
splitting will fail).
Fix #451, parsing error with manifest modes
Since `read` is not a reserved keyword, the following code:
```
class T
read trait Get
```
was parsed as
```
class T
read <Expecting ':'>
trait Get
```
This is fixed by adding a `try` that allows the parser to backtrack when
reading a field fails.
Read mode must be manifestly set
To simplify typechecking, the read mode must be manifestly set. It can
still be used on inclusion, but only if the included trait already is
manifestly read.
Fix #452, consider safe composite types safe
This commit considers `Maybe T`, `Stream T`, `Fut T` and `Par T` as safe
types iff `T` is a safe type. Tuples are safe if all the constituent
types are safe. Ranges are also safe.
Arrays are not safe since they can be written to. In the future one
could consider a type like `[val T]` to be safe (an array that can only
be read from). I'll leave that design up to @glundi.
Fixed upcasting bug
Before this commit, a composite type was only checked for subsumption of
operations, meaning that `T1 + T2` could be cast to `T1 * T2`. Now an
upcast must preserve the conjunctions of the subtype (i.e. not introduce
new ones). It is still safe to forget conjunctions by casting `T1 * T2`
into `T1 + T2`.
Fix #450, check conjunctiveness when splitting
Before this commit, there was a bug when checking of whether an unpack was
allowed that lead to code like `let read Get, linear Set = consume Cell`
compiling. This is now fixed so that all types in an unpack needs to be
separated by a conjunction in the capability being unpacked, unless all
the types can safely be (at least locally) aliased.
A known bug is that we also need to check that the modes are preserved
for all types in an upcast, meaning that the `read Get` above should
also be `linear` (assuming `Get` and `Set` are conjunctive in `Cell`).
Fixed capture bug when matching on tuples
This commit fixes a bug where matching on a tuple with a linear value
would not allow you to capture that value in a pattern:
```
let x = new LinearThing();
match (42, consume x) with
(n, y) => () -- Cannot capture linear expression y
```
The solution is a bit clunky but works. It adds a boolean in the
meta-blob to mark which expressions are patterns. Patterns can then be
ignored by the capture checker.
Disallow sending borrowed values to constructors
Fix #604, a bug where borrowed values could be passed as (non-borrowed)
arguments to constructors. Constructors now work like normal method
calls.
Also moved all (both) tests regarding capabilities to a test-suite of
their own and added more tests regarding borrowing.
Prevent arrays of borrowed elements
Disallow the type `[borrowed T]`, since it can be used to duplicate
linear values (see the test `arrayBorrow.enc`).
Support for safe closures
A closure is now annotated when capturing a `thread`, `subord` or
`borrowed` capability, meaning you cannot cheat the type system by
capturing state in closures. See tests `capabilities/closure*` for
examples.
Check overriding of methods in read traits
This commit adapts method overriding and provision to consider read
traits. A required method in a read trait can only be provided by
another read trait. A read trait can only be extended with `val` fields
of safe type. See tests `readTrait*` for examples.
A current issue is that there is no way to consider passive classes
safe. Currently, there is a special case for the class `String`, but we
should come up with a way that makes it possible to consider classes
safe.
Thread mode => Local mode
Remove unsafe traits from tests
Check for clashing manifest modes
Read and subordinate are minor modes
Support for moded classes (NO TESTS)
Support for looking up marker trait (ignore mode)
Translated capability test suite
Translated basic tests to Kappa
Translated trait tests to Kappa
Translated concurrency tests
Translated the remaining tests, modulo shared
Support for shared mode (very imprecise...)
Only allow safe type arguments
Warnings for unsafe operations
Currently passing arrays and splitting conjunctions
Fixed bug in capability splitting
Support for strong updates (dropping linear capabilities)
Fix regression
Updated last bits of standard library
Allow local in active
Added tests and moved old tests around
* Remove comments and unused code
* Translated Savina benchmarks to Kappa
* Removed null-check hack from Savina
* Refactoring after Kiko's suggentions
* Fixed bug when giving mode to unmoded class
* Fixed bug with implicitly safe class
* Set formal arrow type
* Merged errors
* Merge capturechecking errors with typechecking errors
* Relax polymorphism to allow local type arguments
Instead, polymorphic values cannot be passed between
actors (currently this is only warned about).
* Improve error messages
* Removed unused Makefiles
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
The line TYPE CHECKS below should not.
The text was updated successfully, but these errors were encountered: