Upgrade to Pro — share decks privately, control downloads, hide ads and more …

Towards Language Support for Distributed Progra...

Towards Language Support for Distributed Programming

Heather Miller

November 09, 2018
Tweet

More Decks by Heather Miller

Other Decks in Programming

Transcript

  1. But it doesn’t always look that way from the outside…

    One thing I love about research is that research is very animated.
  2. This talk is about context Whirlwind tour of research on

    language support for distributed programming
  3. Language Support for Distributed Systems = ways that the programming

    language/ compiler can aid in the development of a distributed application
  4. Distributed Programming Research Today If I could visually depict all

    of the various research projects in the space of distributed programming… it’d look something like this! Context
  5. Distributed Programming Research Today Context Session Types Consistency & Programming

    Models Static Analysis & Verification Other research I’ll give a high-level overview of these
  6. Consistency? If I have a replica of an object/datum that

    can be updated by another node… What guarantees do I have about what all other nodes see? Specifically I mean programming models that provide some kind of consistency guarantee. Example scenario:
  7. Consistency? Example scenario: If I have a replica of an

    object/datum that can be updated by another node… What guarantees do I have about what all other nodes see? Specifically I mean programming models that provide some kind of consistency guarantee. Often a developer assumes that they want strong consistency (everyone can see the same state). But sometimes weak consistency is good enough (not every node needs to be in sync before computation can resume)
  8. the CAP theorem. Consistency? Specifically I mean programming models that

    provide some kind of consistency guarantee. In the past decade or so, thinking about controlling consistency by way of a programming model has come out of a famous impossibility result:
  9. the CAP theorem. A Consistency Availability C P Partition Tolerance

    (Linearizability) Quickly must state This has been broadly interpreted as: Pick two.
  10. Models that can enforce or tolerate weaker consistency Models like

    CRDTs choose sides. CRDTs (Conflict-free replicated data types.)
  11. Models that can enforce or tolerate weaker consistency Models like

    CRDTs choose sides. Such models sacrifice consistency in favor of availability. CRDTs (Conflict-free replicated data types.) (People like to call these AP) Think: Data structures that can be replicated over many nodes. When one node updates its replica, a CRDT guarantees that eventually all replicas will be eventually consistent.
  12. Models that can enforce or tolerate weaker consistency There has

    been effort to provide CRDTs as data types in functional languages that allow for composition. On the CRDTs+ programming model front…
  13. Models that choose other points in the design space There

    is also work experimenting with other edges of that triangle.
  14. Models that choose other points in the design space There

    is also work experimenting with other edges of that triangle. Meiklejohn’s work on Spry explores whether there’s other design points in the space, e.g., CA. “Spry is a programming model for building applications that want to tradeoff availability and consistency at varying points in application code to support application requirements.”
  15. Models that choose other points in the design space There

    is also work experimenting with other edges of that triangle. Meiklejohn’s work on Spry explores whether there’s other design points in the space, e.g., CA. “Spry is a programming model for building applications that want to tradeoff availability and consistency at varying points in application code to support application requirements.” Can add bounded staleness and freshness requirements via annotations!
  16. Mixed Consistency Answers the question of what if we want

    to choose from multiple consistency options in one application? Work from the distributed systems community takes a step: Correctables
  17. Mixed Consistency Answers the question of what if we want

    to choose from multiple consistency options in one application? • invokeWeak(operation) • invokeStrong(operation) • invoke(operation[, levels]) Give the user different APIs depending on the sort of consistency they’re after! Correctables They provide incremental consistency guarantees by capturing successive changes to the value of a replicated object. Applications can opt to receive a fast but possibly inconsistent result if eventual consistency is acceptable, or to wait for a strongly consistent result.
  18. Mixed Consistency Answers the question of what if we want

    to choose from multiple consistency options in one application? Work from the programming languages community takes a step: MixT
  19. What are they? Can be thought of as types for

    communication protocols That is, if a program type checks, then it’s guaranteed to follow the defined communication protocol.
  20. What are they? No hanging systems due to an accidental

    message send to the wrong service! Can be thought of as types for communication protocols That is, if a program type checks, then it’s guaranteed to follow the defined communication protocol. More concretely:
  21. What are they? No hanging systems due to an accidental

    message send to the wrong service! Can be thought of as types for communication protocols Binary & Multiparty Static & Dynamic That is, if a program type checks, then it’s guaranteed to follow the defined communication protocol. More concretely: Many variants of session types:
  22. What are they? Tiny example of implementing SMTP: SMTPClient =

    ⊕ { EHLO: !Domain.!FromAddress.!ToAddress.!Message.SMTPClient QUIT: end } great introduction to session types by Simon Fowler: http:/ /simonjf.com/2016/05/28/session-type-implementations.html Client side:
  23. What are they? Tiny example of implementing SMTP: SMTPClient =

    ⊕ { EHLO: !Domain.!FromAddress.!ToAddress.!Message.SMTPClient QUIT: end } great introduction to session types by Simon Fowler: http:/ /simonjf.com/2016/05/28/session-type-implementations.html Client side: means: select between the following two branches
  24. What are they? Tiny example of implementing SMTP: SMTPClient =

    ⊕ { EHLO: !Domain.!FromAddress.!ToAddress.!Message.SMTPClient QUIT: end } great introduction to session types by Simon Fowler: http:/ /simonjf.com/2016/05/28/session-type-implementations.html Client side: EHLO: send (!) domain, from address, to address, and the message. Repeat. means: select between the following two branches
  25. What are they? Tiny example of implementing SMTP: SMTPClient =

    ⊕ { EHLO: !Domain.!FromAddress.!ToAddress.!Message.SMTPClient QUIT: end } great introduction to session types by Simon Fowler: http:/ /simonjf.com/2016/05/28/session-type-implementations.html Client side: EHLO: send (!) domain, from address, to address, and the message. Repeat. QUIT: protocol is over. means: select between the following two branches
  26. What are they? SMTPClient = ⊕ { EHLO: !Domain.!FromAddress.!ToAddress.!Message.SMTPClient QUIT:

    end } SMTPServer = & { EHLO: ?Domain.?FromAddress.?ToAddress.?Message.SMTPServer QUIT: end } great introduction to session types by Simon Fowler: http:/ /simonjf.com/2016/05/28/session-type-implementations.html Tiny example of implementing SMTP: Client side: Server side:
  27. What are they? SMTPClient = ⊕ { EHLO: !Domain.!FromAddress.!ToAddress.!Message.SMTPClient QUIT:

    end } SMTPServer = & { EHLO: ?Domain.?FromAddress.?ToAddress.?Message.SMTPServer QUIT: end } great introduction to session types by Simon Fowler: http:/ /simonjf.com/2016/05/28/session-type-implementations.html Tiny example of implementing SMTP: Client side: Server side: means: offering a choice between the following two branches
  28. What are they? sig smtpClient : (SMTPClient, FromAddress, ToAddress, Message)

    ~> () fun smtpClient(c, from, to, msg) { var c1 = select EHLO c; var c2 = send(getDomain(from), c1); var c3 = send(from, c2); var c4 = send(to, c3); var c5 = send(message, c4) var c6 = select QUIT c5; close c6 } great introduction to session types by Simon Fowler: http:/ /simonjf.com/2016/05/28/session-type-implementations.html Tiny example of implementing SMTP: Implementation of the client: (Implemented in Links)
  29. Is this only theory? No! There are prototypes of session

    types implemented for many languages! C: Multiparty Session C (https://www.doc.ic.ac.uk/~cn06/sessionc/) Rust: session-types (https://github.com/Munksgaard/session-types) Erlang: monitored-session-erlang (https://github.com/SimonJF/monitored-session-erlang) Java: Scribble (https://www.doc.ic.ac.uk/~rhu/scribble/index.html) Scala: Ichannels (http://alcestes.github.io/lchannels/) Haskell: effect-sessions (https://www.doc.ic.ac.uk/~dorchard/popl16/) Python: SPY (https://www.doc.ic.ac.uk/~rn710/spy/)
  30. Still interested? If you want a friendly introduction, check out

    Simon Fowler’s blog article! http:/ /simonjf.com/ 2016/05/28/session-type- implementations.html Sam Lindley Phil Wadler Frank Pfenning
  31. Whip Lucas Waye, Stephen Chong, Christos Dimoulas Whip must… •

    …operate under partial deployment • …be transparent (don’t touch communication) • …be language agnostic • …should accommodate the loose coupling of modern services and be extensible with wire protocols.
  32. Paul Chiusano, Arya Irani, Rúnar Bjarnason Unison move computations around

    which are received and interpreted by the receiving node. Key idea: Functional Haskell-like language, where you can
  33. A bird’s eye view of a couple of our projects

    that we hope will move the needle.
  34. Ilya Sergey University College London Damien Zufferey Max Planck Institute

    for Software Systems Marc Shapiro Sorbonne- Université-LIP6 & Inria ! " # Alexy Gotsman IMDEA Software Institute$ Sebastian Burckhardt Microsoft Research % Tom Van Cutsem Nokia Bell Labs & Suresh Jagannathan Purdue University % Patrick Eugster University of Lugano ' James Cheney University of Edinburgh ! Wolfgang De Meuter Vrije Universiteit Brussel Tony Garnock-Jones University of Glasgow ! Other folks active in this space