[+thiemann, +joe.politz]
On Tue, Dec 3, 2013 at 7:18 AM, Mark Miller <erig...@gmail.com<https://mail.google.com/mail/?view=cm&fs=1&tf=1&to=erig...@gmail.com> > wrote: > Tom and I are in two overlapping conversation threads about the same > issue: Membranes vs Contracts vs Identity. If no one here objects soon, > I'll forward each thread so far to this joint thread and then reply on this > joint thread to all the addressees. > > This joining request will turn out to be ironically related to the subject > matter we're discussing ;). > First, the thread with Phil and Jeremy: Forwarded conversation Subject: Re: Membranes ------------------------ From: *Tom Van Cutsem* <tvcut...@vub.ac.be> Date: Wed, Nov 20, 2013 at 4:11 AM To: Philip Wadler <wad...@inf.ed.ac.uk> Cc: Jeremy Siek <js...@indiana.edu>, Mark Miller <erig...@gmail.com> [+MarkM] Hi Phil, Our use case for membranes so far has mostly been to enable revocation (i.e. the ability to revoke access of all object references that cross the membrane), so we only had a single kind of wrapper. However, I would claim that if you have two kinds of wrappers, one specialized as Int->Int and the other as String->String, for the same function, then those two wrappers should in fact not be identity-equal, as they may have observably different behavior when called. Our litmus test for object-identity is as follows: if (x === y) { // === is JavaScript's object-identity comparator // inside this branch, we should be able to substitute x for y without any observable difference } If you have two type specializations for the same function, and you bind one to x and the other to y, they shoudn't be identity-equal as demonstrated by the above code. Perhaps Mark has other insights on how to resolve this issue, if it can be resolved at all. Best regards, Tom > Tom, > > Thanks again for organising SCRIPT, and for explaining to me about membranes. > > It occurs to me that there may still be an issue with using membranes to ensure that adding wrappers does not change the result of tests for object identity. Imagine that a single JavaScript function of type Any->Any is exported from a module in two places, once specialised to type Int->Int and once specialised to type String->String. This will require two distinct wrappers, and so even using membranes the object identity relation of the original will be lost. I can't see a way around this corner case, but I wonder whether you and Mark had thought about it? > > Yours, -- P > > -- > .\ Philip Wadler, Professor of Theoretical Computer Science > ./\ School of Informatics, University of Edinburgh > / \ http://homepages.inf.ed.ac.uk/wadler/ > The University of Edinburgh is a charitable body, registered in > Scotland, with registration number SC005336. ---------- From: *Philip Wadler* <wad...@inf.ed.ac.uk> Date: Wed, Nov 20, 2013 at 5:07 AM To: Tom Van Cutsem <tvcut...@vub.ac.be> Cc: Jeremy Siek <js...@indiana.edu>, Mark Miller <erig...@gmail.com> Thanks. I agree that there is an argument for treating the two wrappers as distinct, but I have a reason for wanting to treat them the same. I'd like wrapping to satisfy the following guarantee: adding wrappers can cause a program to fail more often, but never to change the answer. Since in the unwrapped program the unwrapped values are the same object, the wrapped ones must be as well in order to preserve the guarantee. Yours, -- P The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ---------- From: *Jeremy Siek* <js...@indiana.edu> Date: Wed, Nov 20, 2013 at 6:21 AM To: Philip Wadler <wad...@inf.ed.ac.uk> Cc: Tom Van Cutsem <tvcut...@vub.ac.be>, Mark Miller <erig...@gmail.com> On Nov 20, 2013, at 8:07 AM, Philip Wadler <wad...@inf.ed.ac.uk> wrote: Thanks. I agree that there is an argument for treating the two wrappers as distinct, but I have a reason for wanting to treat them the same. I'd like wrapping to satisfy the following guarantee: adding wrappers can cause a program to fail more often, but never to change the answer. Since in the unwrapped program the unwrapped values are the same object, the wrapped ones must be as well in order to preserve the guarantee. Yours, -- P On 20 November 2013 12:11, Tom Van Cutsem <tvcut...@vub.ac.be> wrote: > [+MarkM] > > Hi Phil, > > Our use case for membranes so far has mostly been to enable revocation > (i.e. the ability to revoke access of all object references that cross the > membrane), so we only had a single kind of wrapper. > > However, I would claim that if you have two kinds of wrappers, one > specialized as Int->Int and the other as String->String, for the same > function, then those two wrappers should in fact not be identity-equal, as > they may have observably different behavior when called. > > Our litmus test for object-identity is as follows: > > if (x === y) { // === is JavaScript's object-identity comparator > // inside this branch, we should be able to substitute x for y without > any observable difference > } > > This is a good point, though let's look at a related situation that may help make what Phil is saying above more concrete: one wrapper is Int->Any and the other is Any->Int and the underlying function is really of type Int->Int or at least acts that way. In such a case I wonder if there are any observable differences. If you have two type specializations for the same function, and you bind > one to x and the other to y, they shoudn't be identity-equal as > demonstrated by the above code. > > Perhaps Mark has other insights on how to resolve this issue, if it can be > resolved at all. > > Best regards, > Tom > > > Tom, > > > > Thanks again for organising SCRIPT, and for explaining to me about > membranes. > > > > It occurs to me that there may still be an issue with using membranes to > ensure that adding wrappers does not change the result of tests for object > identity. Imagine that a single JavaScript function of type Any->Any is > exported from a module in two places, once specialised to type Int->Int and > once specialised to type String->String. This will require two distinct > wrappers, and so even using membranes the object identity relation of the > original will be lost. I can't see a way around this corner case, but I > wonder whether you and Mark had thought about it? > > > > Yours, -- P > > > > -- > > .\ Philip Wadler, Professor of Theoretical Computer Science > > ./\ School of Informatics, University of Edinburgh > > / \ http://homepages.inf.ed.ac.uk/wadler/ > > The University of Edinburgh is a charitable body, registered in > > Scotland, with registration number SC005336. > > -- .\ Philip Wadler, Professor of Theoretical Computer Science ./\ School of Informatics, University of Edinburgh / \ http://homepages.inf.ed.ac.uk/wadler/ The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. __________________________________________ Jeremy G. Siek <js...@indiana.edu> Associate Professor School of Informatics and Computing Indiana University Bloomington http://homes.soic.indiana.edu/jsiek/ ---------- From: *Mark Miller* <erig...@gmail.com> Date: Wed, Nov 20, 2013 at 8:20 AM To: Jeremy Siek <js...@indiana.edu>, Philip Wadler <wad...@inf.ed.ac.uk>, Tom Van Cutsem <tvcut...@vub.ac.be> Cc: Shriram Krishnamurthi <shri...@gmail.com> [+shriram] When Shriram (cc'ed) first brought to my attention the similarities between membranes and higher-order contracts, I worried about exactly this issue. Except for this issue, it seems like membranes and higher-order contracts should be reconcilable -- that there should be some more general reusable abstraction that can serve both of these purposes. However, given conventional object identity, I think this discrepancy is fundamental. Higher-order contracts requires that the wrapper impose restrictions based on the path from the root by which the wrapped value is reached. Membranes, in order to preserve identity, require that two wrappings of the same value are the same wrapper, independent of the path. OTOH, in a system using only join, not EQ, as its identity/equality primitive, these tensions are reconcilable. By EQ, I mean this interchangeability that Tom explains. By contrast, the E and Dr. SES join operation var z = join(x, y); says that z should designate the object that both x and y designate. In E and Dr. SES we introduced join to deal with asynchrony -- z is a promise for the object that x and y will both eventually designate. If x and y both eventually designate the "same" object, then z will designate that object as well, and messages sent to z will be delivered to that object. If x and y eventually designate known-different objects, z will eventually become a broken (in E terminology) or a rejected (in Dr. SES terminology) promise, and no messages sent to z will ever be delivered. Of course, this is circular so far, as we haven't yet said what we mean by "same". This is subtler than it seems, since we want a meaning of "same" that avoids some of the problems of EQ. The three things to look at are < http://erights.org/elib/equality/grant-matcher/>, the use of join in figure 3 of <http://research.google.com/pubs/pub40673.html> together with the explanation of the security purpose it serves, and the partition and ordering properties of join in section 19.5 / figure 19.3 of < http://erights.org/talks/thesis/markm-thesis.pdf>. Applied to higher-order contracts, this implies that an operation on z should succeed only when it would succeed on both x and y, and mean the same thing as it would if the operation had been performed on either one. In other words, it should impose the conjunction of the restrictions accumulated by x's path and by y's path. For local JS, SES, Caja, and varieties of Scheme (including Racket), all of this is too late, as they are stuck needing to support a local EQ operation. However, for the distributed portion of Dr. SES it would be fine, and would therefore be fine for higher-order contracts that coincide with an asynchrony barrier. It would also be fine for new languages without any equality primitive stronger than join even in the local synchronous case. In the same way that join would need to be in bed with such contract-membranes above, in order to get a similar effect in Horton < https://www.usenix.org/legacy/event/hotsec07/tech/full_papers/miller/miller.pdf>, join would need to be in bed with the system of such responsibility-membranes. The mailkeys-like reconstruction of Horton at < http://www.erights.org/elib/capability/horton/mailkeys.html> is probably a better starting point than Horton itself for this join integration. Possible slogan: Intersect restrictions and union responsibilities. -- Text by me above is hereby placed in the public domain Cheers, --MarkM ---------- From: *Tom Van Cutsem* <tvcut...@vub.ac.be> Date: Wed, Nov 20, 2013 at 8:34 AM To: Mark Miller <erig...@gmail.com> Cc: Jeremy Siek <js...@indiana.edu>, Philip Wadler <wad...@inf.ed.ac.uk>, Shriram Krishnamurthi <shri...@gmail.com> Mark, Thanks for the elaborate explanation and the pointers. I believe the essence of your argument, applied to Phil's work, is that conventional EQ is not the right primitive, and we need another comparison operator (join) that is aware of intermediary wrappers. This reminds me that Racket provides an (impersonator-of? v1 v2) primitive, which tests whether v1 and v2 are EQ *modulo contract wrappers*. Presumably, in a language with wrappers that enforce gradual typing, this is the right comparison operator to include. Regards, Tom ---------- From: *Mark Miller* <erig...@gmail.com> Date: Wed, Nov 20, 2013 at 8:41 AM To: Tom Van Cutsem <tvcut...@vub.ac.be> Cc: Jeremy Siek <js...@indiana.edu>, Philip Wadler <wad...@inf.ed.ac.uk>, Shriram Krishnamurthi <shri...@gmail.com> Yeah, I should look into "impersonator-of?". This could be used to build join if the restrictions could also be extracted and conjoined. But by itself "impersonator-of?" isn't a useful equality operator, as its two operands are still asymmetric and it does not produce or reveal a symmetric value. ---------- From: *Mark Miller* <erig...@gmail.com> Date: Wed, Nov 20, 2013 at 8:53 AM To: Jeremy Siek <js...@indiana.edu>, Philip Wadler <wad...@inf.ed.ac.uk>, Tom Van Cutsem <tvcut...@vub.ac.be> Cc: Shriram Krishnamurthi <shri...@gmail.com> On Wed, Nov 20, 2013 at 8:20 AM, Mark Miller <erig...@gmail.com> wrote: > [+shriram] > > When Shriram (cc'ed) first brought to my attention the similarities > between membranes and higher-order contracts, I worried about exactly this > issue. Except for this issue, it seems like membranes and higher-order > contracts should be reconcilable -- that there should be some more general > reusable abstraction that can serve both of these purposes. However, given > conventional object identity, I think this discrepancy is fundamental. > Higher-order contracts requires that the wrapper impose restrictions based > on the path from the root by which the wrapped value is reached. Membranes, > in order to preserve identity, require that two wrappings of the same value > are the same wrapper, independent of the path. > > OTOH, in a system using only join, not EQ, as its identity/equality > primitive, these tensions are reconcilable. By EQ, I mean this > interchangeability that Tom explains. By contrast, the E and Dr. SES join > operation > > var z = join(x, y); > > says that z should designate the object that both x and y designate. In E > and Dr. SES we introduced join to deal with asynchrony -- z is a promise > for the object that x and y will both eventually designate. If x and y both > eventually designate the "same" object, then z will designate that object > as well, and messages sent to z will be delivered to that object. If x and > y eventually designate known-different objects, z will eventually become a > broken (in E terminology) or a rejected (in Dr. SES terminology) promise, > and no messages sent to z will ever be delivered. > > Of course, this is circular so far, as we haven't yet said what we mean by > "same". This is subtler than it seems, since we want a meaning of "same" > that avoids some of the problems of EQ. The three things to look at are < > http://erights.org/elib/equality/grant-matcher/>, the use of join in > figure 3 of <http://research.google.com/pubs/pub40673.html> together with > the explanation of the security purpose it serves, > That should be Figure 2. ---------- From: *Mark Miller* <erig...@gmail.com> Date: Wed, Nov 20, 2013 at 8:59 AM To: Jeremy Siek <js...@indiana.edu>, Philip Wadler <wad...@inf.ed.ac.uk>, Tom Van Cutsem <tvcut...@vub.ac.be> Cc: Shriram Krishnamurthi <shri...@gmail.com> On Wed, Nov 20, 2013 at 8:20 AM, Mark Miller <erig...@gmail.com> wrote: > [+shriram] > > When Shriram (cc'ed) first brought to my attention the similarities > between membranes and higher-order contracts, I worried about exactly this > issue. Except for this issue, it seems like membranes and higher-order > contracts should be reconcilable -- that there should be some more general > reusable abstraction that can serve both of these purposes. However, given > conventional object identity, I think this discrepancy is fundamental. > Higher-order contracts requires that the wrapper impose restrictions based > on the path from the root by which the wrapped value is reached. Membranes, > in order to preserve identity, require that two wrappings of the same value > are the same wrapper, independent of the path. > > OTOH, in a system using only join, not EQ, as its identity/equality > primitive, these tensions are reconcilable. By EQ, I mean this > interchangeability that Tom explains. By contrast, the E and Dr. SES join > operation > > var z = join(x, y); > > says that z should designate the object that both x and y designate. In E > and Dr. SES we introduced join to deal with asynchrony -- z is a promise > for the object that x and y will both eventually designate. If x and y both > eventually designate the "same" object, then z will designate that object > as well, and messages sent to z will be delivered to that object. If x and > y eventually designate known-different objects, z will eventually become a > broken (in E terminology) or a rejected (in Dr. SES terminology) promise, > and no messages sent to z will ever be delivered. > > Of course, this is circular so far, as we haven't yet said what we mean by > "same". This is subtler than it seems, since we want a meaning of "same" > that avoids some of the problems of EQ. The three things to look at are < > http://erights.org/elib/equality/grant-matcher/>, the use of join in > figure 3 of <http://research.google.com/pubs/pub40673.html> together with > the explanation of the security purpose it serves, and the partition and > ordering properties of join in section 19.5 / figure 19.3 of < > http://erights.org/talks/thesis/markm-thesis.pdf>. Applied to > higher-order contracts, this implies that an operation on z should succeed > only when it would succeed on both x and y, and mean the same thing as it > would if the operation had been performed on either one. In other words, it > should impose the conjunction of the restrictions accumulated by x's path > and by y's path. > > For local JS, SES, Caja, and varieties of Scheme (including Racket), all > of this is too late, as they are stuck needing to support a local EQ > operation. However, for the distributed portion of Dr. SES it would be > fine, and would therefore be fine for higher-order contracts that coincide > with an asynchrony barrier. It would also be fine for new languages without > any equality primitive stronger than join even in the local synchronous > case. > > In the same way that join would need to be in bed with such > contract-membranes above, in order to get a similar effect in Horton < > https://www.usenix.org/legacy/event/hotsec07/tech/full_papers/miller/miller.pdf>, > join would need to be in bed with the system of such > responsibility-membranes. The mailkeys-like reconstruction of Horton at < > http://www.erights.org/elib/capability/horton/mailkeys.html> is probably > a better starting point than Horton itself for this join integration. > Possible slogan: Intersect restrictions and union responsibilities. > Conjoining restrictions intersects authority, making for the more elegant slogan Intersect authority, union responsibility. I have a nagging intuition that authority and responsibility are in some sense duals. This adds to that nagging feeling ;). I am also unsure of the relationship between "responsibility" and "blame". ---------- From: *Shriram Krishnamurthi* <shri...@gmail.com> Date: Wed, Nov 20, 2013 at 6:28 PM To: Mark Miller <erig...@gmail.com> Cc: Jeremy Siek <js...@indiana.edu>, Philip Wadler <wad...@inf.ed.ac.uk>, Tom Van Cutsem <tvcut...@vub.ac.be> For what it's worth, Pyret does _not_ offer a generalized EQ operator, and precisely so that we can support contracts, capabilities, and the like without having to pile (mis-)feature on top of (mis-)feature. For now we have gone with the decision that a particular datatype can choose to offer an EQ, but this is not a decision we're wedded to either. Shriram ---------- From: *Mark Miller* <erig...@gmail.com> Date: Wed, Nov 20, 2013 at 9:22 PM To: Shriram Krishnamurthi <s...@cs.brown.edu> Cc: Jeremy Siek <js...@indiana.edu>, Philip Wadler <wad...@inf.ed.ac.uk>, Tom Van Cutsem <tvcut...@vub.ac.be> How about join? -- Text by me above is hereby placed in the public domain Cheers, --MarkM ---------- From: *Philip Wadler* <wad...@inf.ed.ac.uk> Date: Thu, Nov 21, 2013 at 2:41 AM To: Mark Miller <erig...@gmail.com> Cc: Jeremy Siek <js...@indiana.edu>, Tom Van Cutsem <tvcut...@vub.ac.be>, Shriram Krishnamurthi <shri...@gmail.com> Thanks, Mark, this is very interesting. Just to recap, the question of interest to me is whether we can offer the following guarantee: adding contracts to a system may make it fail more often, but never changes a non-fail result. There are two contexts in which we can ask this question: (1) Can we provide such a guarantee for a JavaScript contract system? (2) Can we design a future system in such a way that it is possible to provide such a guarantee? The answer to (1) appears to be 'Sorry, you are SOL' (to use a technical term). The reason for this is not the existence of EQ, but the desire to use EQ to enforce security policies, which requires that proxies cannot redefine EQ. The answer to (2) appears to be 'Yes, this is possible', because adding a contract may cause join to fail, but not to return a different answer. Of course, in either case for this to work it must not be possible to write code that catches a failure and turns it into an answer. Does JavaScript (or Dr SES, or Pyret) support exceptions that cannot be caught? Yours, -- P . \ Philip Wadler, Professor of Theoretical Computer Science . /\ School of Informatics, University of Edinburgh . / \ http://homepages.inf.ed.ac.uk/wadler/ The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ---------- From: *Mark Miller* <erig...@gmail.com> Date: Thu, Nov 21, 2013 at 8:22 AM To: Philip Wadler <wad...@inf.ed.ac.uk> Cc: Jeremy Siek <js...@indiana.edu>, Tom Van Cutsem <tvcut...@vub.ac.be>, Shriram Krishnamurthi <shri...@gmail.com> On Thu, Nov 21, 2013 at 2:41 AM, Philip Wadler <wad...@inf.ed.ac.uk<https://mail.google.com/mail/?view=cm&fs=1&tf=1&to=wad...@inf.ed.ac.uk> > wrote: > Thanks, Mark, this is very interesting. > > Just to recap, the question of interest to me is whether we can offer the > following guarantee: adding contracts to a system may make it fail more > often, but never changes a non-fail result. There are two contexts in which > we can ask this question: (1) Can we provide such a guarantee for a > JavaScript contract system? (2) Can we design a future system in such a way > that it is possible to provide such a guarantee? > > The answer to (1) appears to be 'Sorry, you are SOL' (to use a technical > term). The reason for this is not the existence of EQ, but the desire to > use EQ to enforce security policies, which requires that proxies cannot > redefine EQ. > I don't think this is quite right. I agree that the answer is SOL, but it is because of the existence of EQ and the desire to preserve the semantics of EQ. Even if we weren't concerned about security policies per se, I think it would damage the language for EQ(x,y) to stop implying that x and y are indistinguishable and substitutable. > > The answer to (2) appears to be 'Yes, this is possible', because adding a > contract may cause join to fail, but not to return a different answer. > If join is independent of the contract-membrane system, then your description is accurate -- it would be the join that fails. But if join is in bed with the contract-membrane system in the way I suggest, then we do even better. If we join two different contract wrappers of the same target, then the join itself succeeds, but produces a wrapper that fails on individual operations whenever either of the original wrappers would have failed. > > Of course, in either case for this to work it must not be possible to > write code that catches a failure and turns it into an answer. Does > JavaScript (or Dr SES, or Pyret) support exceptions that cannot be caught? > In a connected world, an exception that cannot be caught in any sense requires the destruction of the universe. I doubt that is really what you want ;). JavaScript does not support exceptions that are not conventionally catchable. E and Dr.SES have vat creation and preemptive vat destruction, but differing failure models. In E, a vat destroying itself is much like an Erlang process abort -- no code within the vat executes after the destruction, so there's no conventional notion of "caught". However, counter-party vats can sense the partition between themselves and the destroyed vat, enabling them to react to its absence. Since a distributed system must already be prepared for partial failure, E maps not-conventionally-catchable exceptional conditions to destruction of that part of the universe, triggering the means by which counter-parties already cope with partial failure. By contrast, Dr.SES is build on NodeKen and thus the *Ken failure model. E makes partition apparent and encourages vats to cope, and to recover distributed consistency in an application dependent manner. *Ken masks partition, making partition equivalent to a slow network. A crashed process is equivalent to a slow one. Generally, a destroyed process is equivalent to an infinitely slow one. As a result, *Ken applications, including Dr.SES ones, are not expected in general to have their own application dependent logic for reacting to the unavailability or destruction of a counter-party. Dr.SES application code can of course have timeout logic to react to slowness, but this is problematic as the sole basis to deal with destruction or self-destruction of a counter-party. ---------- From: *Philip Wadler* <wad...@inf.ed.ac.uk> Date: Thu, Nov 21, 2013 at 9:40 AM To: Mark Miller <erig...@gmail.com> Cc: Jeremy Siek <js...@indiana.edu>, Tom Van Cutsem <tvcut...@vub.ac.be>, Shriram Krishnamurthi <shri...@gmail.com> On 21 November 2013 16:22, Mark Miller <erig...@gmail.com> wrote: > On Thu, Nov 21, 2013 at 2:41 AM, Philip Wadler > <wad...@inf.ed.ac.uk<https://mail.google.com/mail/?view=cm&fs=1&tf=1&to=wad...@inf.ed.ac.uk> > > wrote: > >> Thanks, Mark, this is very interesting. >> >> Just to recap, the question of interest to me is whether we can offer the >> following guarantee: adding contracts to a system may make it fail more >> often, but never changes a non-fail result. There are two contexts in which >> we can ask this question: (1) Can we provide such a guarantee for a >> JavaScript contract system? (2) Can we design a future system in such a way >> that it is possible to provide such a guarantee? >> >> The answer to (1) appears to be 'Sorry, you are SOL' (to use a technical >> term). The reason for this is not the existence of EQ, but the desire to >> use EQ to enforce security policies, which requires that proxies cannot >> redefine EQ. >> > > I don't think this is quite right. I agree that the answer is SOL, but it > is because of the existence of EQ and the desire to preserve the semantics > of EQ. Even if we weren't concerned about security policies per se, I think > it would damage the language for EQ(x,y) to stop implying that x and y are > indistinguishable and substitutable. > Fair point. I took your security concerns as the main reason why proxies do not permit EQ to be redefined, but there are other reasons. > >> The answer to (2) appears to be 'Yes, this is possible', because adding a >> contract may cause join to fail, but not to return a different answer. >> > > If join is independent of the contract-membrane system, then your > description is accurate -- it would be the join that fails. But if join is > in bed with the contract-membrane system in the way I suggest, then we do > even better. If we join two different contract wrappers of the same target, > then the join itself succeeds, but produces a wrapper that fails on > individual operations whenever either of the original wrappers would have > failed. > Yes, good point. Unclear to me whether or not 'intersect authority' is what is wanted here, but it might be. > > Of course, in either case for this to work it must not be possible to > write code that catches a failure and turns it into an answer. Does > JavaScript (or Dr SES, or Pyret) support exceptions that cannot be caught? > > In a connected world, an exception that cannot be caught in any sense > requires the destruction of the universe. I doubt that is really what you > want ;). > Right. The desire to guarantee that wrappers only introduce failure is in tension with the need to recover from failure. > > JavaScript does not support exceptions that are not conventionally > catchable. E and Dr.SES have vat creation and preemptive vat destruction, > but differing failure models. In E, a vat destroying itself is much like an > Erlang process abort -- no code within the vat executes after the > destruction, so there's no conventional notion of "caught". However, > counter-party vats can sense the partition between themselves and the > destroyed vat, enabling them to react to its absence. Since a distributed > system must already be prepared for partial failure, E maps > not-conventionally-catchable exceptional conditions to destruction of that > part of the universe, triggering the means by which counter-parties already > cope with partial failure. > In short: one may ensure that the wrapped code fails, leaving capture of the failure to surrounding code. That preserves the guarantee while still providing recovery. Yay! > > By contrast, Dr.SES is build on NodeKen and thus the *Ken failure model. E > makes partition apparent and encourages vats to cope, and to recover > distributed consistency in an application dependent manner. *Ken masks > partition, making partition equivalent to a slow network. A crashed process > is equivalent to a slow one. Generally, a destroyed process is equivalent > to an infinitely slow one. As a result, *Ken applications, including Dr.SES > ones, are not expected in general to have their own application dependent > logic for reacting to the unavailability or destruction of a counter-party. > Dr.SES application code can of course have timeout logic to react to > slowness, but this is problematic as the sole basis to deal with > destruction or self-destruction of a counter-party. > This would work if the timeout was caught by a monitoring process, but could lead to a changed answer if the timeout was caught be the process we are attempting to guarantee never changes its answer. Yours, -- P -- .\ Philip Wadler, Professor of Theoretical Computer Science ./\ School of Informatics, University of Edinburgh / \ http://homepages.inf.ed.ac.uk/wadler/ The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. _______________________________________________ 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
