1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Gereon Kremer |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Implementation of time limits that are imposed by the --tlimit option. |
14 |
|
* |
15 |
|
* There are various strategies to implement time limits, with different |
16 |
|
* advantages and disadvantages: |
17 |
|
* |
18 |
|
* std::thread: we can spawn a new thread which waits for the time limit. |
19 |
|
* Unless we use std::jthread (from C++20), std::thread is not interruptible |
20 |
|
* and thus we need a synchronization mechanism so that the main thread can |
21 |
|
* communicate to the timer thread that it wants to finish. Apparently, this |
22 |
|
* is the only platform independent way. |
23 |
|
* |
24 |
|
* POSIX setitimer: a very simple way that instructs the kernel to send a |
25 |
|
* signal after some time. If available, this is what we want! |
26 |
|
* |
27 |
|
* Win32 CreateWaitableTimer: unfortunately, this mechanism only calls the |
28 |
|
* completion routine (the callback) when the main thread "enters an |
29 |
|
* alertable wait state", i.e. it sleeps. We don't want our main thread to |
30 |
|
* sleep, thus this approach is not appropriate. |
31 |
|
* |
32 |
|
* Win32 SetTimer: while we can specify a callback function, we still need |
33 |
|
* to process the windows event queue for the callback to be called. (see |
34 |
|
* https://stackoverflow.com/a/15406527/2375725). We don't want our main |
35 |
|
* thread to continuously monitor the event queue. |
36 |
|
* |
37 |
|
* |
38 |
|
* We thus use the setitimer variant whenever possible, and the std::thread |
39 |
|
* variant otherwise. |
40 |
|
*/ |
41 |
|
|
42 |
|
#include "time_limit.h" |
43 |
|
|
44 |
|
#include "base/cvc5config.h" |
45 |
|
|
46 |
|
#if HAVE_SETITIMER |
47 |
|
#include <signal.h> |
48 |
|
#include <sys/time.h> |
49 |
|
#else |
50 |
|
#include <atomic> |
51 |
|
#include <chrono> |
52 |
|
#include <thread> |
53 |
|
#endif |
54 |
|
|
55 |
|
#include <cerrno> |
56 |
|
#include <cstring> |
57 |
|
|
58 |
|
#include "base/exception.h" |
59 |
|
#include "signal_handlers.h" |
60 |
|
|
61 |
|
namespace cvc5 { |
62 |
|
namespace main { |
63 |
|
|
64 |
|
#if HAVE_SETITIMER |
65 |
5881 |
TimeLimit::~TimeLimit() {} |
66 |
|
|
67 |
|
void posix_timeout_handler(int sig, siginfo_t* info, void*) |
68 |
|
{ |
69 |
|
signal_handlers::timeout_handler(); |
70 |
|
} |
71 |
|
#else |
72 |
|
std::atomic<bool> abort_timer_flag; |
73 |
|
|
74 |
|
TimeLimit::~TimeLimit() |
75 |
|
{ |
76 |
|
abort_timer_flag.store(true); |
77 |
|
} |
78 |
|
#endif |
79 |
|
|
80 |
5881 |
TimeLimit install_time_limit(const Options& opts) |
81 |
|
{ |
82 |
5881 |
unsigned long ms = opts.getCumulativeTimeLimit(); |
83 |
|
// Skip if no time limit shall be set. |
84 |
5881 |
if (ms == 0) { |
85 |
5879 |
return TimeLimit(); |
86 |
|
} |
87 |
|
|
88 |
|
#if HAVE_SETITIMER |
89 |
|
// Install a signal handler for SIGALRM |
90 |
|
struct sigaction sact; |
91 |
2 |
sact.sa_sigaction = posix_timeout_handler; |
92 |
2 |
sact.sa_flags = SA_SIGINFO; |
93 |
2 |
sigemptyset(&sact.sa_mask); |
94 |
2 |
if (sigaction(SIGALRM, &sact, NULL)) |
95 |
|
{ |
96 |
|
throw Exception(std::string("sigaction(SIGALRM) failure: ") |
97 |
|
+ strerror(errno)); |
98 |
|
} |
99 |
|
|
100 |
|
// Check https://linux.die.net/man/2/setitimer |
101 |
|
// Then time is up, the kernel will send a SIGALRM |
102 |
|
struct itimerval timerspec; |
103 |
2 |
timerspec.it_value.tv_sec = ms / 1000; |
104 |
2 |
timerspec.it_value.tv_usec = (ms % 1000) * 1000; |
105 |
2 |
timerspec.it_interval.tv_sec = 0; |
106 |
2 |
timerspec.it_interval.tv_usec = 0; |
107 |
|
// Argument 1: which timer to set, we want the real time |
108 |
|
// Argument 2: timer configuration, relative to current time |
109 |
|
// Argument 3: old timer configuration, we don't want to know |
110 |
2 |
if (setitimer(ITIMER_REAL, &timerspec, nullptr)) |
111 |
|
{ |
112 |
|
throw Exception(std::string("timer_settime() failure: ") + strerror(errno)); |
113 |
|
} |
114 |
|
#else |
115 |
|
abort_timer_flag.store(false); |
116 |
|
std::thread t([ms]() |
117 |
|
{ |
118 |
|
// when to stop |
119 |
|
auto limit = std::chrono::system_clock::now() + std::chrono::milliseconds(ms); |
120 |
|
while (limit > std::chrono::system_clock::now()) |
121 |
|
{ |
122 |
|
// check if the main thread is done |
123 |
|
if (abort_timer_flag.load()) return; |
124 |
|
std::this_thread::sleep_for(std::chrono::milliseconds(100)); |
125 |
|
} |
126 |
|
// trigger the timeout handler |
127 |
|
signal_handlers::timeout_handler(); |
128 |
|
}); |
129 |
|
// detach the thread |
130 |
|
t.detach(); |
131 |
|
#endif |
132 |
2 |
return TimeLimit(); |
133 |
|
} |
134 |
|
|
135 |
|
} // namespace main |
136 |
28176 |
} // namespace cvc5 |