3 ms·

I'd like to learn more: how would one go about ensuring the implementation was an accurate implementation of the specification? Is there a process for doing thi

by kinmi 6y ago

I'd like to learn more: how would one go about ensuring the implementation was an accurate implementation of the specification? Is there a process for doing this?

thamer 6y ago
There's no perfect answer and it's always been a limitation to take into account. There are model-checking solutions which take a spec and generate code, but you don't get this with TLA+. In a way, you could make the same argument about writing tests: the code paths you exercise in your CI environment are not quite the same as what's running in prod, and neither is the environment in which the code is running (e.g. the load your process or host is under, the memory pressure, etc). That said, don't let this small gap and the lack of a perfect solution discourage you from using model checking, there is still a lot to gain from adding it as one more tool in your toolbox.
Jtsummers 6y ago
To the best of my knowledge there's no universal, formal method to translate the spec into code and verify the code properly implements the spec. Just like without TLA+, you're left to conduct your own testing and analysis to verify your code is correct, but with TLA+ you at least have a specification to verify it against (even if it's tedious). That said, some languages offer more capabilities and tooling to support this. Check out Frama-C and its Mthread plugin [0] (NB: I have no experience with either) for something that could help. In Ada there's SPARK, but I'm not sure the extent that it helps with verifying concurrency properties. In some languages, like Erlang, Elixir, and Go, the concurrency mechanism is sufficiently well integrated into the languages that it becomes very clear while reading the code what's happening (especially if you properly segment your code into functions and modules to aid in readability). These can make the analysis much easier to perform. And regardless of language, if you have a specification and design the code tends to come out much cleaner, which makes the manual task of reviewing and verifying these critical parts less onerous. Additionally, it's not as hard to conceive of tests when you have the simpler spec to look at versus the much larger code constructed from it. [0] https://frama-c.com/mthread.html https://frama-c.com/mthread.html
aliceryhl 6y ago
The way I think of it is that TLA+ is a tool for ensuring that the thing you intended to write will work. It's not a tool for checking whether you wrote the thing you intended to.

by kinmi 6y ago

I'd like to learn more: how would one go about ensuring the implementation was an accurate implementation of the specification? Is there a process for doing this?

thamer 6y ago

There's no perfect answer and it's always been a limitation to take into account. There are model-checking solutions which take a spec and generate code, but you don't get this with TLA+. In a way, you could make the same argument about writing tests: the code paths you exercise in your CI environment are not quite the same as what's running in prod, and neither is the environment in which the code is running (e.g. the load your process or host is under, the memory pressure, etc). That said, don't let this small gap and the lack of a perfect solution discourage you from using model checking, there is still a lot to gain from adding it as one more tool in your toolbox.

Jtsummers 6y ago

To the best of my knowledge there's no universal, formal method to translate the spec into code and verify the code properly implements the spec. Just like without TLA+, you're left to conduct your own testing and analysis to verify your code is correct, but with TLA+ you at least have a specification to verify it against (even if it's tedious). That said, some languages offer more capabilities and tooling to support this. Check out Frama-C and its Mthread plugin [0] (NB: I have no experience with either) for something that could help. In Ada there's SPARK, but I'm not sure the extent that it helps with verifying concurrency properties. In some languages, like Erlang, Elixir, and Go, the concurrency mechanism is sufficiently well integrated into the languages that it becomes very clear while reading the code what's happening (especially if you properly segment your code into functions and modules to aid in readability). These can make the analysis much easier to perform. And regardless of language, if you have a specification and design the code tends to come out much cleaner, which makes the manual task of reviewing and verifying these critical parts less onerous. Additionally, it's not as hard to conceive of tests when you have the simpler spec to look at versus the much larger code constructed from it. [0] https://frama-c.com/mthread.html https://frama-c.com/mthread.html

aliceryhl 6y ago

The way I think of it is that TLA+ is a tool for ensuring that the thing you intended to write will work. It's not a tool for checking whether you wrote the thing you intended to.