| uip | title | description | author | status | type | category | created |
|---|---|---|---|---|---|---|---|
0123 |
%loop hint: reify infinite loops as crashes |
A simple hint allows the interpreter to reify "obvious" non-terminating loops as Nock crashes. |
~ritpub-sipsyl (eamsden) |
Draft |
Standards Track |
Nock |
2024-03-25 |
A simple static hint can signal to the runtime to check for nontermination by checking if the current subject and hinted formula have a circular evaluation dependency. Since Nock crashes and non-termination are definitionally semantically equivalent, the interpreter can crash deterministically if this heuristic matches.
Implementing this hint would remove the need to manually implement such checks within Nock, enabling usecases of the %memo hint previously prevented by the need to track such state in the subject.
The %memo hint, supported by both Vere and Ares, allows algorithms to improve performance using memoization. The underlying cache for the hint is, in general, a map from subject-formula pair to result.
Some Nock programs, such as the Hoon compiler, must run complex recursive functions over arbitrary user input. These programs need memoization to be feasible. However, they also need to crash with an error when they detect non-termination. Since the programs store the state used to deduce non-termination in the subject, and this state changes each iteration, they're unable to use the %memo hint. This is a major contributor to the custom memoization jets for the Hoon compiler functions, which manually punch out holes in the subject before caching.
Non-termination and crashes are equivalent in Nock, and an interpreter choosing to report a crash is reporting that the computation would not terminate if continued. Thus, if the interpreter makes this determination, it is correct for it to crash with a stack trace. However, we do not want to check every subject-formula pair against all prior pairs in the call stack at every evaluation site (Nock 2 or Nock 9).
Nock interpreters SHOULD recognize the %loop static hint using the following (or extensionally equivalent) behavior:
- Maintain a stack of subject and formula pairs
- On entry into a
%loophinted computation:- check whether the current subject and hinted formula are already on the stack
- if so, crash
- if not, push the current subject and formula onto the stack
- On exit from the hinted computation, pop the stack
An interpreter that handles the %loop hint allows non-termination detection state to be removed from the subject and instead stored in an interpreter cache. Any algorithm that currently maintains a stack-like structure in order to catch input for which it would naively not terminate can simply be hinted %loop instead, and can also leverage %memo as well.
If %loop was used as described, algorithms which depend on it to detect obvious nontermination would instead actually spin forever in interpreters which do not support the hint. Existing Kelvin-version guarding should suffice to prevent this case.
TBD
Semantically: this proposal presents no security concerns as the kelvin-guarding mechanisms already in place should prevent differential event replay from algorithms relying on its function. Further, crashes and infinite loops are definitionally equivalent in Nock.
Operationally: programs relying on this hint could be made to consume large amounts of memory in a manner not obvious by examining the type or contents of the subject, as the memory would have no direct corresponding noun in the subject.
Copyright and related rights waived via CC0.