Ken Birman Cornell University
The Next Challenges in Distributed Consistency
Building the Isis2 system forced us to lean heavily on formal methods: we needed a formal model capable of unifying virtual synchrony with state machine replication (Paxos), and the system itself relies upon this model in myriad ways. Thus, while the Isis2 model represents a powerful abstraction that the Isis2 user can leverage, it also turns out to be the cornerstone on which the entire system reposes. Yet much as building a compiler for programming language in that language can reveal limitations to a language, building Isis2 using virtual synchrony reveals the limited coverage of this kind of consistency model, and on the language-based tools we use to work with it. This talk will try to set the stage for LADA by reviewing Isis2 in a very brief way (of course, including 2-phase commit as one would code it in Isis2), then looking at the roles that the new dynamic membership model plays in Isis2, and finally at the question of why this model, by itself, doesn't solve the whole problem. We'll end by identifying some challenges for those interested in research that spans the border between programming languages and the class of distributed systems targeted by Isis2.
Leslie Lamport Micrsoft Research
Programming Languages are not the Answer
The question is: How can we create programs and other computer systems that do what they should?
Nancy Lynch MIT EECS and CSAIL
Timed I/O Automata: a Foundation for Languages for Distributed Algorithms
This talk will overview the Timed I/O Automata (TIOA) mathematical modeling framework developed by Kaynar, Lynch, Segala, and Vaandrager. The TIOA framework allows distributed algorithms and systems to be described in terms of infinite-state automata that perform discrete and continuous transitions, and that interact via external events. TIOA includes support for composition and levels of abstraction. It can express Zeno behavior, safety and liveness properties, rely-guarantee conditions, and more. The theory is presented in the monograph "The Theory of Timed I/O Automata (Second Edition)", published by Morgan Claypool in 2010.
The TIOA framework has been used to describe and analyze many distributed algorithms, network protocols, and hybrid systems. It has also been used to prove lower bound results.
In this talk, I will describe the theory in some detail. I will try to make the case that languages intended to describe and analyze distributed algorithms should use the TIOA framework as their mathematical foundation.
Michel Raynal Institut Universitaire de France and IRISA, Université de Rennes 1
Recursion in Distributed Shared-Memory Algorithms
Recursion is a fundamental concept of sequential computing that allows for the design of concise and elegant algorithms. Recently, a few recursive algorithms have been proposed in the context of distributed shared-memory systems. The talk visit some of them (mainly in the context of the renaming problem) and will try to exhibit the benefits of recursion for expressing distributed shared-memory algorithms.