11–20 of 28 posts
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!
Earlier quoted context omitted.
Mozilla's rr is made for exactly that.
WinDBG's Time-Travel Debugging is another nice implementation of this.
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.
Reminds me of Corensic's Jynx. https://en.wikipedia.org/wiki/Jinx_Debugger Never used it but the premise of running different possible thread interleavings in parallel and picking the one that crashes seemed genius.
Sounds like what some model checkers do. See https://en.wikipedia.org/wiki/SPIN_model_checker for example. 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, differe…
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).
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?
Earlier quoted context omitted.
Sounds like what some model checkers do. See https://en.wikipedia.org/wiki/SPIN_model_checker for example. 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, differe…
I think the typical business software could be a great place to start because you have sections of the code that would be very simple to model in a formal methods environment and that really hairy section that could actually use it (but it would be hard). 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…
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.
TLA+ specs explore all state spaces of concurrent processes. Avoiding state explosions is something you need to be conscious of when building those. The modeling required also takes some learning investment. Curious if this can really pull off something like a TLA+ state exploration and invariant violation detection with real-world code.
Maybe that's a good thing since it encourages very symmetric designs, but it bothers me
The interface looks pretty interesting! 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!
TLA+ specs explore all state spaces of concurrent processes. Avoiding state explosions is something you need to be conscious of when building those. The modeling required also takes some learning investment. Curious if this can really pull off something like a TLA+ state exploration and invariant violation detection with real-world code.
TLA+ is great, but it struggles so much to handle lots of states... 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.
Earlier quoted context omitted.
TLA+ is great, but it struggles so much to handle lots of states... Maybe that's a good thing since it encourages very symmetric designs, but it bothers me
Are there other systems where combinatorial explosions of states do not occur? Is there something in TLA that makes it prone to this where other model checkers perhaps aren't? Slightly related, isn't state space explosion an intrinsic part of any such problem? 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 ap…
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.