Cleanup mechanism for ISO Prolog

Ulrich Neumerkel, 2009-07-02 (Version history)
This draft is based on Paulo Moura's draft core 8.15.5 13211-1:2006 of 2008-11-17. It is intended to replace 8.15.5 in it. References refer to 13211-1:1995.

Contributors

Bart Demoen (Belgium). Paulo Moura (Portugal). Richard O'Keefe (New Zealand). Jeffrey Rosenwald (USA). Markus Triska (Austria).

8.15.5 setup_call_cleanup/3

This control construct allows managing resources related to the execution of a goal. It provides protected setup and performs cleanup as soon as the goal has completed execution.
NOTE — A built-in predicate call_cleanup/2 is implemented in many existing processors to provide similar functionality as setup_call_cleanup/3. It is often used to free temporary resources. In the presence of interrupts (7.12 note c), call_cleanup/2 can cause leakage of resources: A processor receiving interrupts between resource allocation and call_cleanup/2 is unable to free the resource timely. For this reason, setup_call_cleanup/3 protects goals in a separate argument.

8.15.5.1 Description

setup_call_cleanup(Setup, Goal, Cleanup) is true iff call(Setup), call(Goal) is true, and Cleanup is not replaced by throw/1.
  1. Setup is executed protected from interrupts.
  2. After the cleanup handler is installed for a solution of Setup, the Goal is called as in call(Goal) with the cleanup handler present.
  3. The cleanup handler is called exactly once at one of the following moments:
    1. When Goal has completed execution normally.
      The precise moment is implementation dependent within the interval defined by the following bounds.
      • after calling Goal
      • after the last solution of Goal, if applicable
      • after the last observable effect of Goal, if applicable
      • up to the failing of Goal

      NOTE — The implementation dependence is due to the varying ability of Prolog processors to detect determinism. For example, a particular processor may execute a goal call((call(Goal);fail)) as call(Goal) and vice versa.

    2. When Goal or the continuation of Goal executes a throw/1 (explicitly or implicitly — 7.8.9 a or b), whose corresponding call of catch/3 is above Goal.
      After executing Cleanup, the "ball" of throw/1 will be passed, regardless of the outcome of Cleanup.

      NOTE — As a consequence, the "ball" of Cleanup is lost in case Cleanup executes another throw/1.

    3. When the continuation of Goal executes a cut (explicitly or implicitly) that concerns the cutparent of Goal.
      After the cut has been executed, Cleanup is called in the place of the cut. A cut is performed implicitly for (->)/2 - if-then (7.8.7), (;)/2 - if-then-else (7.8.8), (\+)/1 (8.15.1), once/1 (8.15.2).
  4. Cleanup is called as once(Cleanup). Failure of Cleanup is ignored. An explicit or implicit throw/1 is ignored for c2. Otherwise (c1 or c3), it is passed to the next matching catch/3.

    Cleanup shares bindings and variables with Setup, Goal and the continuation. The bindings of Setup are always present. No further bindings are present in c2 and at the latest moment of c1. In c2, and in the earliest moment of c1, all bindings are present at the time of calling the cut. All other cases of c1 are implementation dependent.

    A processor may restrict execution of Cleanup in an implementation dependent manner. E.g., a processor may restrict the handling of interrupts within Cleanup or limit resource consumption.

8.15.5.2 Template and modes

setup_call_cleanup(+callable_term,+callable_term, +callable_term)

8.15.5.3 Errors

a) Setup is a variable.
— instantiation_error.
b) Setup is neither a variable nor a callable term— type_error(callable,Setup).
c) Setup is a callable term that is not permitted due to an implementation defined restriction
— representation_error(setup_goal).
d) For a solution of Setup, Goal is a variable
— instantiation_error. The Cleanup is still executed.
e) For a solution of Setup, Goal is neither a variable nor a callable term
— type_error(callable, Goal). The Cleanup is still executed.
f) For a solution of Setup, Cleanup is a variable
&mdash instantiation_error. Goal is not executed.
g) For a solution of Setup, Cleanup is neither a variable nor a callable term
— instantiation_error. Goal is not executed.

8.15.5.4 Examples

In the following, write/1 outputs using standard operators (6.3.4.4, table 7). Unique variables are written as _ which is one possible way to realize the implementation dependent manner of 7.10.5 a)

The different outcomes (labeled either/or) are due to the implementation dependence in c1.

setup_call_cleanup(fail, _, _).
   Fails.  Neither Goal nor Cleanup is executed.

setup_call_cleanup(true, throw(unthrown),_).
   Instantiation error.

setup_call_cleanup(true, true, ( true ; throw(x) )).
   Succeeds. No system error.

setup_call_cleanup(true, X = 1, X = 2).
   Succeeds, unifying X = 1.

setup_call_cleanup(true, true, X = 2).
   Succeeds, unifying X = 2.

setup_call_cleanup(true, X=true,X).
   Instantiation error.

setup_call_cleanup(X=throw(ex), true, X).
   System error due to uncaught ex.

setup_call_cleanup(true, true, fail).
   Succeeds.

setup_call_cleanup(S=1, G=2, C=3).
   Either: Succeeds, unifying S = 1, G = 2, C = 3.
   Or:  Succeeds, unifying S = 1, G = 2. Fails
   on backtracking.

setup_call_cleanup((S=1;S=2), G=3, C=4).
   a) Either: Succeeds, unifying
              S = 1, G = 3, C = 4.
          On backtracking proceed to b)
      Or: Succeeds, unifying S = 1, G = 3.
          On backtracking proceed to b)
   b) Either: Succeeds, unifying
              S = 2, G = 3, C = 4.
      Or: Succeeds, unifying S = 1, G = 3.
          Fails on backtracking.

setup_call_cleanup(S=1,G=2,write(S+G)).
   Succeeds, unifying S = 1, G = 2.
   Either: outputs '1+2'
   Or: outputs on backtracking '1+_',
   prior to failing.
   Or (?): outputs on backtracking '1+2',
   prior to failing.

setup_call_cleanup(S=1,(G=2;G=3),write(S+G)).
   Succeeds, unifying S = 1, G = 2.
   On backtracking, succeeds unifying S = 1 and G = 3.
   Either: outputs '1+3'
   Or: on backtracking outputs '1+_' prior to failing
   Or (?): on backtracking outputs '1+3' prior to failing.

setup_call_cleanup(S=1,G=2,write(S+G>A+B)), A=3, B=4.
   Succeeds, unifying S=1,G=2,A=3,B=4.
   Either:  Outputs one of the following before succeeding
   1+2>_+_.   Disputable: 1+2>3+_.   1+2>3+4.   1+2>_+4.
   Or: outputs one of the above outputs on backtracking
   prior to failing.

setup_call_cleanup(S=1,(G=2;G=3,throw(x)),write(S+G)).
   Succeeds, unifying S = 1, G = 2.
   On backtracking, outputs '1+_' prior
   to system error due to uncaught x.

setup_call_cleanup(open(f,read,S),read(S,X),close(S)).
   Opens file f for reading, reads a term and closes the file.
   Succeeds, unifying S with the term read.
   The file is closed, either immediately or on backtracking.
   In any case, even if there is an error in read, the
   file will be closed.

Events in the continuation

setup_call_cleanup(S=1,(G=2;G=3),write(S+G>B))), B=4, !.
   Outputs '1+2>4'. Succeeds, unifying S = 1, G = 2, B = b.

setup_call_cleanup(S=1,G=2,write(S+G>B)),B=3,!.
   Either:  Outputs '1+2>3'. Succeeds, unifying
      S = 1, G = 2, B = 3.
   Or: Outputs '1+2>_'. Succeeds, unifying
      S = 1, G = 2, B = 3.

setup_call_cleanup(S=1,(G=2;fail),write(S+G>B)), B=3, !.
   Same as above.

setup_call_cleanup(S=1,(G=2;S=2),write(S+G>B)), B=3, !.
   Same as above.

setup_call_cleanup(S=1,(G=2;G=3), write(S+G>B)), B=4, throw(x).
   Outputs '1+_>_'. system_error due to uncaught x.

setup_call_cleanup(S=1,(G=2;G=3), write(S+G>B)), B=4, !, throw(x).
   Outputs '1+2>4'. system_error due to uncaught x.

Multiple exceptions

catch(setup_call_cleanup(true,throw(goal),throw(cl)), Pat, true).
   Succeeds unifying Pat = goal.

catch(( setup_call_cleanup(true,(G=1;G=2),throw(cl)), throw(cont)), Pat, true).
   Succeeds unifying Pat = cont.

Implementation status

SICStus
call_cleanup/2 since 1997. (origin) Open: setup_call_cleanup/3 missing. Different handling of multiple simultaneous exceptions.
SWI
almost fully compliant since Autumn 2007. Open: unwinding for exceptions from aside. Instantiation error for unbound Cleanup. There is only one call to Cleanup (Manual is correct though).
YAP-6
almost fully compliant since June 2009. Open: instantiation error for unbound Cleanup.
Other Prologs
(currently, 2009-07) XSB, B-Prolog have call_cleanup/2 but do not guarantee that Cleanup will be called eventually.