Checking equivalence of two algorithms

[christin...@gmail.com]

Apologies if this is a fairly basic question:

Is it possible to use TLA+ to check if two algorithms always return the same result?

An engineer on my team recently made an optimisation to a routine; interleaving floating point operations with memory operations to make an algorithm run more quickly.

It would seem to me that a good use case would be to check the validity of something like this, but I don't know if that's possible in TLA+. Of course, I can abstract the code sufficiently to the point where the question is essentially "does a+b=b+a?", at which point the proof is perhaps too trivial to be useful.

[Andrew Helwer]

Yes, using TLA+ to verify that optimizations maintain various system properties (relative to baseline) is a common use-case.

Andrew

[christin...@gmail.com]

Thanks! Do you have any pointers towards tutorials so I can figure out how to go about this? I've done a lot of reading about TLA+ but I'm very new to actually using it.

[Andrew Helwer]

This is a fairly broad question, but what I'd probably do is write a spec of both algorithms then check that their final output matches across a range of inputs. Alternatively if you can come up with some good invariants, then you can just write a spec of the optimized algorithm and check that it maintains those invariants.

Andrew

[christin...@gmail.com]

Thanks, that's really helpful!