mirror of
				https://github.com/Z3Prover/z3
				synced 2025-11-04 05:19:11 +00:00 
			
		
		
		
	get rid of threads in the scoped_timer thread pool prior to forking, on non-Windows (#4833)
* on POSIX systems, fork() is dangerous in the presence of a thread pool, because the child process inherits only the thread from the parent that actually called fork(). this patch winds down the scoped_timer thread pool in preparation for forking; workers will get freshly created again following the fork call.
This commit is contained in:
		
							parent
							
								
									05c5f72ca1
								
							
						
					
					
						commit
						b7e1b1e118
					
				
					 2 changed files with 19 additions and 0 deletions
				
			
		| 
						 | 
				
			
			@ -29,6 +29,9 @@ Revision History:
 | 
			
		|||
#include <mutex>
 | 
			
		||||
#include <thread>
 | 
			
		||||
#include <vector>
 | 
			
		||||
#ifndef _WINDOWS
 | 
			
		||||
#include <pthread.h>
 | 
			
		||||
#endif
 | 
			
		||||
 | 
			
		||||
struct scoped_timer_state {
 | 
			
		||||
    std::thread * m_thread { nullptr };
 | 
			
		||||
| 
						 | 
				
			
			@ -119,6 +122,16 @@ scoped_timer::~scoped_timer() {
 | 
			
		|||
    dealloc(m_imp);
 | 
			
		||||
}
 | 
			
		||||
 | 
			
		||||
void scoped_timer::initialize() {
 | 
			
		||||
#ifndef _WINDOWS
 | 
			
		||||
    static bool pthread_atfork_set = false;
 | 
			
		||||
    if (!pthread_atfork_set) {
 | 
			
		||||
        pthread_atfork(finalize, nullptr, nullptr);
 | 
			
		||||
        pthread_atfork_set = true;
 | 
			
		||||
    }
 | 
			
		||||
#endif
 | 
			
		||||
}
 | 
			
		||||
 | 
			
		||||
void scoped_timer::finalize() {
 | 
			
		||||
    unsigned deleted = 0;
 | 
			
		||||
    while (deleted < num_workers) {
 | 
			
		||||
| 
						 | 
				
			
			@ -138,4 +151,5 @@ void scoped_timer::finalize() {
 | 
			
		|||
            delete w;
 | 
			
		||||
        }
 | 
			
		||||
    }
 | 
			
		||||
    num_workers = 0;
 | 
			
		||||
}
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
| 
						 | 
				
			
			@ -26,5 +26,10 @@ class scoped_timer {
 | 
			
		|||
public:
 | 
			
		||||
    scoped_timer(unsigned ms, event_handler * eh);
 | 
			
		||||
    ~scoped_timer();
 | 
			
		||||
    static void initialize();
 | 
			
		||||
    static void finalize();
 | 
			
		||||
};
 | 
			
		||||
 | 
			
		||||
/*
 | 
			
		||||
    ADD_INITIALIZER('scoped_timer::initialize();')
 | 
			
		||||
*/
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue