Posts -

TLA⁺ is more than a DSL for breadth-first search

Posted on September 18, 2024 | Andrew Helwer

Although it isn’t usually taught that way, a lot of TLA⁺ newcomers develop the understanding that TLA⁺ is just a fancy domain-specific language (DSL) for breadth-first search. If you want to model all possible executions of a concurrent system - so the thinking goes - all you have to do is define: The set of variables modeling your system The values of those variables in the initial state(s) Possible actions changing those variables to generate successor states Safety invariants you want to be true in every state The model checker will then use breadth-first search (BFS) to churn through all possible states (& thus execution orders) of your system, validating your invariants. [Read More]

tlaplus formal-methods

TLA⁺ Unicode support

Learning to work with others in open source

Posted on May 28, 2024 | Andrew Helwer

TLA⁺ was developed by Leslie Lamport, originator of \(\LaTeX\), so it’s unsurprising that TLA⁺ syntax looks pretty \(\LaTeX\)-y. It’s a very mathy language, with much use of symbols like (among others) \A,\E, /\, \/, and \in denoting \(\forall\), \(\exists\), \(\land\), \(\lor\), and \(\in\) respectively. The language tools include a tla2tex command to format TLA⁺ specs into \(\LaTeX\) for integration in research papers. However, research papers are not where I spend the most time looking at TLA⁺. [Read More]

tlaplus formal-methods

Wrangling monotonic systems in TLA⁺

Tractable modeling of replicated logs & CRDTs

Posted on November 1, 2023 | Andrew Helwer

TLA⁺ sees a lot of use modeling distributed systems. The ability to explore all possible interleavings of events makes concurrency simple to reason about. For this TLA⁺ uses something called finite model-checking, which is really just a breadth-first search through the entire state space. The key here - and this really must be emphasized - is that the model is finite. There can’t be an infinite number of states, or of course the model checker will run forever. [Read More]

tlaplus distributed-systems formal-methods

FOSS I Love

Local game streaming with Sunshine and Moonlight

Posted on April 29, 2023 | Andrew Helwer

Here I’ll write an ode to two closely-linked FOSS projects that have, recently, absolutely floored me with their competence & quality: Sunshine and Moonlight. These are used to stream video games over a (usually local) network. Sunshine is a game streaming server: it runs on your PC as it chugs away doing all the heavy lifting of running the game itself, while Moonlight is a game streaming client that runs on whatever thin hardware exists where you want to play the game! [Read More]

Inlining SVGs for Dark Mode

Posted on April 6, 2023 | Andrew Helwer

I will here indulge in the traditional practice of using my blog to talk about how I’m using my blog. This page is built with the Hugo static site generator. I recently updated it to use the latest version of the beautifulhugo theme, which unbeknownst to me included a dark mode colorscheme. Recent browsers use the prefers-color-scheme option to automatically choose light or dark mode CSS styles, if the website supports it. [Read More]

Using TLA⁺ at Work

Designing a snapshot coordination system

Posted on April 5, 2023 | Andrew Helwer

Here’s a short report of a time I used TLA⁺ at work, with interesting results. TLA⁺ is a formal specification language that is particularly effective when applied to concurrent & distributed systems. TLA⁺ made it tractable for an ordinary software engineer to reason about a tricky distributed systems problem, and it found a bug introduced by an “optimization” I tried to add (classic). The bug required 12 sequential steps to occur and would not have been uncovered by ordinary testing. [Read More]

tlaplus distributed-systems formal-methods

Pseudocode Showdown

Python vs. PlusCal & TLA⁺

Posted on March 30, 2023 | Andrew Helwer

Last weekend I had a conversation with an undergraduate student new to computer science, who was reading CLRS. “I wish” they said, “that all the pseudocode in my algorithms textbook was just written in Python.” “Ah” I said, “but textbook authors sometimes want their work to endure beyond a decade.” “But Python’s been around for a long time” came the reply, “and it’s very readable, and you can’t execute pseudocode anyway so what’s the harm? [Read More]

formal methods tlaplus

Google Groups has been left to die

Where should the formal methods community move?

Posted on March 8, 2023 | Andrew Helwer

An unusual topic for this blog, but worth boosting to a larger audience: Google Groups is dying. Its epitaph is not yet inscribed on the Killed by Google website, but the end is easily seen from here (although it should also be noted its death was called as early as 13 years ago). The deficiencies in Google Groups search, supposedly Google’s forte, have long been noted. Lately though basic features have just stopped working. [Read More]

Can sanitizers find the two bugs I wrote in C++?

Posted on February 7, 2023 | Andrew Helwer

A few days ago I published a short post about two bugs I wrote while developing the C++ external scanner for my TLA⁺ tree-sitter grammar. Reactions were mixed! Many people were supportive, but there were of course the usual drive-by claims by developers that the bugs were trivial, they would’ve found & fixed them inside of 20 minutes, and I was laughably incompetent for having written them in the first place. [Read More]

programming

Two C++ bugs I wrote

Posted on February 4, 2023 | Andrew Helwer

Here’s a short post about two bugs I wrote while writing C++ code for the external scanner of my TLA⁺ tree-sitter grammar. External scanners use handwritten C or C++ code to parse the non-context-free parts of your language. I’ll try not to dump on C++ too hard but both of the bugs are highly ridiculous and exemplify why I hope to write as little of the language as possible for the rest of my career. [Read More]

programming