matijapretnar/eff

Exception handler semantics regarding multi-shot

Closed this issue · 6 comments

I'm having a hard time to figuring out, in case the computation is spawning multiple threads, what should happen when one or more of those threads is throwing an exception? If the exception handler is provided after the fork, that feels quite normal, but if the exception handler is provided before the fork, should the thrown exceptions trigger multi-shots of the exception handler ?

I kinda see traditional wisdom is to prevent exceptions from crossing fork boundaries, but that seems guilty for go statement considered harmful.

I wonder how this is reasoned with algebraic effects based exception handling, some clue please ?

Btw I don't know either if a finally block can be implemented as an effect, and if it can be implemented, I feel it even more subtle to have a multi-shot finally block.

On the other hand, I feel the said goto semantic of go statement can be fixed if exceptions can cross fork boundaries and properly settled.

Since the result type of exceptions is empty, this is what the continuation in the exception handler expects. However, since the handler cannot produce a value of this type, there is no way to resume the continuation. So the first exception in a thread aborts the rest, and no further exceptions can occur. If you had resumable exceptions (eg. just issuing a warning but allowing one to resume to continuation) then multiple warnings would be issued.

the first exception in a thread aborts the rest

Do you mean the first exception in one of the spawned threads, will abort all its sibling threads?

Yes, if the exception escapes the scheduling handler, everything underneath it is discarded. However, the scheduling handler can also have a special case for handling exceptions in the running thread. One such sensible handler would discard the current continuation (because it cannot resume it for the reasons above), but could resume one of the other sibling threads waiting in the queue.

but could resume one of the other sibling threads waiting in the queue.

I would make sure I understand you correctly, is this in the case that multiple coroutines are scheduled on a single thread?

But I'm thinking about hardware based threads running in true parallel, do you think the handling would be different in that case?

Indeed, I was thinking of a single-threaded hardware implementation. I honestly don't know what to do with multiple threads - perhaps you can ask Multicore OCaml people, who've been dealing with algebraic effects on multiple cores?

FYI I did an experimental implementation and the resulting semantics seems satisfactory.
It runs on GHC's lightweight threads, can be considered true parallel in some sense.

Đ: {
Đ|  1:   method asyncRisk(n) {
Đ|  2:     defer {
Đ|  3:       ;-1<| 'async defer cleanup #' ++ n
Đ|  4:     }
Đ|  5: 
Đ|  6:     throw '!AsyncFailure#' ++ n
Đ|  7: 
Đ|  8:     ;-1<| 'not a chance to see this'
Đ|  9:   }
Đ| 10: 
Đ| 11:   {
Đ| 12:     for i from range(3) do {
Đ| 13:       go asyncRisk(i)
Đ| 14:     }
Đ| 15:   } $=> {  # this exception handler will be triggered to run
Đ| 16:     # in multiple forked threads (forkees), but its recover
Đ| 17:     # continuation will only run by the thread installed it,
Đ| 18:     # i.e. the forker thread.
Đ| 19:     { exc } -> {
Đ| 20:       ;-1<| 'handling ' ++ exc
Đ| 21:     }
Đ| 22:   }
Đ| 23: 
Đ| 24:   # too obviously, but it could really go wrong with,
Đ| 25:   # a continuation based implementation
Đ| 26:   ;-1<| 'this should run only once by forker thread'
Đ| 27: 
Đ| 28:   for _ from console.everyMillis(10) do { break }
Đ| 29: 
Đ| 30:   ;-1<| 'all done.'
Đ| 31: }
 🐞 ThreadId 3 👉 <console>:26:4 ❗ this should run only once by forker thread
 🐞 ThreadId 45 👉 <console>:20:8 ❗ handling !AsyncFailure#0
 🐞 ThreadId 45 👉 <console>:3:8 ❗ async defer cleanup #0
 🐞 ThreadId 46 👉 <console>:20:8 ❗ handling !AsyncFailure#1
 🐞 ThreadId 46 👉 <console>:3:8 ❗ async defer cleanup #1
 🐞 ThreadId 47 👉 <console>:20:8 ❗ handling !AsyncFailure#2
 🐞 ThreadId 47 👉 <console>:3:8 ❗ async defer cleanup #2
 🐞 ThreadId 3 👉 <console>:30:4 ❗ all done.
Đ: 
Đ: 
Đ: # Note:
Đ: # we use negative log level to trigger debug trace, so thread
Đ: # id is shown as well;
Đ: # and the minus sign (-) will parse as infix subtraction
Đ: # operator if following some expression, so we prefix it with
Đ: # a semicolon (;) to disambiguate;
Đ: # then `;-1<| 'xxx'` reads `trace "xxx"` with extra info
Đ: