Dr. TLA+ Series – Global Snapshot
Episode details
Episode description
The presentation slide and the complete schedule of Dr. TLA+ Series are available at https://github.com/tlaplus/DrTLAPlus. 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 See more on this video at https://www.microsoft.com/en-us/research/video/dr-tla-series-global-snapshot/
Watch also from the same channel
More episodes from this channel
You might be interested in
