[mercury-users] Native garbage collector for Mercury

[Jonathan Martin]

> This argument also tells us why we shouldn't use a spell-checker, at least
> not for real documents, until it can detect _every_ spelling mistake.
> Tools like spell-checkers and termination analysers can increase our
> level of confidence in documents/programs without proving the absence
> of errors.

I'm not saying that we shouldn't use termination analysers until they
are well developed.  I believe that some bugs in the Mercury compiler
were found directly as a result of using its termination analysis -
proof enough that even a simple termination analysis can be useful
(and a more sophisticated one could be even more useful).  But the
original suggestion was that a server should only allow programs to
run that can be proven terminating, in which case the answer to the
question "Does this query terminate?" would be required to be "yes",
not "I'm 99% confident".

> Even though the question "Does this query terminate?" still
> has the answer "Don't know", there are other questions such as "How much of
> my program do I need to look at to work out why this query didn't terminate?"
> that have different answers after termination analysis.

But if the termination analysis is only 50% 'effective', say, and the
answer before is 100,000 lines of code and the answer after is 50,000
lines of code, then is there any real difference between the two?

Basically, I just disagree with the claim that "Mercury's termination
analysis is already very good".  I might agree if it could prove 90%
of the compiler terminating, say.  It would certainly be interesting
to see how much it could prove terminating with the following
additions.

> Of the predicates for which the compiler can't prove termination,
> a large proportion have their termination controlled by integer
> loops. It probably won't take much to extend the analysis to
> cope with these sorts of situations. Higher order is another case
> for which the current implementation just throws up its hands,
> but which could be handled better without requiring sophisticated
> changes to the current analysis.

Are these currently being incorporated into the analyser?


Jonathan Martin		jcm93r at ecs.soton.ac.uk
----------------------------------------------
Department of Electronics and Computer Science
The Mountbatten Building  Room 3053
University of Southampton   S017 1BJ
----------------------------------------------