I think adding a way to select multiple universe nodes and say “I expect all these universes to converge on the value 66” and then serialize that expectation into a runtime verification which either runs during program execution or runs during program execution when in a concurrency sanitize mode would be pretty cool!
Maybe that's a good thing since it encourages very symmetric designs, but it bothers me
If possible, could you explain what you mean by symmetry, and how it reduces state space (it's a big ask, I know).
sorry for the firehose of Q's! I'd really appreciate an expert's view though.
this is the biggest difference between relatively naive checkers like tla+ and your brain. you don't think about all the states at the same time. I do not of a model checker that does this.
symmetry was kind of explained by the other commenter. in short, you often have sets of things that have the same allowable states, and the order of these items is irrelevant. e.g. you have several worker nodes... they have state, but if two of them instantly swap states, it's possible that nothing really changed
TLA specifications are typically "checked", or rather "fuzzed" by model checkers; this is not formally required (TLA+ even includes a proof language) but things tend to be done that way.
- (Bounded) model checking is exhaustive, fuzzing is not. If your system successfully model checks, then no possible input can cause an error. Fuzzing is randomized, so there still _could_ be a bad input. That's why model checking is considered formal verification and fuzzing is not.
- Not all model checking is brute force searches. A lot of model checkers use SMT or SAT, so the check time grows slowly even with large state spaces.
- _Empirically speaking_, model-checking has scaled much better and been used for a wider range of applications than correct-by-construction has.
Oh come on. If your bounded model checking is actually checking every possible input or program state, then it's not just a method of verification but an actual proof. (It may be a subjectively inelegant proof, but it's a proof nonetheless.) That much is obvious. What I clearly meant by "glorified fuzzing" was the far more common use of model checking in ways that stop short of this standard. That sort of use can still be nicely scalable, it does count as a formal method, and it can point out remarkably complex bugs in your system - but by definition, it cannot give any assurance that you're doing things correctly! That still requires proof.
I think the difference between small and large is down to how long you're prepared to let it run, but even more fundamentally, how much memory you can give it.
I'd agree that if the model matches the code and you successfully check the entire state space then it's a proof.
Listed in this Hacker News thread we have 7 implementations in gdb, plus rr and WinDBG.
I'll add one more, an in-house hypervisor that I help develop. Stuff like finding "all concurrency bugs" as in this article would be a matter of scripting it up. BTW, we're hiring: https://news.ycombinator.com/item?id=19797601
So that's at least 10, counting the gdb backends distinctly except lumping the Linux native x86 and x86_64 together.
We actually have another gdb remote backend supporting reverse execution that's in active use but not publicly available yet --- Pernosco.
Never used it but the premise of running different possible thread interleavings in parallel and picking the one that crashes seemed genius.
Spin homepage http://spinroot.com/spin/whatispin.html
SPIN's language Promela is very odd, like stripped down basic from the 1980s but even more reduced after that.
Edit: a bit more from the spin site FYI "[spin] checks the logical consistency of a specification and reports on deadlocks, race conditions, different types of incompleteness, and unwarranted assumptions about the relative speeds of processes"
I wish so much I had reason to use it. I so much wish my programming career wasn't the daily, usually boring, straightforward business support. I'd love to work with TLA, formal methods, this and more but there seems no way to do get a job doing this. Any thoughts welcome. Been trying to learn hoare logic but it all seems so abstract, and it's easy to misunderstand things with no-one to ask. Anyway, sorry for the whinge.
I hate to say I've never had the patience for it. For me it has always turned out to be painful without much reward.
I think my experience isn't uncommon given the popularity of formal methods. If it was easy and full of low hanging fruit (like automated testing) it would probably be reasonably popular (like automated testing).
If you can't get the boss's buy-in for even obvious correctness and/or timesaving approaches (where time spent = salaries paid), I'm stuffed.
Or maybe the problem's partly me. I can't rule that out. I'm not the most politic person.
> If [formal methods] was easy and full of low hanging fruit...
It isn't and I don't expect it to be. The fruit is right at the top, but it may be the best quality. I'm ok putting in the work to reach that.
I'm looking for sites/ information that can help me to publish papers. But I do not have much idea about it.
How did you publish?