3 ms·

One thing I'm wondering is whether (or rather, what kind of) bugs arise when you try to translate a model (described as "exhaustively tested pseudocode" elsewhe

One thing I'm wondering is whether (or rather, what kind of) bugs arise when you try to translate a model (described as "exhaustively tested pseudocode" elsewhere in this thread) into a real system. For example, if there is if-branch somewhere that gets missed etc?

zozbot234 7y ago
A TLA+ specification is generally a simplified model of a real system design. So issues can definitely arise when building the real thing, but model testing on a TLA+ spec can definitely help with quickly surfacing bugs that would exist even in a simplified design. Just don't expect it to do more than that.
lemmster 7y ago
I am the engineer who translated https://github.com/tlaplus/tlaplus/blob/master/tlatools/src/tlc2/tool/fp/OpenAddressing.tla https://github.com/tlaplus/tlaplus/blob/master/tlatools/src/... into Java (https://github.com/tlaplus/tlaplus/blob/master/tlatools/src/tlc2/tool/fp/OffHeapDiskFPSet.java https://github.com/tlaplus/tlaplus/blob/master/tlatools/src/...). The translation took me about half a day. Later, while running scalability experiments, a correctness bug intermittently showed up, on which I spent approximately two weeks to find the root cause. The two weeks included fixing around a dozen bugs in code that was not specified in TLA+. However, none of these bugs were correctness bugs and unrelated to the correctness bug. Eventually, I translated the TLA+ spec into input for Java Pathfinder, which found the cause of the correctness bug immediately: The Java translation contained an off-by-one bug in a for loops (TLA+ is one-indexed while Java is zero-indexed). I am still convinced that a code review would have found the bug and that JPF was a very heavyweight substitute for a fresh pair of eyes. In other words, the bugs that get introduced during the translation phase are shallow and easily corrected. Note that no other bugs have been reported for the code since.

zozbot234 7y ago

A TLA+ specification is generally a simplified model of a real system design. So issues can definitely arise when building the real thing, but model testing on a TLA+ spec can definitely help with quickly surfacing bugs that would exist even in a simplified design. Just don't expect it to do more than that.

lemmster 7y ago

I am the engineer who translated https://github.com/tlaplus/tlaplus/blob/master/tlatools/src/tlc2/tool/fp/OpenAddressing.tla https://github.com/tlaplus/tlaplus/blob/master/tlatools/src/... into Java (https://github.com/tlaplus/tlaplus/blob/master/tlatools/src/tlc2/tool/fp/OffHeapDiskFPSet.java https://github.com/tlaplus/tlaplus/blob/master/tlatools/src/...). The translation took me about half a day. Later, while running scalability experiments, a correctness bug intermittently showed up, on which I spent approximately two weeks to find the root cause. The two weeks included fixing around a dozen bugs in code that was not specified in TLA+. However, none of these bugs were correctness bugs and unrelated to the correctness bug. Eventually, I translated the TLA+ spec into input for Java Pathfinder, which found the cause of the correctness bug immediately: The Java translation contained an off-by-one bug in a for loops (TLA+ is one-indexed while Java is zero-indexed). I am still convinced that a code review would have found the bug and that JPF was a very heavyweight substitute for a fresh pair of eyes. In other words, the bugs that get introduced during the translation phase are shallow and easily corrected. Note that no other bugs have been reported for the code since.