5 ms·

Author seems to be using https://github.com/ailidani/paxi https://github.com/ailidani/paxi for actual implementation and proof. I'm more of a python/rust guy.

Author seems to be using https://github.com/ailidani/paxi https://github.com/ailidani/paxi for actual implementation and proof. I'm more of a python/rust guy. There have been some attempts to make model checkers in rust: https://github.com/stateright/stateright https://github.com/stateright/stateright The issue is that rust is a very large language and it's hard to get it right. I have a python implementation of raft over here: https://github.com/adsharma/raft/tree/master/raft/states https://github.com/adsharma/raft/tree/master/raft/states That's small enough to be self contained and perhaps run through a model checker some day and transpiled to many statically typed languages. The issue with TLA+ proofs such as: https://github.com/fpaxos/raft.tla https://github.com/fpaxos/raft.tla is that it's hard to tell if a particular C++ or Rust implementation conforms to the spec. So how do we check and transpile? * https://www.philipzucker.com/Modelling_TLA_in_z3py/ https://www.philipzucker.com/Modelling_TLA_in_z3py/ * https://github.com/adsharma/py2many https://github.com/adsharma/py2many

littlestymaar 5y ago
> The issue is that rust is a very large language and it's hard to get it right. In my experience, Rust type system (especially the Send and Sync traits, which prevent data races) makes it easier − not harder − to get big things work.
- adsharma 5y ago
  My intention is to reuse the rust type system where we can and yet keep the language small enough to be able to implement and verify non-trivial real world programs. https://github.com/adsharma/py2many/blob/main/doc/langspec.md https://github.com/adsharma/py2many/blob/main/doc/langspec.m... https://github.com/adsharma/py2many/blob/main/CHANGELOG.md#rust https://github.com/adsharma/py2many/blob/main/CHANGELOG.md#r...
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.
toolslive 5y ago
you can abstract IO and async'ness from the implementation, and model it as a pure function. Then build and inspect the state space. A detailed description was done here: https://incubaid.wordpress.com/2012/10/25/caulking-your-distributed-algorithm-implementation/ https://incubaid.wordpress.com/2012/10/25/caulking-your-dist...

littlestymaar 5y ago

> The issue is that rust is a very large language and it's hard to get it right. In my experience, Rust type system (especially the Send and Sync traits, which prevent data races) makes it easier − not harder − to get big things work.

adsharma 5y ago
My intention is to reuse the rust type system where we can and yet keep the language small enough to be able to implement and verify non-trivial real world programs. https://github.com/adsharma/py2many/blob/main/doc/langspec.md https://github.com/adsharma/py2many/blob/main/doc/langspec.m... https://github.com/adsharma/py2many/blob/main/CHANGELOG.md#rust https://github.com/adsharma/py2many/blob/main/CHANGELOG.md#r...

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.

toolslive 5y ago

you can abstract IO and async'ness from the implementation, and model it as a pure function. Then build and inspect the state space. A detailed description was done here: https://incubaid.wordpress.com/2012/10/25/caulking-your-distributed-algorithm-implementation/ https://incubaid.wordpress.com/2012/10/25/caulking-your-dist...