4 ms·

> is that it's hard to tell if a particular C++ or Rust implementation conforms to the spec. You can use either TLC's graph output or simulation mode to genera

by hwayne 5y ago

> is that it's hard to tell if a particular C++ or Rust implementation conforms to the spec. You can use either TLC's graph output or simulation mode to generate lots of TLA+ traces. Then you write an orchestrator that reads the trace as JSON and run the same actions in each step on the program, then confirm they have the same final states. You can go the other way, too, where you take program traces and map them onto the TLA+ state space. It's a bit tricky to set up, but it's possible. I've had several clients who've built something similar.

adsharma 5y ago
https://www.microsoft.com/en-us/research/blog/p-programming-language-asynchrony/ https://www.microsoft.com/en-us/research/blog/p-programming-... makes the case better than I can on why it's important to have the specification and implementation come from the same source as opposed to maintaining two and then verify via traces that they're compatible. But definitely worth doing (like Jepsen does) to find problems in the implementation.
- hwayne 5y ago
  Yeah, if you can do it economically, having a single source is preferable.
im_down_w_otp 5y ago
This is, incidentally, one of the kinds of use cases that informed part of our product functionality. 1. A way to write down fairly complicated system/behavior-level specs for distributed systems. 2. A way to instrument implementations to get the necessary signal out of the system to verify it nominally. 3. A way to automatically explore adverse conditions to validate that the system keeps behaving as needed and specifically isolate contributing factors for when it doesn't. The very first prototype was leveraged (in-part, as there was much more too the system under test) in a consensus mechanism that was central to the correct, stable, and most importantly... safe... operation of some critical software infrastructure. It was necessary to try to explore where the model assumptions broke down in practice in a real system.

by hwayne 5y ago

adsharma 5y ago

https://www.microsoft.com/en-us/research/blog/p-programming-language-asynchrony/ https://www.microsoft.com/en-us/research/blog/p-programming-... makes the case better than I can on why it's important to have the specification and implementation come from the same source as opposed to maintaining two and then verify via traces that they're compatible. But definitely worth doing (like Jepsen does) to find problems in the implementation.

hwayne 5y ago
Yeah, if you can do it economically, having a single source is preferable.

im_down_w_otp 5y ago

This is, incidentally, one of the kinds of use cases that informed part of our product functionality. 1. A way to write down fairly complicated system/behavior-level specs for distributed systems. 2. A way to instrument implementations to get the necessary signal out of the system to verify it nominally. 3. A way to automatically explore adverse conditions to validate that the system keeps behaving as needed and specifically isolate contributing factors for when it doesn't. The very first prototype was leveraged (in-part, as there was much more too the system under test) in a consensus mechanism that was central to the correct, stable, and most importantly... safe... operation of some critical software infrastructure. It was necessary to try to explore where the model assumptions broke down in practice in a real system.