Reviewing the Entry-level Model Checker Tutorial

[hwayne]

I was asked by Igor to do a review of the binary search tutorial and provide feedback. First some general thoughts, then specific notes:

First, I do not think the binary search is a good introductory tutorial for Apalache. This is for several reasons:

1. Binary search is a sequential algorithm, which takes a lot of boilerplate in TLA+.
2. The spec is several times larger than the implementation. This tells the reader that specifying with TLA+ will take a lot more time than just writing and testing the code.
3. Binary search is complicated enough that most programmers can’t tell if the spec “obviously matches” the implementation, especially with the conversions between 0- and 1-based indexing.
4. The bug is “unsurprising”. You only see the overflow error if you explicitly model overflow in the spec, and if you’re thinking of integer overflow then the corresponding bug in the implementation is obvious. A good example should have a bug that emerges from a natural specification. Compare to the bounded buffer example: it catches the deadlock even if you aren’t explicitly thinking about deadlocks in the model.

I raised this with Igor and here's his response:

Just for the context, why I picked the binary search. It looks like beginners (our engineers) are trying to juggle several aspects at the same time: (1) How to model a distributed system, (2) How to write this model in TLA+, and (3) How to make the specification good for Apalache. I wanted to focus on (2) and (3) in this tutorial, as people have very different levels when it comes to distributed systems. Also, engineers should be familiar with sequential algorithms, so they should feel more comfortable specifying them (maybe that was a wrong hypothesis).

I'll think a bit more about something that covers (2) and (3) well. In the meantime, specific comments about this example:

https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/docs/src/tutorials/entry-tutorial.md?plain=1#L84-L88 Don’t mention other model checkers if you don’t have to. It’s good to have full disclosure, but better to set up the context that you don’t need to disclose other model checkers at all.

https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/docs/src/tutorials/entry-tutorial.md?plain=1#L98 It's not clear whether the reader is supposed to be typing everything themselves or following along with these files. The tone of the tutorial seems to suggest the first, but there's places where not everything in the file is shown, like the full definition of Next. If the reader is supposed to download the files, make that clear from the start.

https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/docs/src/tutorials/entry-tutorial.md?plain=1#L114

Emphasize here that the module name must match the filename or else apalache won't check it.

https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/docs/src/tutorials/entry-tutorial.md?plain=1#L121-L125

Also emphasize to the reader that == is definition.

https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/docs/src/tutorials/entry-tutorial.md?plain=1#L138 This is only for Unix. For Windows, the command is java -jar path-to-apalache.jar check …

https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/docs/src/tutorials/entry-tutorial.md?plain=1#L141-L142 I agree, it's very hard to know what's important information. Maybe add a --concise flag?

https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/docs/src/tutorials/entry-tutorial.md?plain=1#L186 This should be "1-indexed".

https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/docs/src/tutorials/entry-tutorial.md?plain=1#L238-L244 This needs to be explained better. Is binary search really a state machine? What does it mean that variables are never “introduced or removed”? Why are you telling me that global variables are easier to reason about?

https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/docs/src/tutorials/entry-tutorial.md?plain=1#L390-L394 Having to create a separate model value file feels really messy, especially considering that you only have one model per spec. Why not just inline that all into BinSearch?

https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/docs/src/tutorials/entry-tutorial.md?plain=1#L402-L405 I find this confusing.

https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/docs/src/tutorials/entry-tutorial.md?plain=1#L451-L462

I think the property can be simplified to:

ReturnValueIsCorrect ==
  IF returnValue >= 0
  THEN INPUT_SEQ[returnValue + 1] = INPUT_KEY
  ELSE \A i \in 1..Len(INPUT_SEQ):
    INPUT_SEQ[i] != INPUT_KEY

https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/docs/src/tutorials/entry-tutorial.md?plain=1#L458 Be careful about local constant: People get confused with how TLA+ constants aren't programming constants, and then this introduces the word "constant" again.

https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/docs/src/tutorials/entry-tutorial.md?plain=1#L482-L483

Where is counterexample1.tla coming from? You only tell the reader about the counterexample files later on.

https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/docs/src/tutorials/entry-tutorial.md?plain=1#L497 Tell the reader that “disjunction” is the same thing as “or”.

https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/docs/src/tutorials/entry-tutorial.md?plain=1#L604-L615 I'd remove this entire section, or at the very least move it to a footnote.
https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/docs/src/tutorials/entry-tutorial.md?plain=1#L643-L644 There's two improvements here:

1. Saying we need to use "advanced features" of Apalache tells the reader they need to understand advanced features to get anything done, which suggests they won't be able to get anything useful as a beginner.
2. You introduce two new concepts that only make sense together. Instead find a way to introduce them one at a time, where the first is useful even before they know the second. I'd suggest introducing --cinit earlier, possibly as a way to test both 4- and 8-bit integers without having to create separate model files.

https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/docs/src/tutorials/entry-tutorial.md?plain=1#L667-L671 I don't understand what this is saying.

https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/docs/src/tutorials/entry-tutorial.md?plain=1#L687

1. Interestingly it still works with INPUT_KEY \in Int. Might be easier for people than explaining what Gen(1) is.
2. Does it matter that you're generating with MAX_INT and not MAX_UINT?

https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/docs/src/tutorials/entry-tutorial.md?plain=1#L712-L718 I did not have counterexample1.tla. Instead I had violation.tla.

https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/docs/src/tutorials/entry-tutorial.md?plain=1#L720 Let the reader know they may not get this exact counterexample.

Also, having to navigate to the folder (different for each execution!) is inconvenient. Is there a more convenient way to find the tool output?

https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/docs/src/tutorials/entry-tutorial.md?plain=1#L758-L759

1. Is what a real issue?
2. As you say in the no-pre footnote, this is more conceptually an error in the precondition. Saying it's an imprecision in the postcondition confused me for a while. The reason you give for not adding a precondition (testing it terminates on all sequences) doesn't become relevant until later. A more intuitive sequence would be 1) adding a new ConstInit with the precondtion, 2) raising the termination issue, and 3) adding a second ConstInit for general sequences.

https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/docs/src/tutorials/entry-tutorial.md?plain=1#L780 Is specifying things in the "straightforward" way that much of a performance regression? Do people have to know how to optimize Apalache to get anything of value out of it?

https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/docs/src/tutorials/entry-tutorial.md?plain=1#L782 It's really weird to say "the list isn't sorted" is a "postcondition" of the algorithm. I'd instead write it like this:

Precondition == InputIsSorted

IsCorrect ==
  Precondition => PostCondition

https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/docs/src/tutorials/entry-tutorial.md?plain=1#L794-L797 Do not ask the reader to wait hours for results. Waiting several hours to continue the tutorial is the opposite of "not bad". Switch to 4-bit integers.

(Also, if you're saying how long things take, tell us the system you're running on. I have a workstation desktop and it only took 5 minutes to run.)

https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/docs/src/tutorials/entry-tutorial.md?plain=1#L822-L824

Many engineers reading this will not know off the top of their head the complexity of binary search so can't "recall" it. Better to just say "Binary search is guaranteed to terminate within XYZ steps."

https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/docs/src/tutorials/entry-tutorial.md?plain=1#L837-L857

If you can, it's better to show this as a diff change.

https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/docs/src/tutorials/entry-tutorial.md?plain=1#L861-L865

Termination is too weak, as it passes if you set INT_WIDTH == 8, and then a length-four sequence takes six steps. What you actually want is 2^nSteps >= Len(INPUT_SEQ) + 1 => Termination (or 2^nSteps <= Len(INPUT_SEQ) + 1).

(Note that actually trying those invariants causes apalache to throw an error. Would you like a bug report from me?)

If you decide to stick with INT_WIDTH, you should explain that INT_WIDTH = ceil(log2(MAX_UINT)).

https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/docs/src/tutorials/entry-tutorial.md?plain=1#L879-L882 This is a complicated property, both in terms of what it's doing (why does the second clause mean it's progressing?) and in terms of what's happening conceptually (what does it mean to put primes in properties?) I suggest dropping it entirely.

https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/docs/src/tutorials/entry-tutorial.md?plain=1#L905-L912 Would it make more sense to just add the invariant "NoOverflows" that checks all values (including mid) are above INT_MAX?

If the issue is that you don't have access to mid, why not make that an extra variable? This would also fix the issue on InBounds where you have to calculate mid a second time.

(And also is a good place to discuss the difference between x and x' when both are used in the same step!)

https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/docs/src/tutorials/entry-tutorial.md?plain=1#L925-L941

Do I have to check every property separately? That puts every single violation into a separate folder.

(Also, it surprises me that it passes with no properties checked at all! I expected it to have an overflow, which you do discuss later.)

https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/docs/src/tutorials/entry-tutorial.md?plain=1#L1000-L1001

At this point I started running Apalache in a background job, partially out of convenience and partially out of fear of a model check taking several minutes. Is it okay to run multiple jobs in parallel?

https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/docs/src/tutorials/entry-tutorial.md?plain=1#L1090-L1091

This should be INT_WIDTH=10. I don't know if 16 bits is even checkable on commodity hardware.

https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/docs/src/tutorials/entry-tutorial.md?plain=1#L1143-L1146

I should really emphasize that 35 minutes is too long a runtime to expect for a tutorial.

[hwayne]

Update, I checked PostconditionSorted with an INT_WIDTH of 10 and it took 26 hours to complete. Suggests to me that the tutorial should use an INT_WIDTH of 6, and then have the exercises be checking on len 4 and len 8.

[shonfeder]

Many thanks for this deep and thoughtful feedback, @hwayne! From my preliminary skim here, it seems to offer many critical insights on how we can improve -- not just this tutorial, but -- our instructional material more generally.

I just wanted to let you know that Igor is currently on well-deserved vacation, so if there's some delay in detailed replies and redress on his side, this is the reason. Those are sure to follow shortly! :)

[not-azat]

I went through this tutorial and wanted to create an issue, but I see that most of the things are already covered here, so I'll just add a couple of points:

Step 2: the last snippet misses ELSE UNCHANGED ... line

Step 5: I believe that MAX_INT is not defined in the module file. Also it's not obvious for me why are we limiting sequence length with MAX_INT and not looking at bigger sequences with duplicates (maybe a little clarification would help).

[konnov]

Step 5: I believe that MAX_INT is not defined in the module file. Also it's not obvious for me why are we limiting sequence length with MAX_INT and not looking at bigger sequences with duplicates (maybe a little clarification would help).

Thanks @not-azat! You are right. We should explain that. In short, normally data structures contain an integer counter that keeps the number of the elements in the data structure. As this counter is an integer, it should not go over MAX_INT.