Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

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

github.com

Post reply on HN
Print view View original

41–50 of 96 posts

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

#41

Post by kibwen »

michaelmior wrote: post #9
sanxiyn wrote: post #7

Earlier quoted context omitted.

There is interest in enabling safe interface, that is, improving Rust the language so that you can provide safe interface with better performance. A good example is so-called "streaming iterator". There is less interest in changing Rust so that currently unsafe implementation (not interface) of safe interface can be made safe, that is, verified by compiler. As grandparent stated, and I agree, as long as interface is…

Maybe I'm missing something, but I could write an interface labelled sage on top of any unsafe code I want. Why doesn't it matter that my unsafe implementation is proven correct?

This is going to sound tautological, but the unsafe keyword is for operations that the compiler can't prove. The unsafe keyword only unlocks a very small number of possible new operations (it doesn't turn off any existing checks), and those operations make unsafe Rust as freeform as C; if you could prove unsafe Rust correct then you could just prove C code correct.

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

#42

Post by nickpsecurity »

oconnore wrote: post #40
unboxed_type wrote: post #24

Earlier quoted context omitted.

Well, TLA+ checks your 'contract' by traversing states of your model explicitly which takes a lot of time usually while in ADA we have to deduce feasibility of a contract at compile time. Checking a property of a distributed system at compile time is generally a hard problem, so I expect that ADA`s ability to do this should be rather limited.

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…

"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.

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

#43

Post by nickpsecurity »

pron wrote: post #28
nickpsecurity wrote: post #13

Earlier quoted context omitted.

That's why you implement it in Ada 2012 w/ SPARK 2014. You can encode the verification conditions as contracts. All the basic ones should be proven automatically. Those that aren't can be turned into runtime checks. https://en.wikipedia.org/wiki/SPARK_(programming_language) http://www.electronicdesign.com/industrial/rust-and-spark-so... Here's an example of combining Event-B with SPARK to split overall verification b…

No need to use Ada, though. Similarly powerful options exist for Java and C. The code-level specification language is JML (Java) or ACSL (C), and there are many verification tools, from SMT solvers, through proof assistant obligations, to concolic or randomized test generation. Nevertheless, you're never certain doing that, either, as you don't formally tie the code-level specification to the high-level specification…

They exist but SPARK's were much better on automated proving. It was due to SPARK being a simpler language designed explicitly for verification.

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

#44

Post by DanWaterworth »

munin wrote: post #29
chrisseaton wrote: post #12

Earlier quoted context omitted.

The loop is always open though. Who verifies your verification code? Who verifies the processor implementation? All you can do is reduce the gap in the loop surely?

You can close all of those. You can have large amounts of your verifier itself be verified. You can verify the CPU design (hardware people tell me this used to be standard, and a lot of the formal methods community has roots in verifying hardware). What you can't close is the language that you use to do all the verification in, itself. You wind up with a core calculus that you have to stare at really hard and trust /…

You always have to make assumptions in any formal system able to express arithmetic as proved by Gödel.

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

#45

Post by unboxed_type »

oconnore wrote: post #40
unboxed_type wrote: post #24

Earlier quoted context omitted.

Well, TLA+ checks your 'contract' by traversing states of your model explicitly which takes a lot of time usually while in ADA we have to deduce feasibility of a contract at compile time. Checking a property of a distributed system at compile time is generally a hard problem, so I expect that ADA`s ability to do this should be rather limited.

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…

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.

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

#46

Post by roblabla »

munin wrote: post #29
chrisseaton wrote: post #12

Earlier quoted context omitted.

The loop is always open though. Who verifies your verification code? Who verifies the processor implementation? All you can do is reduce the gap in the loop surely?

You can close all of those. You can have large amounts of your verifier itself be verified. You can verify the CPU design (hardware people tell me this used to be standard, and a lot of the formal methods community has roots in verifying hardware). What you can't close is the language that you use to do all the verification in, itself. You wind up with a core calculus that you have to stare at really hard and trust /…

Isn't this susceptible to a trusting trust[0] attack, where your verifier has a bug that makes it verify itself, even though it shouldn't ?

It's always possible there is a loop somewhere. The best you can hope for is make it infinitesimally small.

[0]: http://wiki.c2.com/?TheKenThompsonHack

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

#47

Post by mafribe »

dronemallone wrote: post #31
munin wrote: post #11

Earlier quoted context omitted.

This is a gap in this kind of verification work. Systems like coq get around this by having a facility to "extract" code from the proof itself. You would define your algorithm as a Fixpoint, prove properties of that Fixpoint, then extract that Fixpoint into some ocaml code and use it directly in your real programs. This closes the loop you describe, insamuch as you trust the extraction process and the ocaml compiler…

That "facility" is the Curry-Howard correspondence!

Not necessarily. Isabelle/HOL, an prover not based on CH but on the LCF-architecture, can also do program extraction, see e.g. Program extraction in Isabelle:

https://wwwbroy.in.tum.de/~berghofe/papers/TYPES2002_slides....

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

#48

Post by samth »

chrisseaton wrote: post #12
munin wrote: post #11

Earlier quoted context omitted.

This is a gap in this kind of verification work. Systems like coq get around this by having a facility to "extract" code from the proof itself. You would define your algorithm as a Fixpoint, prove properties of that Fixpoint, then extract that Fixpoint into some ocaml code and use it directly in your real programs. This closes the loop you describe, insamuch as you trust the extraction process and the ocaml compiler…

The loop is always open though. Who verifies your verification code? Who verifies the processor implementation? All you can do is reduce the gap in the loop surely?

Right, the concept of the TCB (trusted computing base) is the important thing. Good discussions of remaining TCB in verified code are in the seL4 work, or in this paper: https://www.cs.princeton.edu/~appel/papers/verif-sha-2.pdf

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

#49

Post by mcguire »

"Pluscal has two forms, c and p. They are functionally identical, but c form uses braces and p form uses prolog/ruby-esque begin and end statements that can be a little easier to spot errors with, in my opinion."

Nit: that should be Pascal/Ruby, no?

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

#50

Post by dmix »

mcguire wrote: post #49

" Pluscal has two forms, c and p. They are functionally identical, but c form uses braces and p form uses prolog/ruby-esque begin and end statements that can be a little easier to spot errors with, in my opinion. " Nit: that should be Pascal/Ruby, no?

> PlusCal (formerly called +CAL) is a formal specification language created by Leslie Lamport, which transpiles to TLA+

https://www.wikiwand.com/en/PlusCal

Post reply on HN