diff --git a/src/syndicated-actor-model.md b/src/syndicated-actor-model.md index e76fe3a..1eea74c 100644 --- a/src/syndicated-actor-model.md +++ b/src/syndicated-actor-model.md @@ -203,33 +203,39 @@ according to actors' interests. *allSubscribers* ← **new** Set() **on** assertion of semi-structured datum *a*, add *a* to *allAssertions* - if *a* matches Observe(*pattern*, *subscriberRef*), - add (*pattern*, *subscriberRef*) to *allSubscribers* - for *x* in *allAssertions*, if *x* matches *pattern*, - **assert** *x* at *subscriberRef* - otherwise, - for (*p*, *s*) in *allSubscribers*, if *a* matches *p*, - **assert** *a* at *s* + if *a* appears exactly once now in *allAssertions*, + if *a* matches Observe(*pattern*, *subscriberRef*), + add (*pattern*, *subscriberRef*) to *allSubscribers* + for *x* in *allAssertions*, if *x* matches *pattern*, + **assert** *x* at *subscriberRef* + otherwise, + for (*p*, *s*) in *allSubscribers*, if *a* matches *p*, + **assert** *a* at *s* **on** retraction of previously-asserted *a*, - retract *a* from all subscribers to whom it was forwarded remove *a* from *allAssertions* - if *a* matches Observe(*pattern*, *subscriberRef*), - remove (*pattern*, *subscriberRef*) from *allSubscribers* - retract all assertions previously sent to *subscriberRef* + if *a* no longer appears at all in *allAssertions*, + retract *a* from all subscribers to whom it was forwarded + if *a* matches Observe(*pattern*, *subscriberRef*), + remove (*pattern*, *subscriberRef*) from *allSubscribers* + retract all assertions previously sent to *subscriberRef* ``` Assertions sent to a dataspace are routed by pattern-matching. Subscriptions—tuples associating a pattern with a subscriber entity—are placed in the dataspace as assertions like any other. A dataspace entity behaves very similarly to a tuplespace [[Gelernter and Carriero 1992][]]. -One key difference is that tuples in a tuplespace are "generative" [[Gelernter 1985][]], taking -on independent existence once created and potentially remaining in a tuplespace indefinitely; -SAM assertions, by contrast, never outlive their asserting actors. +However, there are two key differences. -Assertions placed at a dataspace only exist as long as they are actively maintained: if an -actor terminates or crashes, *all* its assertions are withdrawn, including those targeted at a -dataspace entity. The dataspace, following its definition, forwards all withdrawals on to -interested subscribers. +The first is that, while tuples in a tuplespace are "generative" [[Gelernter 1985][]], taking +on independent existence once created and potentially remaining in a tuplespace indefinitely, +SAM assertions never outlive their asserting actors. This means that assertions placed at a +dataspace only exist as long as they are actively maintained. If an actor terminates or +crashes, *all* its assertions are withdrawn, including those targeted at a dataspace entity. +The dataspace, following its definition, forwards all withdrawals on to interested subscribers. + +The second is that assertion of a value is idempotent: multiple assertions of the same +value[^entity-reference-equivalence] appear to observers indistinguishable from a single +assertion. In other words, assertions at a dataspace are deduplicated. ### Applications of dataspaces @@ -348,6 +354,13 @@ If the service crashes before replying, the client's request remains outstanding supervisor [[Armstrong 2003][], section 4.3.2] can reset the modem and start a fresh service instance. The client remains blissfully unaware that anything untoward happened. +We may also consider a variation where the client wishes to retract or modify its request in +case of service crash. To do this, the client must pay more attention to the [conversational +frame](https://syndicate-lang.org/tonyg-dissertation/html/#x_2_2_0_0_1) of its interaction with +the server. In the pseudocode above, no explicit service discovery step is used, but the client +could reason about the server's lifecycle by observing the (disappearance of) presence of the +server's subscription to requests: Observe(⌜Observe(⌜Request(⌞_⌟, ⌞_⌟)⌝, _)⌝, ...). + ## Object-capabilities for access control [Object capabilities](https://en.wikipedia.org/wiki/Object-capability_model) are the only @@ -373,7 +386,7 @@ In the SAM, a capability is a triple of An "attenuation" is a piece of syntax including patterns over semi-structured data. When an assertion or message is directed to the underlying entity by way of an attenuated capability, the asserted value or message body is checked against the patterns in the attenuation. Values -not matching are discarded silently. +not matching are discarded silently.[^silent-discard] **Restricting method calls.** For example, a reference to the dataspace where our cellular modem server example is running could be attenuated to only allow assertions of the form @@ -421,6 +434,19 @@ Wolfgang De Meuter. “43 Years of Actors: A Taxonomy of Actor Models and Their In Proc. AGERE. Amsterdam, The Netherlands, 2016. [[DOI (PDF available)]](https://doi.org/10.1145/3001886.3001890) +[Felleisen 1991]: #ref:felleisen-1991 +[**Felleisen 1991**] Felleisen, Matthias. “On the Expressive +Power of Programming Languages.” Science of Computer Programming 17, no. 1–3 (1991): 35–75. +[[DOI (PDF available)]](https://doi.org/10.1016/0167-6423(91)90036-W) +[[PS]](https://www2.ccs.neu.edu/racket/pubs/scp91-felleisen.ps.gz) + +[Fischer et al 1985]: #ref:fischer-1985 +[**Fischer et al 1985**] Fischer, Michael J., Nancy A. Lynch, and +Michael S. Paterson. “Impossibility of Distributed Consensus with One Faulty Process.” Journal +of the ACM 32, no. 2 (April 1985): 374–382. [[DOI (PDF +available)]](https://doi.org/10.1145/3149.214121) +[[PDF]](https://groups.csail.mit.edu/tds/papers/Lynch/jacm85.pdf) + [Garnock-Jones 2017]: #ref:garnock-jones-2017 [**Garnock-Jones 2017**] Garnock-Jones, Tony. “Conversational Concurrency.” PhD, Northeastern University, 2017. @@ -453,6 +479,11 @@ Environment.” In IEEE Aerospace Conference. Big Sky, Montana, 2009. Unified Approach to Access Control and Concurrency Control.” PhD, Johns Hopkins University, 2006. [[PDF]](http://www.erights.org/talks/thesis/markm-thesis.pdf) +[Morris 1968]: #ref:morris-1968 +[**Morris 1968**] Morris, James Hiram, Jr. “Lambda-Calculus Models +of Programming Languages.” PhD thesis, Massachusetts Institute of Technology, 1968. [[Available +online]](http://hdl.handle.net/1721.1/64850) + [Stiegler and Tie 2010]: #ref:stiegler-2010 [**Stiegler and Tie 2010**] Stiegler, Marc, and Jing Tie. “Introduction to Waterken Programming.” Technical Report. Hewlett-Packard Labs, August 6, 2010. @@ -503,6 +534,17 @@ USENIX Annual Technical Conference. Boston, Massachusetts, 2012. [2017 dissertation][Garnock-Jones 2017] ([direct link to relevant section of online text](https://syndicate-lang.org/tonyg-dissertation/html/#sec:RPC)). +[^entity-reference-equivalence]: Here the thorny question of the equivalence of entity + references rears its head. Preserves specifies an equivalence over its `Value`s that is + generic in the equivalence over embedded values such as entity references. The ideal + equivalence here would be *observational equivalence* [[Morris 1968][], [Felleisen + 1991][]]: two references are the same when they react indistinguishably to assertions and + messages. However, this isn't something that can be practically implemented except in + relatively limited circumstances. Fortunately, in most cases, *pointer equivalence* of + entity references is good enough to work with, and that's what I've implemented to date + (modulo details such as structural comparison of attenuations attached to a reference + etc.). + [^background-on-interests]: For more on assertions of interest, see [here](https://syndicate-lang.org/about/#conversational-frames-conversational-knowledge) and [here](https://syndicate-lang.org/tonyg-dissertation/html/#x_2_2_0_0_8). @@ -511,3 +553,22 @@ USENIX Annual Technical Conference. Boston, Massachusetts, 2012. claim along with a worked example of object-capabilities in a personal-computing setting. The capabilities are ordinary E-style capabilities rather than SAM-style capabilities, but the conclusions hold. + +[^silent-discard]: You might be wondering "why *silent* discard of assertions rejected by an + attenuation filter?", or more generally, "why discard assertions and messages silently on + any kind of failure?" The answer is related to the famous *Fischer/Lynch/Paterson (FLP) + result* [[Fischer et al 1985][]], where one cannot distinguish between a failed process or + a slow process. By extending the reasoning to a process that simply ignores some or all of + its inputs, we see that offering any kind of response *at the SAM level* in case of failure + or rejection would be a false comfort, because nothing would prevent successful delivery of + a message to a recipient which then simply discards it. Instead, processes have to agree + ahead of time on the [conversational + frame](https://syndicate-lang.org/tonyg-dissertation/html/#x_2_2_0_0_1) in which they will + communicate. The SAM encourages a programming style where assertions are used to set up a + conversational frame, and then other interactions happen in the context of the information + carried in those assertions; see the section where we [revisit the cellular modem + server](#cellular-modem-server-with-a-dataspace) with the components decoupled and placed + in a conversational frame by addition of a dataspace to the system. Finally, and with all + this said, *debugging-level* notifications of rejected or discarded messages have their + place: it's just the SAM itself that does not include feedback of this kind. Implementions + are encouraged to offer such aids to debugging.