Live data from Hacker News

MIT develops new tool that can interrupt infinite loops

bostinnovation.com

61–70 of 72 posts

Re: MIT develops new tool that can interrupt infinite loops

#61

I thought the message at the end about people expecting full correctness was a bit off; after all, if we expected fully-correct programs, we would be proving them instead of writing C.

They're poking fun at the formal methods community, which spends a lot of time doing research in this direction. Percolation of these techniques back to industry has been... less than stellar.

Re: MIT develops new tool that can interrupt infinite loops

#62
post #38
post #25

Earlier quoted context omitted.

i wish i could do that for safari

You probably can: $ gdb /Applications/Safari.app/Contents/MacOS/Safari $PID iTunes, annoyingly, uses Apple's stupid little "please don't ptrace me" flag, which is a minor inconvenience, but fairly readily circumventable.

"Don't ptrace me, bro!"

Sorry, couldn't resist.

Re: MIT develops new tool that can interrupt infinite loops

#64
post #38
post #25

Earlier quoted context omitted.

i wish i could do that for safari

You probably can: $ gdb /Applications/Safari.app/Contents/MacOS/Safari $PID iTunes, annoyingly, uses Apple's stupid little "please don't ptrace me" flag, which is a minor inconvenience, but fairly readily circumventable.

I wonder if that's to make it harder to crack FairPlay.

Re: MIT develops new tool that can interrupt infinite loops

#65
post #47

Earlier quoted context omitted.

Why would that be bounded far below modern memory limits? Why would that be bounded at all ? Secondly, you're making the logic error A => B implies not A => not B. If state spaces as large as modern memory limits allow are too large, that doesn't imply that state spaces far below modern memory limits are small enough to handle. Thirdly, your program trivially terminates doing nothing.

Troll-feeding time! Pretend that an OOM condition is the same as a False answer. :3 Here's a program, building on the previous one, which either terminates or doesn't. from itertools import count for i in count(1): if not is_collatz(i): break

I don't understand your point. I could run it with memory constrained to, say, 100 KB, and it will quickly produce an OOM condition. I clearly said that the approach I sketched in my first comment is not practically applicable.

Real-life computers have bounded memory, so they don't have any more computational power than, say, regular expressions matchers -- every computational task performed by real computer can be represented by appropriately complicated regular expression. That's why one needs to be especially careful when arguing from computability when talking about real-life problems.

The more serious issue is a treatment of I/O.

Re: MIT develops new tool that can interrupt infinite loops

#66
post #32
post #22

Earlier quoted context omitted.

Due to the fact that a program is a composition of programs which at the lowest level are loops and instructions this also means that it is impossible to determine whether or not a loop halts. It is easily provable that this is theoretically possible, but the required time is too long for it to be applicable. Suppose your memory has N states. Run your program through N+1 computation steps and if it's not already fini…

It also may not be applicable if you don't actually have access to all memory states involved. E.g. when communicating with a 3rd party computer over a network.

It still is applicable, as long as you have a bound on the number of unknown states, however the number of computation steps in this case is so high that it is even less practical than the totally unpractical algorithm I proposed in my first comment.

Let's consider both computers (yours and 3rd party) as a single computational device, with a state represented by a pair of symbols, where the first represents your computer and the second the 3rd party's. Suppose your computer has N states and the other M. It's enough to run N * M + 1 computation steps -- if your program hasn't ended so far, it will never, for there's a certain state (a, b) that must have occured twice, by the pigeonhole principle.

Please keep in mind that this is all purely theoretical, and not at all practical. It's just a counterargument to other purely theoretical argument from unsolvability of halting problem.

Re: MIT develops new tool that can interrupt infinite loops

#67

Earlier quoted context omitted.

Thanks for the explanation! No shame here (I didn't study CS in undergrad) but I find it intuitive that a program can't detect an input that would loop indefinitely.

If that's intuitive for you already (great!) consider one step further: Rice's Theorem. Rice's Theorem in layman's term is "all nontrivial properties of a program are undecidable in the general case". "Undecidable" is the difficulty class of the halting problem (there are actually harder problems!). A couple accessible examples: 1. Constant Propagation - we know that we'll never detect all compile-time constants beca…

Well, you won't always be able to prove that it never raises. In many cases, you can, which is why compilers can eliminate dead code. Sometimes the compiler can prove the code is dead, sometimes it can prove the code is live, and sometimes it just doesn't know. For any prover, there will be code that defeats it.

Re: MIT develops new tool that can interrupt infinite loops

#68

This is a good line of investigation. I don't understand all the harrumphing here, except possibly as a means of self-congratulations at to why the harrumpher in question didn't bother inventing this tool themselves and how they understand the "halting problem" in a way not known at MIT. As the economist famously joked in response to 'how are you'... "Compared to what?" The comparison here is to killing the program a…

I'm one of the authors of this paper and this comment pretty much hits it on the head. Jolt is an investigation in developing tools to help users get more use out of their programs when the alternative is failure. Because the reality is that there will always be programs that fail.

Most of the comments here are pretty fair about where Jolt might not be applicable (busy loops) and how this approach could be integrated with development; we touch on many these points in the paper (already linked by someone in the comments).

All of our emails are on the interwebs, so feel free to ping us if you want more information.

Re: MIT develops new tool that can interrupt infinite loops

#69

This is a good line of investigation. I don't understand all the harrumphing here, except possibly as a means of self-congratulations at to why the harrumpher in question didn't bother inventing this tool themselves and how they understand the "halting problem" in a way not known at MIT. As the economist famously joked in response to 'how are you'... "Compared to what?" The comparison here is to killing the program a…

[deleted]
Post reply on HN