[Dr. TLA+ Series] Global Snapshot - Rustan Leino
Cheng Huang
Dr. TLA+ Series - Global Snapshot (K. Rustan M. Leino)
Time
September 23, 2016 - 10-11:30am PDT
Location
Microsoft Building 99, Research Lecture Room B (99/1927)
- 14820 NE 36th St, Redmond, WA 98052
Abstract
A snapshot of the state of a running program is useful in several ways. For example, it can serve as a check point from which to restart the execution, in case the rest of the execution fails in some way. Another example use of a snapshot is to detect that some stable condition, such as a deadlock, has occurred. This lecture will discuss algorithms for capturing a global snapshot of a distributed, asynchronous system. It will focus on writing a formal specification of such algorithms.
If you want to do or think about something before the lecture, I suggest:
- Think about how you would write a specification of a Global Snapshot
- Read something about Global Snapshots, such as:
- Chapter 10, Parallel Program Design, by K. M. Chandy and J. Misra (Addison-Wesley, 1988)
- “Distributed Snapshots: Determining Global States of Distributed Systems”, K. M. Chandy and L. Lamport, ACM TOCS, 3:1 (1985)
- “The Distributed Snapshot of K. M. Chandy and L. Lamport”, in Control Flow and Data Flow, ed. M. Broy (Springer, 1985), a version of which is found as EWD 864
Bio
Rustan Leino is Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research, Redmond and Visiting Professor in the Department of Computing at Imperial College London. He is known for his work on programming methods and program verification tools, and is a world leader in building automated program verification tools. These include the languages and tools Dafny, Chalice, Jennisys, Spec#, Boogie, Houdini, ESC/Java, and ESC/Modula-3.
Prior to Microsoft Research, Leino worked at DEC/Compaq SRC. Advised by K. Mani Chandy, he received his PhD from Caltech (1995), before which he designed and wrote object-oriented software as a technical lead in the Windows NT group at Microsoft. Leino collects thinking puzzles on a popular web page and hosts the Verification Corner channel on YouTube.
Media
- live broadcast (to be updated)