Discussion:
[e-lang] Coercion, membranes, serialization, and printing are the same thing
Kevin Reid
2013-10-12 05:18:43 UTC
Permalink
A motivating problem
--------------------

One of the things that bugs me about E's design as it currently stands is that the obvious application of a guard on circular structure does not terminate.

That is, suppose we write:

def Binary := nullOk[Tuple[Binary, Binary]]

Used as a guard, this will do exactly what it looks like it ought to do, provided that the value is acyclic; if the value is cyclic then the guard application will not terminate, because the guard protocol does not have any cycle-breaking provision.

This seems to me to be against the spirit of E: all things which _can_ sensibly operate on cyclic structure _should_ do so (just as equality does).

The obvious solution
--------------------

We can see an invocation of a guard as the momentary existence of a fragment of a membrane: it maps references on one side to references on the other, as controlled by the guard's coercion. It is not a membrane in that it does not fully enclose a subgraph, and that there is no (need for a) reverse mapping.

This is then simply the memoization-with-cycle-support of the individual guards' coercions. A straightforward implementation:

def coerceWithCycleSupport(value, guard, ejector) {
def seen := [].asMap().diverge()
def subCoerce(value, guard) {
def key := makeTraversalKey([value, guard])
return seen.fetch(key, fn {
def [p, r] := Ref.promise()
seen[key] := p
r.resolve(guard.coerce(value, ejector, subCoerce))
p
});
}
return subCoerce(value, guard)
}

(Note that subCoerce can be captured. This will be useful later.)

We add a third parameter to guards' coerce method, which they use to invoke their sub-guards with cycle breaking. As an example, a partial implementation of the Tuple parameterized guard:

def makeCTuple2(A, B) {
return def tupleGuard {
to coerce(value, ejector, subCoerce) {
def [a, b] exit ejector := value
return [subCoerce(a, A), subCoerce(b, B)]
}
}
}

Then to use such guards, where current E would do
G.coerce(specimen, ejector)
it is instead
coerceWithCycleSupport(specimen, G, ejector).
This is loosely analogous to the use of 'throw.eject' in place of directly calling an ejector object.

I'm not sure that this is actually a good idea to add to guards, because of the additional complexity-of-mechanism and the runtime cost (though it could be optimized by not constructing any promises, or the seen table, unless subCoerce is actually invoked by the particular guard, so that simple guarding like ':int' doesn't end up allocating anything).

(It is also arguable that deep structural guards are a bad idea, since naïvely using them can result in increasing time complexity due to redundant traversals/reconstructions of the same structure.)

The common structure
--------------------

What I find interesting about this is that we have defined a generic reference graph transformation. The algorithm inside of coerceWithCycleSupport is exactly the same as the one used for printing, serialization, and membranes, with some minor differences:

• Printing and serialization do not output reference graphs, and would rather explicitly handle cycles than get promises on the output side.

• Membranes have a bidirectional mapping (i.e. the inverse function of subCoerce is available) and may invoke subCoerce arbitrarily later in time.

It might well be the case that these applications have enough individual quirks that they should be implemented individually -- the core algorithm is not especially lengthy or hard to implement correctly -- but I think it is worth thinking about whether there is value in conceptual unification, or even in shifting the protocols of these four operations to be more similar to each other.


(One of these things which definitely needs changing is the printing system -- for usability, it should be possible to print a structure which contains far references using their specfic __printOn rather than as "<Far ref>", which is not possible in the current approach. The graph transformation technique may make this more straightforward to define -- I am unsure.)
--
Kevin Reid <http://switchb.org/kpreid/>
Tom Van Cutsem
2013-10-12 10:34:14 UTC
Permalink
Hi Kevin,

I have been thinking about generalizing membranes in similar ways.

You mention serialization as a special case of membranes. There's another
similar case I've come across: wrappers that convert between language
boundaries (e.g. E and Java, or AmbientTalk and Java). This is even closer
to membranes in the sense that the language mapping also requires two
directions, which are each other's inverse.

This has been studied to some extent in academic circles, where it's called
"linguistic symbiosis" or "inter-language reflection". For instance, the
equations on p.9 of the following paper <
http://scg.unibe.ch/archive/papers/Gybe06aSymbioticReflectionESUGJournal.pdf>
remind me a lot of the "dry to wet" and "wet to dry" conversions (or
"in->out" and "out->in" conversions) that revocable membranes must
implement.

As it happens, I'm working on trying to express another possible use case
of membranes: the ability to confine objects through ownership types
(seminal paper: Ownership types for Flexible Alias Protection, Clarke et
al., OOPSLA '98 <
http://www.cs.cornell.edu/courses/cs711/2005fa/papers/cpn-oopsla98.pdf>).

The basic idea of ownership types is that you can prevent objects that are
"owned" by an aggregate object to leak from the aggregate. The example used
in the paper is a Car class that has an Engine, but doesn't want any of its
clients to be able to directly refer to the Engine. Ownership types can
catch such leaks statically.

Last year at the Dynamic Languages Symposium, there was a paper about
expressing these ideas in a dynamically typed language (i.c. Smalltalk) <
http://scg.unibe.ch/archive/papers/Wern12c.pdf>. However, they don't use
proxies to implement the confinement, but dynamic checks embedded in the
runtime. I believe this approach suffers from dynamic scoping issues, and I
think membranes based on proxies might provide an alternative solution that
is more aligned with ocaps. (At least, the authors of the DLS paper are
aware of ocaps, they cite the Paradigm regained paper, and they're aware of
membranes).

If anyone is interested in exploring these ideas further, drop me a line.

Regards,
Tom
Post by Kevin Reid
A motivating problem
--------------------
One of the things that bugs me about E's design as it currently stands is
that the obvious application of a guard on circular structure does not
terminate.
def Binary := nullOk[Tuple[Binary, Binary]]
Used as a guard, this will do exactly what it looks like it ought to do,
provided that the value is acyclic; if the value is cyclic then the guard
application will not terminate, because the guard protocol does not have
any cycle-breaking provision.
This seems to me to be against the spirit of E: all things which _can_
sensibly operate on cyclic structure _should_ do so (just as equality does).
The obvious solution
--------------------
We can see an invocation of a guard as the momentary existence of a
fragment of a membrane: it maps references on one side to references on the
other, as controlled by the guard's coercion. It is not a membrane in that
it does not fully enclose a subgraph, and that there is no (need for a)
reverse mapping.
This is then simply the memoization-with-cycle-support of the individual
def coerceWithCycleSupport(value, guard, ejector) {
def seen := [].asMap().diverge()
def subCoerce(value, guard) {
def key := makeTraversalKey([value, guard])
return seen.fetch(key, fn {
def [p, r] := Ref.promise()
seen[key] := p
r.resolve(guard.coerce(value, ejector, subCoerce))
p
});
}
return subCoerce(value, guard)
}
(Note that subCoerce can be captured. This will be useful later.)
We add a third parameter to guards' coerce method, which they use to
invoke their sub-guards with cycle breaking. As an example, a partial
def makeCTuple2(A, B) {
return def tupleGuard {
to coerce(value, ejector, subCoerce) {
def [a, b] exit ejector := value
return [subCoerce(a, A), subCoerce(b, B)]
}
}
}
Then to use such guards, where current E would do
G.coerce(specimen, ejector)
it is instead
coerceWithCycleSupport(specimen, G, ejector).
This is loosely analogous to the use of 'throw.eject' in place of directly
calling an ejector object.
I'm not sure that this is actually a good idea to add to guards, because
of the additional complexity-of-mechanism and the runtime cost (though it
could be optimized by not constructing any promises, or the seen table,
unless subCoerce is actually invoked by the particular guard, so that
simple guarding like ':int' doesn't end up allocating anything).
(It is also arguable that deep structural guards are a bad idea, since
naïvely using them can result in increasing time complexity due to
redundant traversals/reconstructions of the same structure.)
The common structure
--------------------
What I find interesting about this is that we have defined a generic
reference graph transformation. The algorithm inside of
coerceWithCycleSupport is exactly the same as the one used for printing,
• Printing and serialization do not output reference graphs, and would
rather explicitly handle cycles than get promises on the output side.
• Membranes have a bidirectional mapping (i.e. the inverse function of
subCoerce is available) and may invoke subCoerce arbitrarily later in time.
It might well be the case that these applications have enough individual
quirks that they should be implemented individually -- the core algorithm
is not especially lengthy or hard to implement correctly -- but I think it
is worth thinking about whether there is value in conceptual unification,
or even in shifting the protocols of these four operations to be more
similar to each other.
(One of these things which definitely needs changing is the printing
system -- for usability, it should be possible to print a structure which
contains far references using their specfic __printOn rather than as "<Far
ref>", which is not possible in the current approach. The graph
transformation technique may make this more straightforward to define -- I
am unsure.)
--
Kevin Reid <http://switchb.org/kpreid/>
_______________________________________________
e-lang mailing list
http://www.eros-os.org/mailman/listinfo/e-lang
James Noble
2013-10-20 00:36:02 UTC
Permalink
As it happens, I'm working on trying to express another possible use case of membranes: the ability to confine objects through ownership types (seminal paper: Ownership types for Flexible Alias Protection, Clarke et al., OOPSLA '98 <http://www.cs.cornell.edu/courses/cs711/2005fa/papers/cpn-oopsla98.pdf>).
certainly membranes and ownership must be related - although the precise relationship I hasn't been worked out.
Last year at the Dynamic Languages Symposium, there was a paper about expressing these ideas in a dynamically typed language (i.c. Smalltalk) <http://scg.unibe.ch/archive/papers/Wern12c.pdf>. However, they don't use proxies to implement the confinement, but dynamic checks embedded in the runtime. I believe this approach suffers from dynamic scoping issues, and I think membranes based on proxies might provide an alternative solution that is more aligned with ocaps. (At least, the authors of the DLS paper are aware of ocaps, they cite the Paradigm regained paper, and they're aware of membranes)
there's an older paper on dynamic ownership here - http://dl.acm.org/citation.cfm?id=1297090 & attached.

I think the question of where & how ownership ("property rights") should be enforced is an interesting one.
Patterns like being careful about private or protected names can give effect to ownership in Java;
in Javascript, nested lambda scopes can protect names --- but you'll need another (static?) analysis
to ensure that objects that are intended to be confined are not leaked out.
(see eg. here: http://dx.doi.org/10.1145/949343.949339, http://www.cs.tau.ac.il/~msagiv/courses/encapsulate/p82-vitek.pdf)

But in terms of capturing programmer's intention ---- audibility ---
being able to say "this engine is mine", and being sure that gives rise to
some dependable semantics, is going to be safer than depending on rather
fiddly programming patterns.
If anyone is interested in exploring these ideas further, drop me a line.
I'm always interested in ownership stuff, always happy to talk --- and Sophia is too, I'm sure.

cheers

James
Tom Van Cutsem
2013-10-28 20:17:58 UTC
Permalink
Hi James,
Post by James Noble
there's an older paper on dynamic ownership here -
http://dl.acm.org/citation.cfm?id=1297090 & attached.
Thanks for the reference. I was aware of this work, it's also cited by
Wernli's DLS2012 paper.

One thing that's still different from a membrane-based approach to
implementing ownership, is that your work on dynamic ownership (and also
Wernli's work on Filters), augments objects with explicit ownership
pointers, and adds runtime checks on all method calls to verify ownership.

What I'm considering with membranes is to define ownership *implicitly*:
all objects wrapped by the same membrane would be considered "owned" by the
same owner. Then, instead of intercepting all method calls to perform
runtime ownership checks, only the proxies at the boundary of the membrane
would perform the ownership checks.

Now, this approach is really only viable in an ocap language, because
membranes can easily be circumvented when there is global shared mutable
state.

I've implemented a first prototype of membrane-based ownership in
JavaScript (extensive README available here <
https://github.com/tvcutsem/harmony-reflect/tree/master/examples/ownership>).
It's based on Wernli's ideas of filters, but implemented using membranes
and proxies rather than by augmenting objects with ownership pointers (the
latter would require either changing the VM or doing a full
source-to-source translation).
Post by James Noble
I think the question of where & how ownership ("property rights") should
be enforced is an interesting one.
Patterns like being careful about private or protected names can give
effect to ownership in Java;
in Javascript, nested lambda scopes can protect names --- but you'll need
another (static?) analysis
to ensure that objects that are intended to be confined are not leaked out.
(see eg. here: http://dx.doi.org/10.1145/949343.949339,
http://www.cs.tau.ac.il/~msagiv/courses/encapsulate/p82-vitek.pdf)
But in terms of capturing programmer's intention ---- audibility ---
being able to say "this engine is mine", and being sure that gives rise to
some dependable semantics, is going to be safer than depending on rather
fiddly programming patterns.
Agreed!

Even with support for ownership (static or dynamic), there is still a
danger that the programmer forgets to express the right ownership
boundaries, but at least having a language abstraction to express the
ownership boundaries is a step in the right direction.

Regards,
Tom
James Noble
2013-10-28 20:56:18 UTC
Permalink
Thanks for the reference. I was aware of this work, it's also cited by Wernli's DLS2012 paper.
argh sorry for the gratuitous citation trolling...
One thing that's still different from a membrane-based approach to implementing ownership, is that your work on dynamic ownership (and also Wernli's work on Filters), augments objects with explicit ownership pointers, and adds runtime checks on all method calls to verify ownership.
right. And I still think that's a good conceptual model
What I'm considering with membranes is to define ownership *implicitly*: all objects wrapped by the same membrane would be considered "owned" by the same owner. Then, instead of intercepting all method calls to perform runtime ownership checks, only the proxies at the boundary of the membrane would perform the ownership checks.
Yes. Or rather, it's not really implicit ownership (because putting objects inside a membrane is explicit
in program code) --- but it's doing that without language / VM level support.
Now, this approach is really only viable in an ocap language, because membranes can easily be circumvented when there is global shared mutable state.
of course...
I've implemented a first prototype of membrane-based ownership in JavaScript (extensive README available here <https://github.com/tvcutsem/harmony-reflect/tree/master/examples/ownership>). It's based on Wernli's ideas of filters, but implemented using membranes and proxies
oh that is cool!
rather than by augmenting objects with ownership pointers (the latter would require either changing the VM or doing a full source-to-source translation).
right. Donald Gordon hacked the Bean Shell implementation,
and many moons ago I did something reflexive in Self...
Even with support for ownership (static or dynamic), there is still a danger that the programmer forgets to express the right ownership boundaries, but at least having a language abstraction to express the ownership boundaries is a step in the right direction.
right. And that's the distinction I'd make between implicit and explicit:
explicit says "this stuff belongs behind a boundary" in some way in code;
implicit says it in comments, and is just (hopefully) careful not to let things leak.

James
Moore, Scott
2013-10-31 18:07:04 UTC
Permalink
Hi Tom,

Recently, we’ve been studying how we can reason about using membranes to control the flow of capabilities in web applications. As part of this, we’ve also been working on establishing the relationship between ownership and membranes in ocap languages.

We developed a formal system that uses higher-order contracts to track the ownership of capabilities. This mechanism can be considered a particular type of membrane. We show that the mechanism soundly tracks the ownership of capabilities. Thus, the technique may be useful in showing that membranes are sufficient to track ownership in other (non-capability safe) settings (like JavaScript), or what additional conditions are required to do so.

For those that are interested, in addition to tracking the ownership of capabilities we extend our model of a capability-safe language with access control and information-flow policy annotations on capabilities that describe restrictions on which parts of the program may access the capabilities or influence their use. Access control policies can be used to ensure that capabilities are not “leaked” from the abstractions (membranes) designed to protect them. The information-flow policies can be used to enforce stronger invariants: that certain parts of the program may not affect the use of certain capabilities (i.e. integrity of use), even *indirectly*.

We use the higher-order contracts described above as membranes to enforce the access control policies. For the information-flow policies, we use an information-flow type system. We also show how to compose these mechanisms, in particular allowing for programs in which some parts enforce only access control policies and others enforce information-flow policies.

If you are interested in our work, please drop us a line and we can send you a draft of our paper. (It's joint work with Christos Dimoulas, Aslan Askarov, and Stephen Chong here at Harvard.)

Cheers,
Scott Moore
Post by Tom Van Cutsem
Hi James,
there's an older paper on dynamic ownership here - http://dl.acm.org/citation.cfm?id=1297090 & attached.
Thanks for the reference. I was aware of this work, it's also cited by Wernli's DLS2012 paper.
One thing that's still different from a membrane-based approach to implementing ownership, is that your work on dynamic ownership (and also Wernli's work on Filters), augments objects with explicit ownership pointers, and adds runtime checks on all method calls to verify ownership.
What I'm considering with membranes is to define ownership *implicitly*: all objects wrapped by the same membrane would be considered "owned" by the same owner. Then, instead of intercepting all method calls to perform runtime ownership checks, only the proxies at the boundary of the membrane would perform the ownership checks.
Now, this approach is really only viable in an ocap language, because membranes can easily be circumvented when there is global shared mutable state.
I've implemented a first prototype of membrane-based ownership in JavaScript (extensive README available here <https://github.com/tvcutsem/harmony-reflect/tree/master/examples/ownership>). It's based on Wernli's ideas of filters, but implemented using membranes and proxies rather than by augmenting objects with ownership pointers (the latter would require either changing the VM or doing a full source-to-source translation).
I think the question of where & how ownership ("property rights") should be enforced is an interesting one.
Patterns like being careful about private or protected names can give effect to ownership in Java;
in Javascript, nested lambda scopes can protect names --- but you'll need another (static?) analysis
to ensure that objects that are intended to be confined are not leaked out.
(see eg. here: http://dx.doi.org/10.1145/949343.949339, http://www.cs.tau.ac.il/~msagiv/courses/encapsulate/p82-vitek.pdf)
But in terms of capturing programmer's intention ---- audibility ---
being able to say "this engine is mine", and being sure that gives rise to
some dependable semantics, is going to be safer than depending on rather
fiddly programming patterns.
Agreed!
Even with support for ownership (static or dynamic), there is still a danger that the programmer forgets to express the right ownership boundaries, but at least having a language abstraction to express the ownership boundaries is a step in the right direction.
Regards,
Tom
_______________________________________________
e-lang mailing list
http://www.eros-os.org/mailman/listinfo/e-lang
James Noble
2013-10-31 18:14:38 UTC
Permalink
Scott-- I'm interested, and I'm sure Sophia will be too - James
Post by Moore, Scott
If you are interested in our work, please drop us a line and we can send you a draft of our paper. (It's joint work with Christos Dimoulas, Aslan Askarov, and Stephen Chong here at Harvard.)
Mike Stay
2013-10-31 18:24:41 UTC
Permalink
Ditto!
Post by James Noble
Scott-- I'm interested, and I'm sure Sophia will be too - James
Post by Moore, Scott
If you are interested in our work, please drop us a line and we can send you a draft of our paper. (It's joint work with Christos Dimoulas, Aslan Askarov, and Stephen Chong here at Harvard.)
_______________________________________________
e-lang mailing list
http://www.eros-os.org/mailman/listinfo/e-lang
--
Mike Stay - ***@gmail.com
http://www.cs.auckland.ac.nz/~mike
http://reperiendi.wordpress.com
Drossopoulou, Sophia
2013-10-31 18:27:12 UTC
Permalink
ditto

-----Original Message-----
From: Mike Stay [mailto:***@gmail.com]
Sent: 31 October 2013 18:25
To: Discussion of E and other capability languages
Cc: Sophia Drossopoulou
Subject: Re: [e-lang] Coercion, membranes, serialization, and printing are the same thing

Ditto!
Post by James Noble
Scott-- I'm interested, and I'm sure Sophia will be too - James
Post by Moore, Scott
If you are interested in our work, please drop us a line and we can send you a draft of our paper. (It's joint work with Christos Dimoulas, Aslan Askarov, and Stephen Chong here at Harvard.)
_______________________________________________
e-lang mailing list
http://www.eros-os.org/mailman/listinfo/e-lang
--
Mike Stay - ***@gmail.com
http://www.cs.auckland.ac.nz/~mike
http://reperiendi.wordpress.com
Mark S. Miller
2013-10-31 18:39:54 UTC
Permalink
of course ;).


On Thu, Oct 31, 2013 at 11:27 AM, Drossopoulou, Sophia <
Post by Drossopoulou, Sophia
ditto
-----Original Message-----
Sent: 31 October 2013 18:25
To: Discussion of E and other capability languages
Cc: Sophia Drossopoulou
Subject: Re: [e-lang] Coercion, membranes, serialization, and printing are the same thing
Ditto!
Post by James Noble
Scott-- I'm interested, and I'm sure Sophia will be too - James
Post by Moore, Scott
If you are interested in our work, please drop us a line and we can
send you a draft of our paper. (It's joint work with Christos Dimoulas,
Aslan Askarov, and Stephen Chong here at Harvard.)
Post by James Noble
_______________________________________________
e-lang mailing list
http://www.eros-os.org/mailman/listinfo/e-lang
--
http://www.cs.auckland.ac.nz/~mike
http://reperiendi.wordpress.com
_______________________________________________
e-lang mailing list
http://www.eros-os.org/mailman/listinfo/e-lang
--
Cheers,
--MarkM
Loading...