1
Vote

timeout signal handler invokes non-signal-safe functions

description

On platforms where z3 uses signals to implement timeouts (anything but mac/windows), z3 has a race where it can run into problems when it invokes non-async-signal-safe functions from inside the timout signal handler.

A quick investigation reveals the following problematic calls in on_timeout (smtlib_frontend.cpp):
  • various cout methods
  • exit
  • clock
    I'm not sure that this list is exhaustive.
To be safe, it looks like the signal handler should only use functions from this page:
http://pubs.opengroup.org/onlinepubs/009696899/functions/xsh_chap02_04.html#tag_02_04

Here is the linux specific list (it would be better to use the previous list):
http://www.kernel.org/doc/man-pages/online/pages/man7/signal.7.html

One possible fix is to avoid use of clock and use an iostream that calls write instead of going through a FILE* stream. I don't believe it is possible to safely flush cout and cerr from a signal handler.

I am working around the problem by having the calling process invoke alarm(n), and keeping z3 in the dark about the timeout.

Presumably, all scoped_timer events need to be careful about invoking only signal safe functions. I don't know if there actually are other events, or whether they are sticking to safe functions.

comments

leodemoura wrote Feb 6, 2013 at 11:47 PM

Thanks for reporting the problem.
Does the problem also affects the unstable ("working-in-progress") branch?
We have recently fixed some problems with timers.

Thanks

dvitek wrote Feb 7, 2013 at 7:19 PM

It looks like the problem still exists -- the timer is still implemented using signals on linux and freebsd. The signal handler still invokes a bunch of functions that aren't signal safe:
static void display_statistics() {
clock_t end_time = clock();
if ((g_solver || g_cmd_context) && g_display_statistics) {
    std::cout.flush();
    std::cerr.flush();
    if (g_solver) {
        g_solver->display_statistics();
        memory::display_max_usage(std::cout);
        std::cout << "time:               " << ((static_cast<double>(end_time) - static_cast<double>(g_start_time)) / CLOCKS_PER_SEC) << " secs\n";
    }
    else if (g_cmd_context) {
        g_cmd_context->set_regular_stream("stdout");
        g_cmd_context->display_statistics(true, ((static_cast<double>(end_time) - static_cast<double>(g_start_time)) / CLOCKS_PER_SEC));
    }
}
}

static void on_timeout() {
display_statistics();
exit(0);
}


The ctrl+c suffers from the problem too, since it invokes display_statistics:
static void on_ctrl_c(int) {
signal (SIGINT, SIG_DFL);
display_statistics();
raise(SIGINT);
}


I'm happy working around this issue for the foreseeable future, so don't fix this bug on my behalf.