Re: [TYPES] Types in distributed systems

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Behavioural types (of which session types are an instance) handle the 
scenario described in several ways, providing guarantees ranging from 
protocol compatibility to progress.

An European project (BETTY - www.behavioural-types.eu) is dedicated to 
the topic, and produced recently state-of-the-art reports covering the 
(huge!) bibliography on the subject. You can find them at 
http://www.behavioural-types.eu/publications.

Hope this helps.
antonio

On 29/08/14 03:24, "Ionuț G. Stan" wrote:
> [ The Types Forum,
> http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Hello,
>
> First, let me acknowledge upfront that I'm a complete dilettante when it
> comes to type theory (I'm still working through the first chapters of
> TaPL). That means that what I'm about to ask will be either stupid or
> extremely inexact. Nevertheless, I'm curious.
>
> Now, onto my question...
>
> The TL;DR version is: how does one specify types in a distributed
> programming model, like actors? And how much can we trust these types?
>
> I was debating today, on Twitter [1], how to type the sets of messages
> two actors can exchange; a producer (P) and a consumer (C).
>
> Let's say that the possible set of messages produced by P is M. We would
> like, by means of a type system, to know that C can handle: 1) just
> messages of type M and 2) all possible messages of type M.
>
> M could be represented by a sum type. Let's consider this particular one:
>
> M1 = A | B | C
>
> In a closed world this makes complete sense (to me, at least) and it's
> easy to verify statically. But in an open world setting, like a
> distributed system, where P and C are on different machines that may be
> upgraded separately, things look harder to me. You may guarantee
> statically that the two properties are met, but at runtime there may
> appear race conditions that violate the second property.
>
> For example, we deploy P1 and C1, both agreeing on M1. Next, we add a
> new variant to M1:
>
> M2 = A | B | C | D
>
> P1 and C1 are updated accordingly and we get P2 and C2, which we try to
> deploy, but a race condition appears and P2 send message D to C1.
> Obviously, C1 does not understand it. Even though the type system told
> us that C1 can handle all variants of M, it can't actually.
>
> A similar scenario appears when removing one of the variants of M1.
>
> Is there any typing approach to this kind of problem?
>
> It looks to me that types would have to include a version as well and
> all runtime communication between different versions should be
> prohibited by having versioned communication channels.
>
> Does anyone have any insights or pointers to articles, papers or books
> that discuss this sort of problem?
>
> Thank you for reading this!
>
>
> [1]: https://twitter.com/shajra/status/504568858967953408
>