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

[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 --]

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

[Mark Shinwell]

On Tue, Jul 05, 2011 at 11:26:52PM -0400, Khoo Yit Phang wrote:
> 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 *)
> >   ...
[snip]
> 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.

I'm presuming this is native code.  Are you compiling with or without the
Caml threads library?

If using the threads library, reception of a signal will cause it to be noted
down, and the user-defined signal handler written in Caml will be executed
later.  "Later" is difficult to pin down in words, but it should be the case
that if you have a section of code which does not involve any allocation nor
calls to any functions which drop the runtime lock, then it will never be
interrupted by the execution of a signal handler.  Indeed, it will also never
be interrupted by a context switch between Caml threads, so you can get
thread safety guarantees this way.  As far as user code goes, I believe the
things you have to think about in the two cases of raising an exception from
a signal handler and experiencing a context switch between Caml threads are
the same.

Establishing whether a particular section of code is atomic in this
regard---let us just say "thread safe"---might involve reading the assembly
code.  (I've wondered in the past about a construct which could be used to
indicate that a section is required to be atomic, and the compiler would check
it.)  I think it is clear that [Queue.add] is not thread safe.  The reason is
due to the two record allocations in the code, one of which is:

  let add x q =
    q.length <- q.length + 1;
                                  <------- signal happens here
    if q.length = 1 then
      let rec cell =
                                  <------- Caml signal handler executed here
                                           since the record allocation might
                                           trigger a garbage collection
      {
        content = x;
        next = cell
      ...

It isn't clear to me that it is reasonable to assume all libraries are thread
safe.  Perhaps the documentation needs improving in this area.  Specifically
in the case of signal handlers, I would recommend restricting processing in
them to an absolute minimum, and in particular not throwing exceptions.  The
code will be easier to think about that way.  If you must throw an exception,
you have to ensure that any data structure which you rely on in the exception
handler is Caml thread safe, in order that it is not caught in an inconsistent
state.

If you're not using the threads library then I believe the signal handler could
be executed immediately upon reception of the signal in certain cases (for
example if you're calling a blocking syscall); and if you're running Caml code
at the time of the signal, then it should be queued as above.  As such, in this
scenario, you will need to be even more careful about what you do in the signal
handler.  Further, you also have to take into account that if your handler is
immediately executed then you are still inside the genuine operating system
signal handler---which means you've got the C library in an arbitrary state.
You need to restrict yourself to async signal safe glibc (or equivalent) calls
in that scenario (cf. the signal(2) manual page on Linux) and make sure that
the runtime doesn't call any other C library functions as a result of your
signal handling code.  I recommend avoiding that can of worms entirely by doing
as little as possible in the handler.

Mark

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

[Fabrice Le Fessant]

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

The code in queue.ml should be rewritten as:

let add x q =
  if q.length = 0 then
    let rec cell = {
      content = x;
      next = cell
    } in
    q.length <- q.length + 1;
    q.tail <- cell
  else
    let tail = q.tail in
    let head = tail.next in
    let cell = {
      content = x;
      next = head
    } in
    q.length <- q.length + 1;
    tail.next <- cell;
    q.tail <- cell

so that the allocation would be performed before actually mutating the
data structure. Consequently, the signal handler (executed at the
allocation points) would not break the invariants of the queue.

I reported this morning the problem into the bug tracker:
http://caml.inria.fr/mantis/view.php?id=5309

Fabrice
PS: while waiting for the next bug fix release, you should copy and
modify the queue module for yourself...

On 07/06/2011 10:17 AM, Mark Shinwell wrote:
> On Tue, Jul 05, 2011 at 11:26:52PM -0400, Khoo Yit Phang wrote:
>> 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 *)
>>>   ...
> [snip]
>> 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.
> 
> I'm presuming this is native code.  Are you compiling with or without the
> Caml threads library?
> 
> If using the threads library, reception of a signal will cause it to be noted
> down, and the user-defined signal handler written in Caml will be executed
> later.  "Later" is difficult to pin down in words, but it should be the case
> that if you have a section of code which does not involve any allocation nor
> calls to any functions which drop the runtime lock, then it will never be
> interrupted by the execution of a signal handler.  Indeed, it will also never
> be interrupted by a context switch between Caml threads, so you can get
> thread safety guarantees this way.  As far as user code goes, I believe the
> things you have to think about in the two cases of raising an exception from
> a signal handler and experiencing a context switch between Caml threads are
> the same.
> 
> Establishing whether a particular section of code is atomic in this
> regard---let us just say "thread safe"---might involve reading the assembly
> code.  (I've wondered in the past about a construct which could be used to
> indicate that a section is required to be atomic, and the compiler would check
> it.)  I think it is clear that [Queue.add] is not thread safe.  The reason is
> due to the two record allocations in the code, one of which is:
> 
>   let add x q =
>     q.length <- q.length + 1;
>                                   <------- signal happens here
>     if q.length = 1 then
>       let rec cell =
>                                   <------- Caml signal handler executed here
>                                            since the record allocation might
>                                            trigger a garbage collection
>       {
>         content = x;
>         next = cell
>       ...
> 
> It isn't clear to me that it is reasonable to assume all libraries are thread
> safe.  Perhaps the documentation needs improving in this area.  Specifically
> in the case of signal handlers, I would recommend restricting processing in
> them to an absolute minimum, and in particular not throwing exceptions.  The
> code will be easier to think about that way.  If you must throw an exception,
> you have to ensure that any data structure which you rely on in the exception
> handler is Caml thread safe, in order that it is not caught in an inconsistent
> state.
> 
> If you're not using the threads library then I believe the signal handler could
> be executed immediately upon reception of the signal in certain cases (for
> example if you're calling a blocking syscall); and if you're running Caml code
> at the time of the signal, then it should be queued as above.  As such, in this
> scenario, you will need to be even more careful about what you do in the signal
> handler.  Further, you also have to take into account that if your handler is
> immediately executed then you are still inside the genuine operating system
> signal handler---which means you've got the C library in an arbitrary state.
> You need to restrict yourself to async signal safe glibc (or equivalent) calls
> in that scenario (cf. the signal(2) manual page on Linux) and make sure that
> the runtime doesn't call any other C library functions as a result of your
> signal handling code.  I recommend avoiding that can of worms entirely by doing
> as little as possible in the handler.
> 
> Mark
> 

[-- Attachment #2: fabrice_le_fessant.vcf --]
[-- Type: text/x-vcard, Size: 380 bytes --]

begin:vcard
fn:Fabrice LE FESSANT
n:LE FESSANT;Fabrice
org:INRIA Saclay -- Ile-de-France;P2P & OCaml
adr;quoted-printable:;;Parc Orsay Universit=C3=A9 ;Orsay CEDEX;;91893;France
email;internet:fabrice.le_fessant@inria.fr
title;quoted-printable:Charg=C3=A9 de Recherche
tel;work:+33 1 74 85 42 14
tel;fax:+33 1 74 85 42 49 
url:http://fabrice.lefessant.net/
version:2.1
end:vcard

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

[Gerd Stolpmann]

I think this is not very surprising, at least for imperative programs.
After all, interrupting with a signal just means to leave the current
execution flow in an inconsistent state. I don't think you can
systematically do much against this.

Signals are simply a bad mechanism for limiting the runtime of an
algorithm (except you do it the "soft" way - the handler only sets a
flag, which is regularly consulted by the algorithm at safe exit
points).

Gerd

Am Dienstag, den 05.07.2011, 23:26 -0400 schrieb Khoo Yit Phang:
> 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


-- 
------------------------------------------------------------
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
------------------------------------------------------------

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

[Richard W.M. Jones]

I don't find this surprising, and I don't think it's a problem with
OCaml or the standard library (or at least, it's not specific to OCaml).

Another solution to this which hasn't already been noted is to have
your signal write one byte on a pipe which "loops back" to the same
process, and then use a reactor / select / whatever in the main
program to catch this event.

http://cr.yp.to/docs/selfpipe.html

You might need to write such a signal handler in C to ensure it's
really safe.  In our experience, writing signal handlers correctly is
hard.  (Perhaps not as hard as all the scary stuff that happens with
threads, eg:
http://www.linuxprogrammingblog.com/threads-and-fork-think-twice-before-using-them )

Rich.

-- 
Richard Jones
Red Hat

[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
------------------------------------------------------------

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

[ygrek]

On Tue, 5 Jul 2011 23:26:52 -0400
Khoo Yit Phang <khooyp@cs.umd.edu> wrote:

> 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.

See also http://caml.inria.fr/mantis/view.php?id=5141

-- 
 ygrek
 http://ygrek.org.ua

[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.