On Wed, Dec 4, 2013 at 5:59 PM, Mark Miller <erig...@gmail.com> wrote: > Good, I think we're converging on what the important sub-problem is: > building an abstraction mechanism that enables the open-ended expression of > projections, but not the expression of non-projections. My previous > statements about join were premised on such a projection-only abstraction. > But I mistakenly thought that we could build it by adapting the E and Joe-E > auditor logic. Sam is right that we can't. Some of Cormac's work on > trace-monitoring temporal contracts might be the answer, or at least a place > to start. > > Once we have such an open-ended projection-only abstraction, then all these > questions about equality become interesting and pressing.
I'm unconvinced that this is genuinely a problem that needs solving. In particular, I don't think that given such a projection-only abstraction, any of the questions about equality are easier. For example, if we had one, that wouldn't reduce our desire to have a pointer-equality predicate for performance, given which none of the invariants about programs that you think you have in the presence of projection-only abstractions are actually invariants. Additionally, I'm still unconvinced that "is a projection" is a useful heuristic for "I should be willing to trust this unknown code". In particular, termination and resources are both real concerns. When the question is "should I synchronously invoke this unknown untrusted code in my heap and address space", I'd want a lot stronger guarantee than "is a projection". Third, the ability to handle failure is a genuine semantic problem. Finally, if the expression of non-projections in proxies that produce true when compared to the underlying object is a problem, then there ought to be some some program that demonstrates this problem; some attack that can be demonstrated. But I don't think we've seen one yet in this discussion. Sam > > > On Wed, Dec 4, 2013 at 1:55 PM, Peter Thiemann > <thiem...@informatik.uni-freiburg.de> wrote: >> >> On 12/4/13 5:54 PM, Mark Miller wrote: >>> >>> >>> Consider >>> var p = new Proxy ( target, handler); >>> The trick is *not* to trap equality, but to let the handler >>> control whether EQ dereferences p to target before comparing >>> pointers. Notice that one handler only controls one step of >>> dereferencing. If target is a proxy, again, then EQ recursively >>> asks that proxy's handler until either a non-proxy object is >>> reached *or* the handler does not request further forwarding. >>> Here is an outline of the proposal: >>> http://proglang.informatik.uni-freiburg.de/projects/JSProxy/proxy.pdf >>> >>> With this design each individual proxy can choose to be >>> transparent or opaque, while guaranteeing that EQ implements a >>> non-trivial equivalence relation - the latter is straightforward >>> to check. >>> >>> >>> Ok good, I see how this provides a meaningful equivalence relation. But I >>> don't see how it helps your goal. >>> >>> a) In order to do a membrane of any sort, including a contract-membrane, >>> you need to use the shadow target technique, where the system-recognized >>> target for master and slave in your example are distinct shadow targets. And >>> where the shared real target is not system recognized, but is only our way >>> of describing what the handlers are doing; and thus not available to any >>> system enforcement mechanism. >> >> >> I don't think that all contracts require a membrane, for example, if you >> just restrict an object to reading or writing a subset of its properties, >> then no recursive wrapping is required. >> I don't understand "shadow target technique", but if the master/slave >> roles are contracts like Role1 and Role2, then each of them can be >> represented by a proxy and the two proxies can share a single target. >> >> >>> >>> You write "If x===y, then uses of x and y *in their common interface* >>> (i.e., in the intersection of their roles) are interchangeable." >>> >>> b) But this is untrue in your proposal, even if the same >>> system-recognized target were somehow used, because the different handlers >>> can perform different side effects, including differing side effects on the >>> shared target. >> >> >> True. I was stuck in the contract world, where the handler implements a >> projection. >> So I should tune down my proposal to contract wrappers where contracts are >> implemented in a suitable DSL that only expresses projections. >> >> >>> >>> >>> Let's distinguish two categories of membrane: >>> >>> x) A general membrane maintains the basic membrane invariant, that there >>> is no leakage across the membrane boundary. But invocations that cross the >>> membrane can have their meaning changed by the handlers in any way allowed >>> by the JS Proxy invariant enforcement mechanism. >>> >>> y) A guarding membrane is one which either disallows an operation, or >>> (identity aside) allows it with the same semantics it would have had in the >>> absence of the membrane's interposition. >>> >>> Given checkably-pure functions (which E and Joe-E have but JS currently >>> does not) one can use the general membrane mechanism to build a membrane >>> maker to be parameterized by checkably-pure guard predicates, so that it >>> only makes guarding membranes. What you (and IIUC Phil and Jeremy) are >>> generally seeking are guarding membranes, which would answer issue #b. But >>> in JS (as of ES6) these would be implemented by unprivileged user code, and >>> so not something that the === implementation could directly recognize. A new >>> equivalence operation, whether an EQ-like equivalence predicate or a join, >>> could be provided as part of the same package and be in bed with this >>> guarding membrane maker. >>> >>> Note that the guarding membranes made by this maker would still need to >>> use the shadow target technique, so objection #a still stands -- testing >>> "the same system-recognized proxy target" will not help you build these new >>> equivalence operations as part of the guarding membrane maker package. >> >> >> My understanding of the above is that given an appropriate way of >> restricting a handler to essentially implement a projection, then the proxy >> of that handler could safely be transparent while granting an equivalence >> restricted to uses in the common interface. >> Well, such a handler DSL could be designed and then we could all have our >> cake and eat it. >> >> >> -Peter >> >> >>> >>> >>> >>> >>> In any case, weakening EQ so that the only guarantee that >>> remains is that it is an equivalence relation would break >>> existing uses of EQ in JS (i.e., "===" aside from NaN). For >>> example, an EQ that always said true would still be an >>> equivalence relation, so clearly something more is needed. The >>> position Tom and I take is that, aside from -0.0, JS === >>> guarantees full observational equivalence, i.e., for any >>> program containing the fragment >>> >>> if (x === y) { >>> .... x .... >>> } >>> >>> if all or any or all of the mentions of x in the body were >>> changed to y, the meaning of the program would not change. >>> (Also, given the usual simplifying assumptions about renaming, >>> non-shadowing, and alpha equivalence.) >>> >>> If the guarantees your === would provide is weaker than that, >>> what are its guarantees, and why do you believe those to be >>> sufficient? >>> >>> >>> Observational equivalence is hard to argue against, but I’ll give >>> it a try, anyway. I believe such a strong spec is too limiting and >>> excludes many useful applications. Examples that I am concerned >>> about are wrappers for transparent monitoring and enforcing >>> contracts. Apparently and unsurprisingly others are concerned >>> about these examples, too. >>> >>> >>> Here is an example scenario. Then, I provide some code fragments >>> to support a proposal for a weaker spec for ===. This leads to a >>> question about join in the end. >>> >>> ~~~~~~ >>> >>> Consider a function sync(master,slave) that takes two objects and >>> that wants these two objects to exchange information: the master >>> syncing with the slave. For efficiency, the function sync first >>> checks if these two objects are “the same”, in which case no >>> synchronization is needed; perhaps a flag or timestamp needs to be >>> set to indicate that synchronization has been achieved. If the >>> objects are different, then some potentially expensive sequence of >>> method calls may be needed to exchange the information. (Perhaps >>> involving authentication, passing of capabilities, etc.) >>> >>> >>> If we put a contract on sync that imposes a Master interface on >>> master and a Slave interface on slave and this contract is >>> implemented using opaque proxies, then the sync function is losing >>> the efficient shortcut. >>> >>> >>> (Why would an object implement the Master and the Slave interface? >>> Here are two possible reasons: the master may be elected at run >>> time or there may be a hierarchical system where level-n masters >>> are slaves on level-(n+1)) >>> >>> ~~~~~~ >>> >>> A proposal for a weaker spec for === >>> >>> >>> In the following code fragments, I am using Java interface >>> notation to indicate a dynamically checked contract for brevity. >>> >>> Let’s say we have a function that can treat “same” objects more >>> efficiently, as motivated in the sync example: >>> >>> >>> function f (x, y) { >>> >>> ... >>> >>> if (x === y) { >>> >>> … x.foo(); x.inc(); y.inc(); z = y.bar() … >>> >>> } >>> >>> … >>> >>> } >>> >>> >>> Using contracts, x and y may be restricted to certain roles. >>> >>> Let’s say, >>> >>> interface Role1 { >>> >>> foo(); >>> >>> inc(); >>> >>> } >>> >>> interface Role2 { >>> >>> bar(); >>> >>> inc(); >>> >>> } >>> >>> >>> var g = … apply contract( (Role1, Role2) -> Any ) to f; >>> >>> >>> var obj = { >>> >>> state: 42; >>> >>> foo: function () { this.state = 0; }; >>> >>> bar: function () { return this.state;}; >>> >>> inc: function () { this.state++; }; >>> >>> } >>> >>> >>> g (obj, obj); >>> >>> >>> I want to argue that this call of g should execute the code >>> guarded by (x === y) in f, because the interposition of the >>> contract may otherwise change the semantics. In other words, I >>> want to make sure that g(obj, obj) either raises an error due to a >>> contract violation or it has exactly the same effect and result as >>> f(obj, obj). >>> >>> >>> What guarantees can we assume below (x===y)? >>> >>> If x===y, then uses of x and y *in their common interface* (i.e., >>> in the intersection of their roles) are interchangeable. >>> >>> >>> In the example, the common interface is >>> >>> interface Role1&Role2 { >>> >>> inc(); >>> >>> } >>> >>> therefore >>> >>> if (x === y) { … x.foo(); x.inc(); y.inc(); z = y.bar() … } >>> >>> must be observationally equivalent to each of the following >>> >>> if (x === y) { … x.foo(); x.inc(); x.inc(); z = y.bar() … } >>> >>> if (x === y) { … x.foo(); y.inc(); y.inc(); z = y.bar() … } >>> >>> if (x === y) { … x.foo(); y.inc(); x.inc(); z = y.bar() … } >>> >>> >>> That is, sameness of x and y is reduced to the ability to observe >>> the same state changes through both x and y. Of course, limited to >>> the common interface. >>> >>> >>> The extreme case for the above f-example would arise if the >>> interfaces Role1 and Role2 were disjoint. In this case, no >>> transformation would be sanctioned from the knowledge that x === y. >>> >>> ~~~~~~ >>> >>> This observation leads me to a question about join: >>> >>> If only join is provided, but not EQ, then I don’t see how to >>> implement the function f above. If I successfully obtain z = >>> join(x, y), then it fulfills interface Role1&Role2, but I cannot >>> use it in lieu of x or y in the body of the conditional because it >>> does not implement foo() and bar(). >>> >>> If Role1&Role2 were empty, then the successful join would produce >>> a useless object. For example, in the Master/Slave example above, >>> it is highly likely that the interfaces are disjoint. >>> >>> >>> >>> Given a synchronous join: >>> >>> if (join(master, slave)) { >>> ... use master for mastery stuff, use slave for slavy stuff ... >>> } else { >>> ... do the more expensive thing ... >>> } >>> >>> Given the actual async join: >>> >>> Q(join(master, slave)).then(() => { >>> ... use master for mastery stuff, use slave for slavy stuff ... >>> }, () => { >>> ... do the more expensive thing ... >>> }); >>> >>> We're here using join only to test whether it succeeds, not to actually >>> use its result. Admittedly this is kludgy, but IMO no more kludgy than the >>> problem statement demands. This would certainly not be the typical case for >>> using join. >>> >>> >>> >>> >>> -- Cheers, >>> --MarkM >>> >>> >>> -Peter >>> >>> >>> >>> >>> >>> -- >>> Text by me above is hereby placed in the public domain >>> >>> Cheers, >>> --MarkM >> >> > > > > -- > Text by me above is hereby placed in the public domain > > Cheers, > --MarkM _______________________________________________ dev-tech-js-engine-internals mailing list dev-tech-js-engine-internals@lists.mozilla.org https://lists.mozilla.org/listinfo/dev-tech-js-engine-internals
