This work begins during the development of a parser for the new syntax introduced with the ReScript language. Learning from previous experience, it was decided to avoid parser generators, and go instead for a hand-crafted parser. In this way, the parser could be optimized for performance, be more maintainable, and most importantly give much more flexibility with error messages.
The new parser delivered on the promises, though a new issue appeared during live testing. The laptop would get hot once in a while, and only improve after re-starting the editor. Not all the time, but often enough to notice. The problem was an infinite loop in the parser, triggered by unexpected character combinations introduced while editing and never encountered in automated tests. It took a while to reproduce the issue and locate a mistake in the parser code, which was then fixed. Then, the next week it happened again, and again.
Infinite loops are a manifestation of one of the best known problems in computer science. The halting problem, formulated by Alan Turing in 1936. In a nutshell, computers cannot detect infinite loops. So over 80 years before, Turing proved that our problem is not solvable.
Even though the problem is not solvable in full generality, there is academic research, and some industrial tools, dedicated to solving some instances of the problem. However, no tool would apply to our use case. We had about 20000 lines of code consisting essentially of several hundreds mutually recursive functions, and functions passed as arguments to other functions.
An analysis tool was built, using this specific parser as a starting point. The tool aims to provide value to the developer by finding infinite loops, without requiring specialist knowledge or disrupt the development flow. On the entire parser, it runs in under 200 milliseconds before reporting the results. Since deploying the tool on every build, no new infinite loops were introduced in the codebase under active development.
This note describes the technology that underpins the termination analysis tool, which is now part of the open-source package reanalyze. There is no claim that the same analysis will be effective on every program. After all, Turing has proven that it is impossible. However, we believe that it has application beyond the construction of parsers, and would love to explore new applications in future.
let loop = n =>
while n.contents > 0 {
n := n.contents - 1
print_int(n.contents)
}Does this program terminate for all integers n? How does one reason about it?
The typical argument goes as follows: consider a progress function on the state, and check that it's not possible to make progress infinitely often. In the example, the progress function is the distance from n.contents to zero. Each iteration of the loop decreases the number, hence the distance. The distance cannot decrease infinitely often, as it would eventually go below 0. Therefore, the program must terminate.
Consider now a variant of the example written as a recursive function:
let rec loop = n =>
if n.contents > 0 {
n := n.contents - 1
print_int(n.contents)
loop(n)
}The program follows a pattern: there is a recursive function, and some progress happens in its body. The termination argument becomes the following: every execution of the loop body makes progress. So does the program terminate?
If, in an execution of the program, loop is called infinitely often, then progress is made infinitely often. But making progress infinitely often is not possible. Therefore, loop is not called infinitely often. Therefore, the program always terminates.
We now go through the termination argument for the recursive example, and analyze the implications. There is a global character to the argument: "the whole program terminates". But there is also a local sub-argument: "function loop is not called infinitely often".
Based on this, there is a simple strategy for ensuring termination: ban while and for loops, and check the recursive functions. Namely, for each recursive function, check that it is not called infinitely often.
If one focuses on logal sub-arguments, something interesting happens: the termination problem is now broken into a set of sub-problems, one for each function. Also, it's an opening for pragmatism. Wearing a pragmatic hat, one would expect that most non-trivial programs cannot be proven terminating as a whole, for the simple fact that they don't always terminate (even those that by design should).
What to do then when presented with a program which, as a whole, does not terminate? As developers, we might know/suspect of a particular way it could fail to terminate. And it might be worth spending energy investigating that one important way it might fail to terminate, not all the possible ways. Breaking up the termination problem allows to do exactly that: if the program is broken into recursive functions, and there is one function (or more) that represents the particular way of non-terminating we are interested in, then we can analyze that function in isolation.
The sub-problem of interest then becomes: given a set of recursive functions, check that none of them is called infinitely often. This might involve several progress measures, e.g. even one per recursive function.
Newton's method is an algorithm in numerical analysis to gradually approximate the roots of a real-valued function.
let newton = (~f, ~fPrimed, ~initial, ~threshold) => {
let current = ref(initial)
let iterateMore = (previous, next) => {
let delta = next >= previous ? next - previous : previous - next
current := next
!(delta < threshold)
}
@progress(iterateMore)
let rec loop = () => {
let previous = current.contents
let next = previous - f(previous) / fPrimed(previous)
if iterateMore(previous, next) {
loop()
} else {
current.contents
}
}
loop()
}The algorithm consists of a loop which progressively finds new approximations using the provided function f and its first derivative fPrimed, until the delta between the last two values is within a given threshold.
This is how to apply it to a 3rd degree polynomial
let f = x => x * x * x - 2.0 * x * x - 11.0 * x + 12.0
let fPrimed = x => 3.0 * x * x - 4.0 * x - 11.0
let result = newton(~f, ~fPrimed, ~initial=5.0, ~threshold=0.0003)There is an entire line of research dedicated to inferring progress measures automatically. In the above example of the Newton–Raphson method, which is parametric in the functions f and fPrimed, if an automatic inference procedure existed, it would need to independently reconstruct the theorems and proofs in Newton's_method. What this means, is that inferring a measure automatically can be extremely difficult, if at all possible.
Our analysis does not try to infer the progress measure. Instead, the user is asked to specify what they consider as progress. In the example, the annotation @progress(iterateMore) is the way to indicate that iterateMore will be considered as a progress function.
This design decision of employing user-provided annotations is both limiting and empowering. It's limiting as it removes mathematical certainty that the program terminates. It's empowering, as more liveness properties can be encoded (e.g. that a server, which does not terminate, keeps on responding to requests).
What if I want to have trust in the fact that a program terminates? First, it's possible to approach the problem gradually. One (or more) function at a time. Wearing a pragmatic hat again: it's not impossibly difficult to stare at a single function long enough, one designated as a progress function, and convince yourself that it is a valid measure. Or, you could use a theorem prover, or even write a manual proof. In any case, the pragmatic observation is that the termination function likely changes less often than the program does.
In the Newton–Raphson, the analysis assumes that iterateMore is a progress measure, and checks that the loop function terminates. The loop function cannot be called infinitely often without making progress infinitely often: because iterateMore is called every time loop is called.
Notice that there are no assumptions about termination of f or fPrimed. For what we know, they might even fail to terminate. What matters for checking the annotation is that loop does not cause non-termination by being called infinitely often. If repeated for each relevant function, whole program termination follows.
In the rest, several aspects of the analysis are illustrated though simple examples.
If you don't opt in by adding a @progress annotation, nothing is checked. No issues are reported on the following:
let rec loop = () => loop()This time, opt into termination checking with the @progress annotation (without specifying any progress functions). This time a potential infinite loop is reported.
@progress
let rec loop = () => loop()This time, an actual progress function is defined, which in this example is just a placeholder that does nothing. This can be used for quick experimentation. No warnings are reported as every infinite loop would make infinite progress as far as the analysis is concerned.
let progress = () => ()
@progress(progress)
let rec loop = () => {
progress()
loop()
}See what's wrong now? A possible infinite loop is reported.
let progress = () => ()
@progress(progress)
let rec loop = () => {
loop()
progress()
}It's possible to play a trick, and implement indirect recursion by storing a function and calling it indirectly through the reference, in the style of (Peter) Landin's knot:
let cheekyRef = ref(() => ())
@progress
let rec cheekyLoop = () => {
cheekyRef := cheekyLoop
cheekyRef.contents()
}This triggers a hygiene violation:
cheekyLoop can only be called directly, or passed as labeled argument
What's going on is that functions we opt into termination checking, such as cheekyLoop, are restricted. Storing them in a reference is not allowed. This simple restriction replaces a complex escape check, to make sure that the function is not called behind your back.
Another restriction: you can't alias a function you opted into for termination checking:
@progress
let rec loop = () => {
let l = loop
l()
}That also gives a hygiene violation error:
loop can only be called directly, or passed as labeled argument
A progress annotation on mutually recursive functions opts them all into termination checking.
This reports an infinite loop
@progress
let rec foo = () => bar()
and bar = () => foo()But this does not report:
let progress = () => ()
@progress(progress)
let rec foo = () => bar()
and bar = () => {
progress()
foo()
}That's because every infinite loop through either foo, or bar, would make progress infinitely often.
Does this always terminate?
type token =
| Int(int)
| Float(float)
| Eof
type parser = {token: token}
let next = _parser => () // consume one token, implementation omitted
@progress(next)
let rec f = parser =>
switch parser.token {
| Int(i) => g(parser) + i
| Eof => 0
| _ =>
next(parser)
f(parser)
}
and gParam = (parser, ~gFun) =>
switch parser.token {
| Int(i) => gFun(parser) + i
| _ => f(parser)
}
and g = parser => {
next(parser)
gParam(parser, ~gFun=g)
}According to the analysis, it does terminate.
This demonstrates the use of a higher-order function gParam, which is passed g via labeled argument gFun. This is one case which does not trigger a hygiene violation: functions we opt into can either be called directly or passed via labeled arguments.
Internally the analysis keeps a table of relevant functions: those that are part of a mutual recursive definition annotated with @progress, and those that receive one of these functions as argument.
Function Table
1 f: [g; _ || _ || +next; f]
2 g: +next; gParam<gFun:g>
3 gParam<gFun>: [gFun; _ || f]
The body of the functions has been stripped of all unnecessary details, such as pattern matching. Only explicit calls to relevant functions are left, including +next where + indicates a progress function. The non-determinism in the control flow is represented as [... || ... || ...], and sequential composition as ;.
The analysis proceeds by checking that no path from a function to itself exists without passing through a progress function first. In case of parametric functions such as gParam, specific instantiations are analyzed separately. For example, the instantiation gParam<gFun:g> can end up calling itself by either calling gFun, i.e. g, which calls gParam<gFun:g>, or by calling f which calls g which calls gParam<gFun:g>. In either case, progress is made, hence the analysis reports no issues.
Starting from a problem observed during the development of a hand-crafted language parser, a termination analysis was developed. The analysis is designed to be a lightweight layer on top of an existing language, and integrate with the normal development flow without requiring specialist knowledge. It is opt-in, just for the areas of code the user is interested in, and its execution time is negligible. The analysis has brought clear value by eliminating a common class of bugs during development of the parser. We believe that the technique has wider applicability, and would love to explore other application domains. Another interesting direction is the full integration with the programming language, e.g. using a form of termination types that encode the mechanisms used by the analysis engine.