New Essay, Intentional Errors, and a TLA+ CLI

New Essay

I haven't posted any essays on formal methods in a while, so let's start of the new year right:

(No, I got no idea what the missing picture in the top left is supposed to be. There aren't any images in the post itself.)

As you can tell from the title, this is about hyperproperties: properties that span sets of behaviors, not just individual behaviors. So that's things like "If I kick the server, it doesn't change the output, whatever the output is supposed to be" or "Is this vulnerable to Spectre". Prooooooobably not very useful in practice, but still very interesting in theory! And the ideas are informally useful: hyperproperties help me think about systems better, even if I don't use them directly.

(Yes that's the same argument used for learning Lisp, Smalltalk, Haskell, Forth, APL, Erlang, Prolog, Eiffel, Coq, Rust, UML, and juggling. My justification is my thing is, like, a 10 minute read, as opposed to weeks or months of study.)

Intentional Errors

So I did two things that are unusual for me with that post.

1. I didn't have anybody else look at it. I still edited it a bunch, but it didn't get a second pair of eyes. I just wanted to put it up as fast as possible so I could get it out of my system and move on with life.
2. There are some things I know are wrong in there! Can you spot them???

I'll give you a hint, one of the errors is in this sentence:

The 2-safety in the regular spec becomes 1-safety in the hyperspec.

Give up??? The error is that it becomes safety, not 1-safety. Safety is defined over individual program traces, 1-safety is defined over sets containing one individual program trace. If a counterexample to safety is behavior B, then the corresponding 1-safety violation is {B}.

Shocking, I know.

Or you might think it's not a big deal, because nobody reading this is going to be in a situation where that difference matters, and trying to explain the difference would just distract from the overall ideas. I could have just said "safety" instead of "1-safety", but then I'd lose narrative symmetry. Sometimes being technically correct means being pedagogically incorrect.

There's a few other small things like that, things where I intentionally said the wrong thing if it's not that wrong and flows better. I try to avoid it if possible. That often means restructuring things so that the mistake doesn't come up. For example, I never say whether "mean response time" is hypersafety or hyperliveness. That's because it looks like hypersafety but is actually hyperliveness. The reasoning gets deep enough in the weeds that it would kill the beginner's momentum. Maybe okay later in the essay, fatal right at the beginning.

I think a lot about these things. It's good to notice the specific ways writing can have problems. The more you can say beyond "this is bad" the more you can actually do to improve it.

TLA+ CLI

The essay has a couple of TLA+ error traces. In order to get them I needed to do a couple things that aren't easy in the toolbox. One: model-checking both an individual module A and also a module that instantiates A. Two: copying and pasting a plaintext error trace without the -tool metadata.

The toolbox is designed for standard users. As a writer and educator I often need to do things that are outside the standard usecase. There's already a CLI for each tool, but they require some practice to use well. In particular, you need to learn how to write TLC config files, which is its own syntax. Tweaking config files is annoying if you want to, say, add an invariant to the check just this once.

Anyway, I wrote a wrapper CLI that adds some extra affordances to the model-checker. In particular, you don't need to write a config file, and you can pass in parameters as flags. To model-check a spec with two threads and the TypeInvariant invariant, you can just write

# Linebreaks for legibility
python tlacli.py 
    --inv TypeInvariant 
    --constant Threads "{t1, t2}"
  spec.tla

You can also save config files for later and read them in as templates, so you can say "Run with template.cfg except set MaxFoo to 4."

Now, a couple of big disclaimers. One: this is a personal tool, it's incomplete and janky, and I make no promises about any backwards compatibility or future development. Second, it's not an official TLA+ project, nor a prototype of where the tooling is going to go. It's just a convenience wrapper I wrote for myself, and figured hey, some other people might find this useful too!

If you're reading this on the web, you can subscribe here. Updates are once a week. My main website is here.

My new book, Logic for Programmers, is now in early access! Get it here.