An Extension of PlusCal for Modeling Distributed Algorithms

on YouTube ↗10m

" summary

An extension called distributed PlusCal adds nested sub-processes and first-class channel types so a single process models a node with a main thread plus a helper for async reception, and provides FIFO channels and unordered channels with send receive multicast broadcast clear operations. A backward compatible translator reuses and extends the TLA+ Toolbox translator producing TLA+ that encodes pc with sub-process ids and implements multicast operator semantics using sequences or sets.

AI-written summary · about

" chapters (13)

1. 0:00Introduction
2. 0:56Distributed PlusCal Algorithms
3. 1:43Motivating example
4. 2:40Algorithm in Pluscal: main process
5. 3:22Algorithm in PlusCal: helper process
6. 4:07Lamport Mutex in Distributed Plus Cal
7. 4:43Modeling channels
8. 6:08Operations on channels
9. 6:32Translation of Unordered Channels
10. 6:59Translation of FIFO Channels
11. 7:26Program counter
12. 8:10Translation to TLA
13. 8:59Contributions and future work