Problems with 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.
Exceptions as presented in the paper rely on a global property of the operational semantics, essentially that there is only one control stack per process. However, the parallel evaluation of pairs creates multiple control stacks that are related by juxtoposition in the ordered context. Therefore, the two cannot be combined without problems, as demonstrated in this example.
One possibility for addressing this problem is given in par-exn2.olf.
Parallel evaluation for pairs (Figure 5), plus unit
epair1 : eval(pair E1 E2) ->> comp(pair1) • eval(E1) • eval(E2).
epair2 : comp(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)
eraise : eval(raise) ->> fail.
epop : comp(F) • fail ->> fail.
ecatch : catch(E2) • fail ->> eval(E2).
eret : catch(E2) • return(V) ->> return(V).
If there is an exception in the first branch of a pair's evaluation, then the error will "abandon" the stack belonging to the second branch, eagerly propogating the error before the second branch has even necessarily finished evaluating.
If there is an exception in the second branch, it will be "blocked" by the return in the first branch and execution will become stuck.