mirror of
				https://github.com/Z3Prover/z3
				synced 2025-10-31 19:52:29 +00:00 
			
		
		
		
	do not cooperate if OMP mode is disabled (i.e. it's single threaded only)
This commit is contained in:
		
							parent
							
								
									bdd8685146
								
							
						
					
					
						commit
						7d20fbb280
					
				
					 3 changed files with 8 additions and 45 deletions
				
			
		|  | @ -16,6 +16,8 @@ Author: | |||
| Notes: | ||||
| 
 | ||||
| --*/ | ||||
| 
 | ||||
| #ifndef _NO_OMP_ | ||||
| #include "util/cooperate.h" | ||||
| #include "util/trace.h" | ||||
| #include "util/debug.h" | ||||
|  | @ -36,7 +38,7 @@ struct cooperation_lock { | |||
|     } | ||||
| }; | ||||
| 
 | ||||
| cooperation_lock g_lock; | ||||
| static cooperation_lock g_lock; | ||||
| 
 | ||||
| bool cooperation_ctx::g_cooperate = false; | ||||
| 
 | ||||
|  | @ -59,29 +61,4 @@ void cooperation_ctx::checkpoint(char const * task) { | |||
|     } | ||||
| } | ||||
| 
 | ||||
| cooperation_section::cooperation_section() { | ||||
|     SASSERT(!cooperation_ctx::enabled()); | ||||
|     SASSERT(!omp_in_parallel()); | ||||
|     cooperation_ctx::g_cooperate = true; | ||||
| } | ||||
| 
 | ||||
| cooperation_section::~cooperation_section() { | ||||
|     SASSERT(cooperation_ctx::enabled()); | ||||
|     cooperation_ctx::g_cooperate = false; | ||||
| } | ||||
| 
 | ||||
| init_task::init_task(char const * task) { | ||||
|     SASSERT(cooperation_ctx::enabled()); | ||||
|     SASSERT(omp_in_parallel()); | ||||
|     cooperation_ctx::checkpoint(task); | ||||
| } | ||||
| 
 | ||||
| init_task::~init_task() { | ||||
|     int  tid      = omp_get_thread_num(); | ||||
|     if (g_lock.m_owner_thread == tid) { | ||||
|         g_lock.m_owner_thread = -1; | ||||
|         omp_unset_nest_lock(&(g_lock.m_lock)); | ||||
|     } | ||||
| } | ||||
| 
 | ||||
| 
 | ||||
| #endif | ||||
|  |  | |||
|  | @ -19,10 +19,9 @@ Notes: | |||
| #ifndef COOPERATE_H_ | ||||
| #define COOPERATE_H_ | ||||
| 
 | ||||
| class cooperation_section; | ||||
| #ifndef _NO_OMP_ | ||||
| 
 | ||||
| class cooperation_ctx { | ||||
|     friend class cooperation_section; | ||||
|     static bool g_cooperate; | ||||
| public: | ||||
|     static bool enabled() { return g_cooperate; } | ||||
|  | @ -33,18 +32,8 @@ inline void cooperate(char const * task) { | |||
|     if (cooperation_ctx::enabled()) cooperation_ctx::checkpoint(task); | ||||
| } | ||||
| 
 | ||||
| // must be declared before "#pragma parallel" to enable cooperation 
 | ||||
| class cooperation_section { | ||||
| public: | ||||
|     cooperation_section(); | ||||
|     ~cooperation_section(); | ||||
| }; | ||||
| 
 | ||||
| // must be first declaration inside "#pragma parallel for"
 | ||||
| class init_task { | ||||
| public: | ||||
|     init_task(char const * task); | ||||
|     ~init_task(); | ||||
| }; | ||||
| #else | ||||
| inline void cooperate(char const *) {} | ||||
| #endif | ||||
| 
 | ||||
| #endif | ||||
|  |  | |||
|  | @ -814,9 +814,6 @@ public: | |||
|     bool is_even(mpz const & a) { return mpz_manager<SYNCH>::is_even(a); } | ||||
| public: | ||||
|     bool is_even(mpq const & a) { return is_int(a) && is_even(a.m_num); } | ||||
| 
 | ||||
|     friend bool operator==(mpq const & a, mpq const & b) ; | ||||
|     friend bool operator>=(mpq const & a, mpq const & b); | ||||
| }; | ||||
| 
 | ||||
| typedef mpq_manager<true> synch_mpq_manager; | ||||
|  |  | |||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue