Solution for combining parallel evaluation and exceptions
Robert J. Simmons, Frank Pfenning
These examples are derived from Figures 5 and 10 in
Substructural Operational Semantics as Ordered Logic Programming.
In par-exn1.olf, we describe an issue with the parallel evaluation of
pairs combined with exceptions. In this example, we modify the computation
frames to allow exceptions to deal generically with suspended parallel
computations.
Parallel evaluation for pairs (Figure 5), plus unit
Now the suspended computation created by pair evaluation is marked as
a comp2, to distinguish it from a comp waiting on only one return.
eunit : eval(unit) ->> return(unit).
epair1 : eval(pair E1 E2) ->> comp2(pair1) • eval(E1) • eval(E2).
epair2 : comp2(pair1) • return(V1) • return(V2) ->> return(pair V1 V2).
elet1 : eval(split E (λx1.λx2. E' x1 x2)) ->> comp(split1 E') • eval(E).
elet2 : eval(split1 (λx1.λx2. E' x1 x2)) • return(pair V1 V2) ->> eval(E' V1 V2).
Exceptions (Figure 10), including exceptions for comp2 frames
Because we have generically defined a suspended computation, we can
generically define what to do if the left branch, the right branch, or
both branches generate failure.
The alternative semantics that raises an exception if one branch raises an
exception and the other fails to terminate is not natural to encode in
this setting; the natural setting for such a thing would seem to be either
linear destination-passing with affine resources or some alternate logic
that can correctly deal with having a single atomic resource to the left
of two ordered contexts.
etry : eval(try E1 E2) ->> catch(E2) • eval(E1).
eraise : eval(raise) ->> fail.
ecatch : catch(E2) • fail ->> eval(E2).
eret : catch(E2) • return(V) ->> return(V).
epop : comp(F) • fail ->> fail.
epop1 : comp2(F) • fail • return(V) ->> fail.
epop2 : comp2(F) • return(V) • fail ->> fail.
epop3 : comp2(F) • fail • fail ->> fail.
The troublesome examples from before now correctly evaluate to unit.
%trace * eval(try (pair raise (pair unit unit)) unit).
eval(try (pair raise (pair unit unit)) unit)
catch(unit)•eval(pair raise (pair unit unit))
catch(unit)•comp2(pair1)•eval(raise)•eval(pair unit unit)
catch(unit)•comp2(pair1)•fail•eval(pair unit unit)
catch(unit)•comp2(pair1)•fail•comp2(pair1)•eval(unit)•eval(unit)
catch(unit)•comp2(pair1)•fail•comp2(pair1)•return(unit)•eval(unit)
catch(unit)•comp2(pair1)•fail•comp2(pair1)•return(unit)•return(unit)
catch(unit)•comp2(pair1)•fail•return(pair unit unit)
catch(unit)•fail
eval(unit)
return(unit)
%trace * eval(try (pair (pair unit unit) raise) unit).
eval(try (pair (pair unit unit) raise) unit)
catch(unit)•eval(pair (pair unit unit) raise)
catch(unit)•comp2(pair1)•eval(pair unit unit)•eval(raise)
catch(unit)•comp2(pair1)•comp2(pair1)•eval(unit)•eval(unit)•eval(raise)
catch(unit)•comp2(pair1)•comp2(pair1)•return(unit)•eval(unit)•eval(raise)
catch(unit)•comp2(pair1)•comp2(pair1)•return(unit)•return(unit)•eval(raise)
catch(unit)•comp2(pair1)•return(pair unit unit)•eval(raise)
catch(unit)•comp2(pair1)•return(pair unit unit)•fail
catch(unit)•fail
eval(unit)
return(unit)
%trace * eval(try (pair (pair raise unit) (pair unit raise)) unit).
eval(try (pair (pair raise unit) (pair unit raise)) unit)
catch(unit)•eval(pair (pair raise unit) (pair unit raise))
catch(unit)•comp2(pair1)•eval(pair raise unit)•eval(pair unit raise)
catch(unit)•comp2(pair1)•comp2(pair1)•eval(raise)•eval(unit)•eval(pair unit raise)
catch(unit)•comp2(pair1)•comp2(pair1)•fail•eval(unit)•eval(pair unit raise)
catch(unit)•comp2(pair1)•comp2(pair1)•fail•return(unit)•eval(pair unit raise)
catch(unit)•comp2(pair1)•fail•eval(pair unit raise)
catch(unit)•comp2(pair1)•fail•comp2(pair1)•eval(unit)•eval(raise)
catch(unit)•comp2(pair1)•fail•comp2(pair1)•return(unit)•eval(raise)
catch(unit)•comp2(pair1)•fail•comp2(pair1)•return(unit)•fail
catch(unit)•comp2(pair1)•fail•fail
catch(unit)•fail
eval(unit)
return(unit)