Writing correct lock-free and distributed stateful systems in Rust, with TLA+

Re:Writing correct lock-free and distributed stateful system... by oconnore on Friday May 19, 2017 @10:46AM (#14376118)

You wouldn't write an Ada contract describing the full system, you would write one describing the local behavior you just described in your TLA+ model. The model ensures that the emergent behavior of the system is correct, and the local contract ensures that the local behavior of the various actors is correct -- and therefore results in that emergent behavior. Combined, that's a fairly solid argument that your system does what you intended.

If you had to implement the full proof in Ada, there would be no point to doing the TLA+ work.

[ Parent | on HN ]

Re:Writing correct lock-free and distributed stateful system... by unboxed_type on Friday May 19, 2017 @11:05AM (#14376369)

Oh, now I see your point. Checking a TLA+ model of an algorithm and then implementing each actor in Ada reinforcing it with pre/post conditions perfectly makes sense.

Its just a little out of scope of the current thread, because the author of parent message was talking about using pure Ada/SPARK, without help of TLA+ (As I understand it in the first place), so my comment about using contracts was in that context.

[ Parent | on HN ]

Re:Writing correct lock-free and distributed stateful system... by nickpsecurity on Friday May 19, 2017 @12:10PM (#14377041)

No, I meant implementation in SPARK. The specs were already done in TLA+ in the OP's model. There's also implied porting between two notations.

[ Parent | on HN ]

Re:Writing correct lock-free and distributed stateful system... by nickpsecurity on Friday May 19, 2017 @11:01AM (#14376317)

"You wouldn't write an Ada contract describing the full system, you would write one describing the local behavior you just described in your TLA+ model. The model ensures that the emergent behavior of the system is correct, "

This is how I was seeing it happen, too.

[ Parent | on HN ]