TLA+

Perhaps I'm missing something but shouldn't that bug be filed with the glibc project rather than with the weave project?

Has glibc since fixed the issue?

>"100% convinced it's worth learning to debug or verify any kind of distributed or multithreaded synchronization primitive."

Might you or anyone else have some resources you could recommend for learning TLA+?

I have compiled my research in formal verification tools and papers here, there are a couple dozens:

- https://github.com/mratsim/weave/issues/18

I find it suspicious that glibc and musl should have the same bug. Double check your code?

Heckin'! One of my favorite things to see in TLA+ adoption is people making more tools to work with it.

TLA+ is fear driven development. If you have any fears that your TLA+ model or proofs might have been written wrong, your job is to encode those fears as further TLA+ proofs.

The last TLA+ specification I wrote was only about two pages long. The actual model was a handful of lines. A handful of definitions. And then a page and a half of proofs and proof proofs.

So it's easy to look over your spec exhaustively. And if there's any part of it you aren't sure about, or think you might have written wrong, then write more proofs that show that it you can't have written it wrong that way.

The IDE provides lots of feedback and ways to debug. So like learning any language, you'll spend your formative time just trying out different parts of the TLA+ semantics and introspecting the outputs to make sure the models are behaving the way you expect them to.

TLA+ is very much like doing math. If you do it wrong, you get answers that don't make sense. And it's easy to check if you're doing it wrong, by doing something you _know_ is wrong. If you get a "right" answer, you know you are making a mistake or don't understand a semantic correctly. The joy is that TLA+ allows you to write out these proof proofs and have them checked every time along with the rest of your spec.

> how do I decide if the most plausible cause is a bug in my code, or a bug in the spec ?

Your implementation and your TLA+ model share the same state data structures (though the TLA+ model might have a simplified representation of those states, eliding unimportant details). If you suspect your spec, you just copy the broken state sequence your implementation is encountering into your TLA+ model. If the model displays the same behavior you know your spec is wrong. If it doesn't, you know your implementation is wrong.

TLA+ specs are often short which aids in verifying and validating them, especially in comparison to typical development projects. TLA+ also permits ignoring non-essential details and focusing on the core aspects of the problem.

As an example of the latter, I used TLA+ once (only) for work to great success. But the spec I wrote ignored nearly every detail about the larger system, and focused on a few hardware details and modeled the shared memory system as a simple sequence of, rather arbitrarily, 5-11 elements (fixed in the models, in the spec it was a variable). What was stored in the memory? It didn't matter at all, it could literally be anything as far as the model and spec were concerned.

My point being, the spec was so simple that visual inspection and a bit of analysis could tell us that it was correct, it fit in a couple pages if printed out. Model checking let us verify that it had the desired behaviors (with respect to the invariants that I put in based on the official specs for the hardware). Later, weakening the invariants allowed me to "recreate" the race condition that existed in the hardware implementation and was causing all our problems.

> 1. Given you have to learn the language, and, at first, you don't know it - how do you even trust that you're writing a proof right, and that you're not simply writing gibberish ? TDD has code execution as an "arbiter of peace". If, when calling a function, you get an unexpected result, then... you did something wrong.

I write TLA+ specs in the same way I do TDD: first write an invariant or property I know I should half, then make it fail, then modify the spec to pass the invariant.

> If my TLA+ set of rules holds, how do I get confidence that I wrote the right set of rules ?

Ultimately, nothing can guarantee this for us, just as nothing can guarantee we wrote the right code. This is one reason why I'm a strong advocate of spec reviews. Getting another pair of eyes on the spec goes a long way.

> 2. Once I've got a set of rule that I decided to trust, when I implement it and I get bugs (as demonstrated by executable code) ; how do I decide if the most plausible cause is a bug in my code, or a bug in the spec ?

It depends. This has happened to me a couple of times before. In one case, it was because I forgot to include something in the spec. Adding that caused the spec to immediately fail, which corresponded to the executable bug. In another case, I was able to identify, assuming the spec was correct, where the spec-code mistmatch must have been to cause the bug. So I was able to identify the code issue much faster than without the spec.

It helps that specs are usually much smaller than the corresponding codebase, so you can sweep it for issues much faster.

SAT and SMT solvers deal with propositional logic only. TLA+ is based on propositional logic with added modalities (i.e. what a type theorist would call monads) for "time" (in the temporal logic sense) and non-determinism. It is essentially a somewhat bespoke modal logic. Modal logics in general have lower expressive power than FOL, but are conversely more computationally tractable.

Depending on the problem that you are trying to solve with TLA+, you may prefer one encoding or another. For instance, here is one encoding for the proof system: https://hal.archives-ouvertes.fr/hal-01768750/. And here is another encoding for model checking: https://dl.acm.org/doi/10.1145/3360549

TLA+ is just a mathematical language; it doesn't do anything other than help you formally express the behaviour of discrete dynamical systems and write formal proofs of propositions about them. It was designed to be used with pen and paper, and often the greatest benefit comes from using it that way. Various automated tools -- two model checkers employing completely different algorithms and a proof assistant that also uses different technique to talk to different backends (SMT solvers, Isabelle, tableaux provers) -- were added much later, and at different times, and they each cover different subsets of the language. So the multitude of algorithms employed by the tools are not the primitives.

I've written a series of posts that covers the TLA+ theory (but it isn't a tutorial): https://pron.github.io/tlaplus

I think you'd be better off starting with a simpler formalism for this, like Linear Temporal Logic. That's a good pick because there's a straightforward mapping to Büchi automata. This will give you some more intuition on model checking in general, but TLA+ is much more complex than LTL.

(The most popular model checker for TLA+, TLC, is a brute forcer that represents the state space as a directed graph. Lamport talks about it a bit in Specifying Systems.)

TLA has some amazing capabilities, no doubt about it. A few years ago I had to try to fix some security issues in the most complicated code I'd ever worked with [1]. Some of the "attacks" involved race conditions across three different processors: it was incredibly difficult to keep everything in my head.

So I entered the key parts of the algorithm in to TLA+. It found all of the races that I'd found in the original algorithm; and then didn't find any issues in my fixed algorithm. That gave me at least some confidence that I'd gotten things mostly right.

That said, it's really quite a wonky tool in a number of ways. The almost-C dialect which doesn't have local variables is quite a footgun. And it's quite tightly bound to their particular UI tool, which makes keeping the models in git possible but somewhat quirky.

What I'd honestly like more is to be able to make some files which could be compiled either in the real software project, or as part of a formal verification testing step. That way you could verify the properties as part of your CI loop (or perhaps part of more extended testing done elsewhere, if that's too expensive), and also have more confidence that the implementation matched your model.

[1] https://xenbits.xen.org/xsa/advisory-299.html

I've mentioned this a number of times here. AWS uses TLA+ all over the place, and use is strongly encouraged and supported.

A service team I worked for had to implement a back-end process that had zero tolerance for mistakes. The engineers involved had a principle engineer peer reviewed process worked out, and got encouraged to model it in TLA+ as part of that review process given what it was at hand. Two engineers learned TLA+ and PlusCal over the space of about a week, and then outlined the process over the next week or so, and kept finding minor, improbable, correctness bugs.

Once fixed, they found translating the code in to actual Java to be very straight-forward "It's fill in the blanks. The whole logical structure is there already".

In the end, the feature landed well ahead of planned time, even accounting for the time taken to learn and prove correctness, and was able to be launched with little fanfare and high degrees of confidence.

I know at least one of those engineers has gone on to use it very regularly. It gives them a good chance to model the logic first, solving the actual problem at hand, and then start thinking about "the boring stuff" like database connections, unit tests etc.

> I recommend watching the video series introducing TLA+ by Lamport

I'm guessing this is the video series for anyone looking for a link https://lamport.azurewebsites.net/video/videos.html

I love his meticulous explanation of how to use the toolbox and hammering on the Getting started and help. It really show his experience with explaining this to so many students and reflects the questions he got the most.

It's a manual process, but I read there are tools that try to automate it.

But as far as I understood it, if you know TLA+ and the target language well, it's like writing an article from a good outline.

For TLA it's manual. For other systems, like Coq for instance, you can extract to another language.

(Also important are that systems in this space are different. What something like Coq is good for is completely different to what TLA+ is good for. Another idea in the same vein is property-based-testing. Here the concrete code is tested by invoking random test examples, so you are testing the actual code/implementation. But this also means you can't use typical tricks of model checkers where they can regard whole classes of inputs the "same" in a test).

Think of writing a TLA+ spec as structured thinking with error checking. It helps create a correct algorithm. Having your code implement the algorirthm correctly is a different problem.

There was a Racket language that actually syntesized programs from specs (e.g. go from spec of a sorting algo to its implementation automatically), but I forget what it's called. Fun to play around with.

You can construct formal proofs about a TLA+ spec, using the "TLA proof system" (TLAPS). Or, you can verify properties for "bounded models" of your spec via brute force.

The latter is much less overhead, so it's good to use bounded models (with the TLC model checker) to become confident in the spec, then construct proofs if warranted.

> How valuable is TLA+ for non-concurrent applications?

My understanding is that TLA+ is for concurrent applications, but with a broad definition of "concurrent." For example, it could be...

* multiple hosts messaging each other

* multiple threads in one process sharing a data structure

* multiple API calls that all use the same Postgres DB

In other words, any sort of system where different actors can step on each others' toes.

If you don't have any concurrency or nondeterminism in your spec, then you'll probably want different tools. It's not that TLA+ is bad at modeling single-threaded algorithms, it's just that makes a lot of design decisions around representing concurrency, and there's an opportunity cost to that. I'd consider a code-level formal verification language, like Liquid Haskell or Dafny.

IMHO your CS212 work is didactic, not applied

Not familiar with that course, but there are definitely applications for proof-writing to show that code does what you expect and/or satisfies certain properties - the seL4 microkernel [1] is probably the highest-profile example - but it quickly becomes impractical beyond small programs, or if the code wasn't written with proving in mind initially.

IMO the most "practical" application for those methods is in strengthening type systems to allow more expressive constraints - one small example that comes to mind is Idris [2] allowing you to explicitly mark certain functions as total [3] and fail type-checking if they don't return a value for every possible input.

The main thing to keep in mind with TLA+ is that it's not really meant for validating code, it's more for showing that your design is consistent and satisfies safety requirements (e.g. "no temporary node failure should result in data loss"). However, having a TLA+ specification usually makes the implementation fairly straightforward, especially in languages/environments with message-passing concurrency.

You can use TLAPS [4] to write proofs-by-induction similar to yours for TLA+ specifications, but IMO the real power is in model-checking them with TLC, which gives you a lot of the advantages of formal methods with much less proof work.

[1] https://github.com/seL4/l4v

[2] https://www.idris-lang.org/

[3] https://idris.readthedocs.io/en/latest/tutorial/typesfuns.ht...

[4] https://tla.msr-inria.inria.fr/tlaps/content/Home.html

That's a different style of proof, based on equational reasoning; Agda [0], Coq [1] and Lean [2] are three theorem provers that work with those proofs better. Being able to quickly and informally perform equational reasoning on functional programs is also what (imo) makes those languages easier to think about, so it's a valuable skill outside of proving.

[0]: https://wiki.portal.chalmers.se/agda/pmwiki.php [1]: https://coq.inria.fr/ [2]: https://leanprover.github.io/

In my school our Software Eng program is heavily focussed on formal verification. In my experience, the practical applications we learn are still too fat detracted from industry to be applicable.

Everything starts with two logic courses EECS/MATH 1028 which covers basics like induction and pigeon hole princele and MATH 1090 which covers first principles and axioms of logic.

Then, using the courses on logic that we did by hand, we have a system verification course (EECS 3342) with SMTs like Rodin which can solve on its up to a point where we need to manually input the proofs. Beyond this, we also cover proving preconditions and post conditions through design by contract in EECS 3311 - Software Design (which is usually tough in Eiffel, but finally being taught in Java after a year of lobbying the faculty).

Then our final courses are EECS 4312 and 4315 for requirements engineering and mission critical systems respectively. In 4312 we learn TLA+ and 4315 is focussed on tree and path logic for states. As well, we have EECS 4313 advanced software testing which is primarily about writing bug reports, creating tests (JUnit) and touches on distributed systems tests a bit.

The point is that we do learn the "practical" (quite impractical since our prof's are not in industry) only once we have had a lot of exposure to proving things by hand. But even once we have learned everything, they fail to connect material to realistic SDLCs and how to implement the tools in an agile methodology.

What you will realize years after you leave college is that in many cases, the way you do things is designed to get you to integrate a concept with your understanding of the domain. For instance, this is why many courses will ask you to write code to do something while disallowing the standard library. I see a lot of students complain "There's a library function that does exactly this but for some reason I can't use it!" But not using it is exactly the point.

Viewing college as a trade school is a mistake many of us make. No, you're almost certainly never going to be manually proving things by induction in the real world. But that doesn't make the exercise valueless.