PinnedGregory TerzianAn afternoon in the park with 杜可風 — Christopher Doyle, Shanghai, 2021On a sunny mid-autumn afternoon in Shanghai, Christopher Doyle, also known by his Chinese name 杜可風(“like the wind”), was enjoying the…Dec 10, 2021Dec 10, 2021
Gregory TerzianRe-fixing Servo’s event-loopA follow-up on a previous story, in which we identify another problem, and perhaps confirm a theory through a theorem.Aug 13Aug 13
Gregory TerzianFixing Servo’s Event LoopThe story of Servo’s event-loop fix, written in Rust and modeled in TLA+Jun 28Jun 28
Gregory TerzianTalk at GOSIM Europe May 2024I will hold a talk at Gosim 2024, May 6 at 15:10, on Modularity in Servo:Apr 302Apr 302
Gregory TerzianWhy TLA+ is important(for concurrent programming)Sometimes, one is asked why TLA+ is useful, in particular in the light that “it cannot verify code.”Apr 231Apr 231
Gregory TerzianUnderstand Viewstamped Replication with Rust, Automerge, and TLA+Viewstamped Replication is the underdog of consensus algorithms: invented just before Paxos, and revisited in 2012, it so far missed the…Nov 26, 2023Nov 26, 2023
Gregory TerzianUnderstand Paxos with Rust, Automerge, and TLA+ — Part 3: Multi-Decree.In the first part of this series, we went over the single-decree synod algorithm of Paxos. In the second part we discussed a mechanism for…Oct 18, 2023Oct 18, 2023
Gregory TerzianUnderstand Paxos with Rust, Automerge, and TLA+ — Part 2: ElectionOne way of doing election in PaxosOct 2, 2023Oct 2, 2023
Gregory TerzianUnderstand Paxos with Rust, Automerge, and TLA+ — Part 1: The Synod.What a computing device does next depends on its current state, not on what steps it took in the past. Leslie Lamport, in Teaching…Sep 25, 2023Sep 25, 2023
Gregory TerzianDistributing Lamport’s bakery with Automerge, and a touch of TLA+Leslie Lamport discovered the the Bakery Algorithm in 1974 as an alternative solution to Edsger W. Dijkstra’s mutual exclusion problem…Jul 28, 2023Jul 28, 2023