Setting Execution Limits

Distinguish budget, termination, and Div.

11.1 A program can still run forever

General loops and recursion may not terminate. Tauto reflects this possibility with the Div effect. However, the absence of Div is not a guarantee that execution will finish in every environment without exhausting time or memory.

11.2 Interrupt execution with a step budget

ch11-budget.taut

let value := handle {
  budget(steps: 3) { 7 }
} with {
  exceeded(info), k => info.more(100)
}
perform show("value", value)

// Grant additional evaluation steps when the local budget is exhausted.

Execution result

value = 7

value = 7

budget(steps: n) { body } gives evaluation a step budget. When it runs out, exceeded occurs. Its handler can grant more steps, as in info.more(100), and continue execution.

Step counting is implementation-dependent. steps: 3 does not mean “execute exactly three instructions.”

There are also limits outside a budget. If the overall limit set by tauto run --steps N is reached, execution stops as “interrupted,” rather than performing exceeded.

tauto run --steps 5 ch11-budget.taut

ch11-budget.taut: interrupted: the step limit ran out

11.3 Adding budget does not prove termination

Repeated calls to info.more can keep a nonterminating computation running indefinitely. Time and memory limits imposed outside the implementation, and operating-system termination requests, are also distinct from exceeded.

When reasoning about safety, distinguish:

Static properties expressed by types and effects.
Dynamic limits imposed by step budgets.
Resource limits enforced by the host.

Exercise 11.1: Why does wrapping an infinite computation in budget fail to prove that the computation itself terminates?