2,920 karma · joined March 21, 2017
A really good paper on the difference between "possible" and "eventual" is '"Sometime" is sometimes "not never"': https://dl.acm.org/doi/10.1145/567446.567463
- Have a clear notion of what part of the specs represents the system under your control (the "machine"), and what part represents the broader world it interacts with. The world can do more than the machine, and the properties on the world are much more serious.
- Make lots of helpers. You need them more than you think.
- Add way more comments than you normally would. Specs are for analyzing very high-level ideas, and you should be explaining your high-level ideas.
- Make the spec assumptions clear. What has to be true about the operating environment for the spec to be sensible in the first place?
- Use lots of model values, use lots of constants, use lots of ASSUME statements. Constrain your fairness clauses as narrowly as possible.
- Understand the difference between the semantics of TLA+ as an abstract notation and the semantics of TLA+ as something concretely model-checked. For example, TLA+ is untyped, but the model checker is typed. Also, a lot of TLA+ features are not available in different model checkers. OTOH, you can break TLA+ semantics with use of TLCSet and TLCGet.
The last tip applies to whatever modeling language you use: most have the same distinction.
The other big question: what happens if user A makes change X and user B makes change Y? There's a lot of outcomes the product can pick between, but whatever they pick it should be consistent. That consistency in conflict resolution is a good property to model.
This has burned me before when I e.g needed to take the mean of a sequence.
(Then again, AIUI it's basically a thin wrapper over stochastic matrices, so maybe that's asking too much...)
I think it's disingenuous to say that TLA+ verifiers "may or may not have limitations" wrt floats when none of the available tools support floats. People should know going in that they won't be able to verify specs with floats!
- McCarthy's "Direct Union" is probably conflating "disjoint union" and "direct sum".
- ML probably got the sum/product names from Dana Scott's work. It's unclear if Scott knew of McCarthy's paper or was inspired by it.
- I called ALGOL-68 a "curious dead end" but that's not true: Dennis Ritchie said that he was inspired by 68 when developing C. Also, 68 had exhaustive pattern matching earlier than ML.
- Hoare cites McCarthy in an earlier version of his record paper [2].
Also I kinda mixed up the words for "tagged unions" and "labeled unions". Hope that didn't confuse anybody!
[1] https://lobste.rs/s/ppm44i/very_early_history_algebraic_data...
from z3 import \*
a, b, c = Ints('a b c')
x, y = Ints('x y')
s = Solver()
s.add(a > 5)
s.add(a % 2 == 0)
theorem = Exists([b, c],
And(
a == b + c,
And(
Not(Exists([x, y], And(x > 1, y > 1, x \* y == b))),
Not(Exists([x, y], And(x > 1, y > 1, x \* y == c))),
)
)
)
if s.check(Not(theorem)) == sat:
print(f"Counterexample: {s.model()}")
else:
print("Theorem true")- T550.6. T550.6. Only half a son is born by queen who ate merely half of mango.
- A1066. A1066. Sun will lock moon in deep ditch in earth's bottom and will eat up stars at end of world.
- K87.1. K87.1. Laughing contest: dead horse winner.
I try not to use them too much because I want to build the skill of using SMTs directly for now.
It models N threads non-atomically incrementing a shared counter, with the property "the counter eventually equals the number of threads in the model". When checked in TLA+, it finds a race condition where one threads overwrites another value. I've written implementations of the buggy design and on my computer, they race on less than 0.1% of executions, so testing for it directly would be very hard.
Most TLA+ specs are for significantly more complex systems than this, but this is a good demo because the error is relatively simple.