Microsoft has a program called Terminator that basically tries to solve the halting problem. They claim it's helped them root out some bugs in their device drivers. Of course, we know the halting problem is unsolveable, but we also know that Microsoft engineers aren't stupid. So what are they doing? Well, some types of halting problems can be detected and highlighted and even if you don't find all bugs, even automatically finding some bugs is better than finding none.
Though they'll be releasing papers explaining this, I'm not sure how applicable it will be in Perl. Here's a typical example in C:
float x = 0.1;
while (x != 1.1) {
x = x + 0.1;
printf("x = %f\n", x);
}
If you translated that to Perl, would it be an infinite loop? There's actually no way to tell just by looking directly at the code:
my $x = 0.1;
while ($x != 1.1) {
$x += .1;
print "x = $x\n";
}
Well, that certainly looks like an infinite loop. Why might it not be? Because the following might not be an infinite loop:
print $foo while 1;
We're not even talking source filters here.
#!/usr/bin/perl -l
use strict;
use warnings;
{
package Arnie;
use overload '""' => \&to_string;
sub new { bless {}, shift }
my $x = 1;
sub to_string {
die if 5 == $x;
return $x++;
}
}
my $sarah = Arnie->new;
print $sarah while 1;
I suspect this is one of many types of problems which would make such an approach difficult to use for Perl.
Action at a distance
ziggy on 2006-02-14T21:01:08
Let's ignore source filters, because presumably any proof to see if a program halts will necessarily happen on the post-filtered source. (This is regardless of whether you're talking about C+cpp, Lisp + Macros or Perl + Source Filters.) I'm not familiar with any of the formal theories here, but in your (somewhat contrived) example, it should be reasonably easy to tell that the second Perl program terminates. The hard part is when your termination conditions are derived from side effects, like environment variables, time of day, or input to your program. (Not the kind of thing you need to worry about in a device driver.)
Finding degenerate cases in Perl is actually simpler than what you posit, because of tied variables. Because any variable can be tied, it's not immediately obvious if a program will halt, because a tied method could call
die, which will be handled by an
eval {} three or four levels up the stack (or not). Then again, it may not be a tied variable; it may be a regular variable, or tied some of the time. Then there's objects, duck typing, reblessing, etc.
Tcl has the same problem, with variable traces. The principle is similar to a tied variable -- any variable can have a "trace" function attached to it that will fire whenever the variable is updated. Great if you have a few magic variables that trigger a GUI update whenever they're modified. Horrible whenever you're trying to capture full Tcl semantics, or apply any kind of reasoning on the behavior of some random Tcl program.
It's (currently) an either-or decision: either you take the benefit from increased dynamism and flexibility, or you open yourself up to the
possibility of benefits from automated reasoning about your program. (Note that decidability and type safety theorems don't map particularly well to C at the moment.)
All in all, these kinds of tools would be nice to have, but they aren't a compelling reason to stop using Perl.
Re:Action at a distance
Dom2 on 2006-02-15T07:32:01
This seems similar to the arguments for static typing -- it lets you build a better IDE because you can reason about the code (eg: what methods does this object have?) In a dynamic language like Perl, that's much, much harder. But it does mean that interfaces in Perl tend towards being simpler and not requiring an IDE, unlike Java.
-Dom
That would still be useful in perl
TeeJay on 2006-02-15T10:01:50
I think you're claiming that terminator wouldn't be of use in perl programming because of some obscure edge cases.
In production code where I'd want to use something like this I work to minimise such edge cases (which simplifies maintainence and debugging), and would rather have to look through false alarms and check them than not have any help with a halting bug or infinite loop.
