[Caml-list] Re: Race conditions with asynchronous exceptions in standard library

[Caml-list] Re: Race conditions with asynchronous exceptions in standard library

[oleg]

Just a few clarifications. The posted Queue code gives the
segmentation fault when compiled with ocamlopt without threads. When
bytecode-compiled, the code is accidentally safe, at least on my
platform. The bytecode interpreter checks for signals when executing
any of the `application' instructions or popping the exception
handler. It just so happens that no function application instructions
were executed in the critical section of the standard library Queue
code. That is a mere accident however: a new version of the standard
library (or Batteries) might add some sort of debugging printing; or
the code generation will change to emit calls to auxiliary, debugging
or tracing facilities.

Incidentally, comments in the bytecode interpreter justify a particular
piece of code by saying that a signal handler may raise an
exception. Thus Xavier Leroy certainly did allow for such signal
handlers, at least as a possibility.

Mark Shinwell wrote:
> Specifically in the case of signal handlers, I would recommend
> restricting processing in them to an absolute minimum, and in
> particular not throwing exceptions.

If this is the consensus, to which INRIA assents, it ought to be
written in the user documentation, alongside of other warnings (like
living in harmony with GC). At the same time, one should describe the
recommended solution to Yit's original problem, to interrupt a
long-running library function with a timeout.

[Caml-list] Race conditions with asynchronous exceptions in standard library

[Khoo Yit Phang]

[-- Attachment #1: Type: text/plain, Size: 3038 bytes --]

Hi all,

I recently discovered a race condition when asynchronous exceptions, i.e., exceptions raised by signal handlers, are used with the DelimCC library. After consulting with Oleg Kiselyov, he realized that the problem with asynchronous exceptions is far more pervasive than I had originally thought. For example, the following program, using only the standard OCaml library, leads to a segfault:

> let q = Queue.create ();;
> 
> let () =
>     let en = ref false in
>     Sys.set_signal Sys.sigalrm (Sys.Signal_handle (fun _ -> if !en then raise Exit));
>     ignore (Unix.setitimer Unix.ITIMER_REAL { Unix.it_interval=1e-6; Unix.it_value=1e-3 });
>     while true do
>         try
>             en := true;
>             Queue.add "a" q;
>             en := false;
>             ignore (Queue.pop q)
>         with Exit ->
>             en := false;
>             if Queue.length q > 0 then prerr_endline "Non-empty";
>             assert (let len = Queue.length q in len = 0 || len = 1);
>             Queue.iter print_string q;
>             Queue.clear q;
>     done

The problem occurs in Queue.ml:

> let create () = {
>   length = 0;
>   tail = Obj.magic None
> }
> 
> let add x q =
>   q.length <- q.length + 1;
>   (* asynchronous exception occurs here *)
>   ...

When Queue.add is interrupted by an exception immediately after the length is updated, the length becomes inconsistent with the tail, and subsequent operations such as Queue.iter will attempt to operate on Obj.magic None, leading to the segfault.

Probably much of the standard library is similarly susceptible to such races, particularly the parts that operate on mutable data. These mostly lead to less dramatic consequences than segfaults, but are still seemingly random errors such as corrupted data or violated invariants.

For DelimCC, my solution was to provide a pair of C functions, mask_signals and unmask_signals, to bracket operations that are unsafe under asynchronous exceptions, using sigprocmask to suppress signal handling between them. However, since this requires access to OCaml's signal handling internals (caml_process_pending_signals and caml_signals_are_pending) to flush pending signals, it would be great to have mask_signals and unmask_signals or something similar in the standard library, so as to make it easier to develop libraries that are safe under asynchronous exceptions. (For reference, Haskell has seen this and other issues with asynchronous exception and implemented a similar solution, see http://hackage.haskell.org/trac/ghc/ticket/1036.)

Another option would be to simply warn against or disallow signal handlers that raise exceptions, but that seems less useful, e.g., it would make it hard to interrupt a long-running library function with a timeout.

We look forward to hearing what the official fix or guideline for handling asynchronous exception will be, for the standard library, third-party libraries, as well as applications.


Thank you,

Yit
July 5, 2011

[-- Attachment #2: Type: text/html, Size: 7208 bytes --]

[Caml-list] Re: Race conditions with asynchronous exceptions in standard library

[Khoo Yit Phang]

Hi,

As Oleg clarified, this issue arises even without threads, in native code as well as bytecode executions (with differences due to when signals are processed). Let me further distinguish several scenarios:


1) Writing third-party libraries that are safe under asynchronous exceptions

With some care, it is possible to write third-party Ocaml libraries that are safe even if asynchronous exceptions occur. One way would be to write in purely functional style, another would be to fork and execute a separate process, yet another would be to carefully arrange the code to avoid signals (as Fabrice suggested for queue.ml). However, I don't believe it would be possible to implement, for example, memoization or hashconsing, in a purely functional manner or by forking; forking would be impractical to implement libraries such as imperative graph data structures; and it may not always be possible to rearrange the code in a safe manner.

Instead, I propose to provide signal masking functions (sigprocmask), e.g., mask_signals and unmask_signals, to bracket regions of code where signals should not be processed. It would be great if these were part of the standard library, since they require some knowledge of how the Ocaml runtime handles signal processing, in particular, to flush signals that have been recorded by the runtime, but not yet dispatched, before entering the signal-masked code region.

(Unix.sigprocmask may work, though it has a higher overhead since the signal mask is encoded as a list.)

Another reason to have this in the standard library would be to support reentrancy, i.e., of a signal-masked code region calling another function that itself enters signal-masking, and not accidentally unmask signals prematurely (see http://hackage.haskell.org/trac/ghc/ticket/1036 for example). Having libraries implement signal-masking in an ad-hoc manner is likely to lead to such mistakes.



2) Writing applications that are safe that use libraries that are unsafe under asynchronous exceptions

Even if libraries are unsafe, applications can be written safely by carefully wrapping those library functions with signal-masking functions as above.



3) The OCaml standard library

I don't think that the OCaml standard library needs to be changed, if applications can wrap these libraries as above. It would be useful to document which libraries are safe to use under asynchronous exceptions, if only for a small performance consideration. Alternatively, if signal masking isn't available, then it would be useful to document the hazards of asynchronous exceptions under Sys.signal and similar functions.

I may have missed it, but does the OCaml manual explain exactly where signals are processed (other than reading the source code)? If so, it would also be useful to link to it from Sys.signal and friends.


Yit
July 6, 2011

Re: [Caml-list] Re: Race conditions with asynchronous exceptions in standard library

[Gerd Stolpmann]

Well, such a function for temporarily masking the execution of ocaml
signal handlers would be useful for something else, at least. The way
multi-threading is implemented in the runtime is coupled with signals.
When masking signals you would also get the ability to mask thread
switches. That would be a very cheap way for getting critical sections,
and it would also work in contexts where you normally cannot have
critical sections, e.g. in GC finalizers.

Generally I don't think it is possible to catch all code blocks that are
async-unsafe, and to fix them by masking signals. This is a really heavy
constraint. Also, there are execution flows that could not be
effectively handled by just masking signals, e.g. callbacks when you've
already turned off signals, but are are sure it is now safe to allow
them again for the time of the callback. At least, it sounds like a very
messy coding style.

I fear for a working and scalable implementation you also need STM - you
can then just roll the transaction back, and all the state
inconsistencies are gone. (Well, maybe this is not what you want - all
the results from the interrupted computation would be away, too.)

Gerd

Am Mittwoch, den 06.07.2011, 19:40 -0400 schrieb Khoo Yit Phang:
> Hi,
> 
> As Oleg clarified, this issue arises even without threads, in native code as well as bytecode executions (with differences due to when signals are processed). Let me further distinguish several scenarios:
> 
> 
> 1) Writing third-party libraries that are safe under asynchronous exceptions
> 
> With some care, it is possible to write third-party Ocaml libraries that are safe even if asynchronous exceptions occur. One way would be to write in purely functional style, another would be to fork and execute a separate process, yet another would be to carefully arrange the code to avoid signals (as Fabrice suggested for queue.ml). However, I don't believe it would be possible to implement, for example, memoization or hashconsing, in a purely functional manner or by forking; forking would be impractical to implement libraries such as imperative graph data structures; and it may not always be possible to rearrange the code in a safe manner.
> 
> Instead, I propose to provide signal masking functions (sigprocmask), e.g., mask_signals and unmask_signals, to bracket regions of code where signals should not be processed. It would be great if these were part of the standard library, since they require some knowledge of how the Ocaml runtime handles signal processing, in particular, to flush signals that have been recorded by the runtime, but not yet dispatched, before entering the signal-masked code region.
> 
> (Unix.sigprocmask may work, though it has a higher overhead since the signal mask is encoded as a list.)
> 
> Another reason to have this in the standard library would be to support reentrancy, i.e., of a signal-masked code region calling another function that itself enters signal-masking, and not accidentally unmask signals prematurely (see http://hackage.haskell.org/trac/ghc/ticket/1036 for example). Having libraries implement signal-masking in an ad-hoc manner is likely to lead to such mistakes.
> 
> 
> 
> 2) Writing applications that are safe that use libraries that are unsafe under asynchronous exceptions
> 
> Even if libraries are unsafe, applications can be written safely by carefully wrapping those library functions with signal-masking functions as above.
> 
> 
> 
> 3) The OCaml standard library
> 
> I don't think that the OCaml standard library needs to be changed, if applications can wrap these libraries as above. It would be useful to document which libraries are safe to use under asynchronous exceptions, if only for a small performance consideration. Alternatively, if signal masking isn't available, then it would be useful to document the hazards of asynchronous exceptions under Sys.signal and similar functions.
> 
> I may have missed it, but does the OCaml manual explain exactly where signals are processed (other than reading the source code)? If so, it would also be useful to link to it from Sys.signal and friends.
> 
> 
> Yit
> July 6, 2011
> 


-- 
------------------------------------------------------------
Gerd Stolpmann, Bad Nauheimer Str.3, 64289 Darmstadt,Germany 
gerd@gerd-stolpmann.de          http://www.gerd-stolpmann.de
Phone: +49-6151-153855                  Fax: +49-6151-997714
------------------------------------------------------------