synit
/
synit-manual
1
0
Fork 0
Code Issues 2 Pull Requests Projects Releases Wiki Activity

Incorporate more feedback from ccx in #syndicate

This commit is contained in:
Tony Garnock-Jones 2022-03-04 10:48:17 +01:00
parent 5a36a66e0a
commit d38e856629
1 changed files with 80 additions and 19 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

99
src/syndicated-actor-model.md
View File

@ -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)</span>
[Felleisen 1991]: #ref:felleisen-1991
[**Felleisen 1991**] <span id="ref: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)</span>
[Fischer et al 1985]: #ref:fischer-1985
[**Fischer et al 1985**] <span id="ref:fischer-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)</span>
[Garnock-Jones 2017]: #ref:garnock-jones-2017
[**Garnock-Jones 2017**] <span id="ref: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)</span>
[Morris 1968]: #ref:morris-1968
[**Morris 1968**] <span id="ref: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)</span>
[Stiegler and Tie 2010]: #ref:stiegler-2010
[**Stiegler and Tie 2010**] <span id="ref:stiegler-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.