4 ms·

TLA is the awesomest thing I've ever learned, yet the least frequent technique I use as an "enterprise product" software engineer. No regrets. I recommend watc

TLA is the awesomest thing I've ever learned, yet the least frequent technique I use as an "enterprise product" software engineer. No regrets. I recommend watching the video series introducing TLA+ by Lamport, what a wonder.

gwd 6y ago
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 https://xenbits.xen.org/xsa/advisory-299.html
- agstewart 6y ago
  > And it's quite tightly bound to their particular UI tool, which makes keeping the models in git possible but somewhat quirky. I couldn't find a way of tracking the TLA+ Toolkit's files nicely in git, but with a bit of manual work it's possible, using the `tlc-bin` CLI[0]. I used the TLA+ Toolkit to write the spec[1], but wrote the models by hand (eg. [2]). This was before I heard of the VS-Code extension. I think it's quite good now, so there might be a better workflow that avoids the TLA+ toolkit altogether. > 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. Do you mean you'd like to generate a TLA+ spec from your source code? [0] https://github.com/pmer/tla-bin https://github.com/pmer/tla-bin [1] https://github.com/statechannels/tla-specs/blob/6d7227e2d18331c7a415b27cada2639557e99d48/ForceMove.tla https://github.com/statechannels/tla-specs/blob/6d7227e2d183... [2] https://github.com/statechannels/tla-specs/blob/6d7227e2d18331c7a415b27cada2639557e99d48/Version1.tla https://github.com/statechannels/tla-specs/blob/6d7227e2d183...
  - gwd 6y ago
    Yes, I think I was more or less inspired by tlc-bin; but in the end it didn't give me the control that I wanted, so I ended up just putting the Java command into my Makefile. I'm not sure what you're calling "spec" vs "model"; I wrote stuff in PlusCal, which I checked into git; then used `make` to translate that into .tla automatically as needed. The .tla files are .gitignored, so don't choke up your commit history with machine-generated stuff. Here's a snippet of my Makefile: %.tla: %.pcal cp $< $@ java -cp $(TLATOOLS_JAR) pcal.trans -nocfg $@ rm -f $*.old .PHONY: all-sources all: all-sources SOURCETARGETS += XSA287.tla TESTTARGETS += XSA287-A.out XSA287-A.out: XSA287-A.cfg XSA287.tla java -cp $(TLATOOLS_JAR) -XX:+UseParallelGC tlc2.TLC -config $< -workers 8 XSA287.tla | tee $@ The idea here is that doing "make" would simply compile all the .pcal files into .tla files (thus effectively doing a syntax check); but if you wanted to run any specific test, you would name the output file the test would generate. You can see how I'm working against the way TLA wants to work: It wants to take your PlusCal code at the beginning of the file and rewrite the end of the file, "helpfully" backing up the old file with a ".old" extension; I want to take plain PlusCal code and generate an intermediate file (like an object file) which is not checked in. So I have to copy $FOO.pcal to $FOO.tla, run `pcal.trans` on $FOO.tla, and then delete the useless "$FOO.tla.old" file. I always meant to publish these after XSA-299 went public, but haven't gotten around to it. > Do you mean you'd like to generate a TLA+ spec from your source code? Well obviously the whole project is so large as to be completely prohibitive. The model is written in the C-like variant of PlusCal, and uses a lot of the same variable names and such to help make sure they match the real C functions; and then translated into TLA. It would be nice if I could designate just one file (written in C) whose functions would be translated into TLA. The properties you want to verify about those functions would obviously need to be written in TLA directly.
    - agstewart 6y ago
      > I'm not sure what you're calling "spec" vs "model" This is from memory, but the TLA+ toolkit distinguishes between your "specification of your algorithm" and a (bounded) "model of your specification". So, you might have some spec for a sorting function that works for arrays of natural numbers of arbitrary length. And your model would limit it to arrays of length 5, and "define" the natural numbers to be `range(0,10)` -- ie. you are checking a finite "model". I think this is consistent with the language used in the wiki article (the OP). > You can see how I'm working against the way TLA wants to work I'd much prefer your suggested workflow. I don't recall that you can write plain old pcal It's amusing that you want some TLA CLI tools that work kind of how the LaTex toolkit works, another of Leslie Lamport's contributions... > I always meant to publish these after XSA-299 went public, but haven't gotten around to it. Please do! > It would be nice if I could designate just one file (written in C) whose functions would be translated into TLA. The properties you want to verify about those functions would obviously need to be written in TLA directly. That seems like a really tractable problem to me, if the C files were written with this in mind. I've actually been thinking about this since giving an internal talk on my TLA+ project last week!
Twirrim 6y ago
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.
mattm 6y ago
> 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 https://lamport.azurewebsites.net/video/videos.html
aequitas 6y ago
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.

gwd 6y ago

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 https://xenbits.xen.org/xsa/advisory-299.html

agstewart 6y ago
> And it's quite tightly bound to their particular UI tool, which makes keeping the models in git possible but somewhat quirky. I couldn't find a way of tracking the TLA+ Toolkit's files nicely in git, but with a bit of manual work it's possible, using the `tlc-bin` CLI[0]. I used the TLA+ Toolkit to write the spec[1], but wrote the models by hand (eg. [2]). This was before I heard of the VS-Code extension. I think it's quite good now, so there might be a better workflow that avoids the TLA+ toolkit altogether. > 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. Do you mean you'd like to generate a TLA+ spec from your source code? [0] https://github.com/pmer/tla-bin https://github.com/pmer/tla-bin [1] https://github.com/statechannels/tla-specs/blob/6d7227e2d18331c7a415b27cada2639557e99d48/ForceMove.tla https://github.com/statechannels/tla-specs/blob/6d7227e2d183... [2] https://github.com/statechannels/tla-specs/blob/6d7227e2d18331c7a415b27cada2639557e99d48/Version1.tla https://github.com/statechannels/tla-specs/blob/6d7227e2d183...
- gwd 6y ago
  Yes, I think I was more or less inspired by tlc-bin; but in the end it didn't give me the control that I wanted, so I ended up just putting the Java command into my Makefile. I'm not sure what you're calling "spec" vs "model"; I wrote stuff in PlusCal, which I checked into git; then used `make` to translate that into .tla automatically as needed. The .tla files are .gitignored, so don't choke up your commit history with machine-generated stuff. Here's a snippet of my Makefile: %.tla: %.pcal cp $< $@ java -cp $(TLATOOLS_JAR) pcal.trans -nocfg $@ rm -f $*.old .PHONY: all-sources all: all-sources SOURCETARGETS += XSA287.tla TESTTARGETS += XSA287-A.out XSA287-A.out: XSA287-A.cfg XSA287.tla java -cp $(TLATOOLS_JAR) -XX:+UseParallelGC tlc2.TLC -config $< -workers 8 XSA287.tla | tee $@ The idea here is that doing "make" would simply compile all the .pcal files into .tla files (thus effectively doing a syntax check); but if you wanted to run any specific test, you would name the output file the test would generate. You can see how I'm working against the way TLA wants to work: It wants to take your PlusCal code at the beginning of the file and rewrite the end of the file, "helpfully" backing up the old file with a ".old" extension; I want to take plain PlusCal code and generate an intermediate file (like an object file) which is not checked in. So I have to copy $FOO.pcal to $FOO.tla, run `pcal.trans` on $FOO.tla, and then delete the useless "$FOO.tla.old" file. I always meant to publish these after XSA-299 went public, but haven't gotten around to it. > Do you mean you'd like to generate a TLA+ spec from your source code? Well obviously the whole project is so large as to be completely prohibitive. The model is written in the C-like variant of PlusCal, and uses a lot of the same variable names and such to help make sure they match the real C functions; and then translated into TLA. It would be nice if I could designate just one file (written in C) whose functions would be translated into TLA. The properties you want to verify about those functions would obviously need to be written in TLA directly.
  - agstewart 6y ago
    > I'm not sure what you're calling "spec" vs "model" This is from memory, but the TLA+ toolkit distinguishes between your "specification of your algorithm" and a (bounded) "model of your specification". So, you might have some spec for a sorting function that works for arrays of natural numbers of arbitrary length. And your model would limit it to arrays of length 5, and "define" the natural numbers to be `range(0,10)` -- ie. you are checking a finite "model". I think this is consistent with the language used in the wiki article (the OP). > You can see how I'm working against the way TLA wants to work I'd much prefer your suggested workflow. I don't recall that you can write plain old pcal It's amusing that you want some TLA CLI tools that work kind of how the LaTex toolkit works, another of Leslie Lamport's contributions... > I always meant to publish these after XSA-299 went public, but haven't gotten around to it. Please do! > It would be nice if I could designate just one file (written in C) whose functions would be translated into TLA. The properties you want to verify about those functions would obviously need to be written in TLA directly. That seems like a really tractable problem to me, if the C files were written with this in mind. I've actually been thinking about this since giving an internal talk on my TLA+ project last week!

Twirrim 6y ago

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.

mattm 6y ago

> 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 https://lamport.azurewebsites.net/video/videos.html

aequitas 6y ago

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.