Checking equivalence of two algorithms

52 views
Skip to first unread message

christin...@gmail.com

unread,
Mar 26, 2021, 9:51:46 AMMar 26
to tlaplus
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

unread,
Mar 29, 2021, 9:31:07 AMMar 29
to tlaplus
Yes, using TLA+ to verify that optimizations maintain various system properties (relative to baseline) is a common use-case.

Andrew

christin...@gmail.com

unread,
Mar 30, 2021, 11:26:36 AMMar 30
to tlaplus
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

unread,
Mar 30, 2021, 5:23:42 PMMar 30
to tlaplus
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

unread,
Mar 31, 2021, 5:55:59 AMMar 31
to tlaplus
Thanks, that's really helpful!
Reply all
Reply to author
Forward
0 new messages