Fifth in a series on using the TLA Toolbox to explore the failure tolerance of distributed algorithms. The previous post was a description of Lamport’s 1978 mutual exclusion algorithm.
more ...Fourth in a series on using the TLA Toolbox to explore the failure tolerance of distributed algorithms. The previous post was a specialized discussion of the fairness semantics of PlusCal. The post preceding that was a general discussion of writing distributed algorithms in PlusCal. The next post presents the results of simulation runs on the algorithm.
more ...Third in a series on using the TLA Toolbox to explore the failure tolerance of distributed algorithms. The second post presented some PlusCal conventions for writing distributed algorithms. The next post presents Lamport’s (1978) mutual exclusion algorithm in PlusCal.
more ...Second in a series on using the TLA Toolbox to explore the failure tolerance of distributed algorithms. The first post presented the context and why the topic is important. The next post describes the semantics of fairness in PlusCal.
more ...First in a series on using the TLA Toolbox to explore the failure tolerance of distributed algorithms. The next post describes conventions for distributed algorithms in PlusCal.
more ...