mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

Merge pull request from Z3Prover/nomp

Browse source 
Nomp
This commit is contained in:
Nikolaj Bjorner 2019-06-07 02:05:11 +02:00 committed by GitHub
parent 2752bb232a 783f998892
commit e731a44880
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
52 changed files with 484 additions and 552 deletions

52
CMakeLists.txt
View file

@ -272,41 +272,6 @@ else()
message(STATUS "Not using libgmp")
endif()
################################################################################
# OpenMP support
################################################################################
find_package(OpenMP)
if (OPENMP_FOUND)
set(USE_OPENMP_DEFAULT ON)
else()
set(USE_OPENMP_DEFAULT OFF)
endif()
# By setting `USE_OPENMP` this way configuration will fail during the first
# configure if the user explicitly passes `-DUSE_OPENMP=ON` and the compiler
# does not support OpenMP. However if the option is not set explicitly during
# the first configure OpenMP support will be automatically enabled/disabled
# depending on whether OpenMP is available.
option(USE_OPENMP "Use OpenMP" ${USE_OPENMP_DEFAULT})
if (USE_OPENMP)
if (NOT OPENMP_FOUND)
message(FATAL_ERROR "USE_OPENMP is ON but your compiler does not support OpenMP")
endif()
list(APPEND Z3_COMPONENT_CXX_FLAGS ${OpenMP_CXX_FLAGS})
# GCC and Clang need to have additional flags passed to the linker.
# We can't do ``target_link_libraries(libz3 INTERFACE ${OpenMP_CXX_FLAGS})``
# because ``/openmp`` is interpreted as file name rather than a linker
# flag by MSVC and breaks the build
if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR
("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU"))
list(APPEND Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS ${OpenMP_CXX_FLAGS})
endif()
message(STATUS "Using OpenMP")
else()
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_NO_OMP_")
message(STATUS "Not using OpenMP")
endif()
################################################################################
# API Log sync
@ -316,15 +281,26 @@ option(API_LOG_SYNC
OFF
)
if (API_LOG_SYNC)
if (NOT USE_OPENMP)
message(FATAL_ERROR "API_LOG_SYNC feature requires OpenMP")
endif()
list(APPEND Z3_COMPONENT_CXX_DEFINES "-DZ3_LOG_SYNC")
message(STATUS "Using API_LOG_SYNC")
else()
message(STATUS "Not using API_LOG_SYNC")
endif()
################################################################################
# Thread safe or not?
################################################################################
option(SINGLE_THREADED
"Non-thread-safe build"
OFF
)
if (SINGLE_THREADED)
list(APPEND Z3_COMPONENT_CXX_DEFINES "-DSINGLE_THREAD")
message(STATUS "Non-thread-safe build")
else()
message(STATUS "Thread-safe build")
endif()
################################################################################
# FP math
################################################################################

2
cmake/z3_append_linker_flag_list_to_target.cmake
View file

@ -3,7 +3,7 @@
# them to append them as strings to the ``LINK_FLAGS`` property of
# the specified target.
# E.g.
# z3_append_linker_flag_list_to_target(mytarget "-fopenmp" "-static")
# z3_append_linker_flag_list_to_target(mytarget "-static")
function(z3_append_linker_flag_list_to_target target)
if (NOT (TARGET "${target}"))
message(FATAL_ERROR "Specified target \"${target}\" is not a target")

17
scripts/azure-pipeline.vs.yaml
View file

@ -1,17 +0,0 @@
pool:
vmImage: "vs2017-win2016"
steps:
- task: DotNetCoreInstaller@0
displayName: 'Use .NET Core sdk 2.1'
inputs:
version: 2.1.300
- task: BatchScript@1
displayName: 'run windist'
inputs:
filename: 'scripts/mk_win_dist.cmd'

60
scripts/mk_util.py
View file

@ -110,8 +110,8 @@ GPROF=False
GIT_HASH=False
GIT_DESCRIBE=False
SLOW_OPTIMIZE=False
USE_OMP=True
LOG_SYNC=False
SINGLE_THREADED=False
GUARD_CF=False
ALWAYS_DYNAMIC_BASE=False
@ -136,7 +136,7 @@ def git_hash():
raise MKException("Failed to retrieve git hash")
ls = r.split(' ')
if len(ls) != 2:
raise MKException("Unexpected git output")
raise MKException("Unexpected git output " + r)
return ls[0]
def is_windows():
@ -272,24 +272,6 @@ def test_gmp(cc):
return exec_compiler_cmd([cc, CPPFLAGS, 'tstgmp.cpp', LDFLAGS, '-lgmp']) == 0
def test_openmp(cc):
if not USE_OMP:
return False
if is_verbose():
print("Testing OpenMP...")
t = TempFile('tstomp.cpp')
t.add('#include<omp.h>\nint main() { return omp_in_parallel() ? 1 : 0; }\n')
t.commit()
if IS_WINDOWS:
r = exec_compiler_cmd([cc, CPPFLAGS, 'tstomp.cpp', LDFLAGS, '/openmp']) == 0
try:
rmf('tstomp.obj')
rmf('tstomp.exe')
except:
pass
return r
else:
return exec_compiler_cmd([cc, CPPFLAGS, 'tstomp.cpp', LDFLAGS, '-fopenmp']) == 0
def test_fpmath(cc):
global FPMATH_FLAGS
@ -664,8 +646,8 @@ def display_help(exit_code):
if not IS_WINDOWS:
print(" -g, --gmp use GMP.")
print(" --gprof enable gprof")
print(" --noomp disable OpenMP and all features that require it.")
print(" --log-sync synchronize access to API log files to enable multi-thread API logging.")
print(" --single-threaded non-thread-safe build")
print("")
print("Some influential environment variables:")
if not IS_WINDOWS:
@ -692,14 +674,14 @@ def display_help(exit_code):
def parse_options():
global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM
global DOTNET_CORE_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, JS_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED, PYTHON_ENABLED, ESRP_SIGN
global LINUX_X64, SLOW_OPTIMIZE, USE_OMP, LOG_SYNC
global LINUX_X64, SLOW_OPTIMIZE, LOG_SYNC, SINGLE_THREADED
global GUARD_CF, ALWAYS_DYNAMIC_BASE
try:
options, remainder = getopt.gnu_getopt(sys.argv[1:],
'b:df:sxhmcvtnp:gj',
['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj', 'guardcf',
'trace', 'dotnet', 'dotnet-key=', 'esrp', 'staticlib', 'prefix=', 'gmp', 'java', 'parallel=', 'gprof', 'js',
'githash=', 'git-describe', 'x86', 'ml', 'optimize', 'noomp', 'pypkgdir=', 'python', 'staticbin', 'log-sync'])
'githash=', 'git-describe', 'x86', 'ml', 'optimize', 'pypkgdir=', 'python', 'staticbin', 'log-sync', 'single-threaded'])
except:
print("ERROR: Invalid command line option")
display_help(1)
@ -763,10 +745,10 @@ def parse_options():
ML_ENABLED = True
elif opt == "--js":
JS_ENABLED = True
elif opt in ('', '--noomp'):
USE_OMP = False
elif opt in ('', '--log-sync'):
LOG_SYNC = True
elif opt == '--single-threaded':
SINGLE_THREADED = True
elif opt in ('--python'):
PYTHON_ENABLED = True
PYTHON_INSTALL_ENABLED = True
@ -2426,7 +2408,7 @@ def mk_config():
if ONLY_MAKEFILES:
return
config = open(os.path.join(BUILD_DIR, 'config.mk'), 'w')
global CXX, CC, GMP, CPPFLAGS, CXXFLAGS, LDFLAGS, EXAMP_DEBUG_FLAG, FPMATH_FLAGS, HAS_OMP, LOG_SYNC
global CXX, CC, GMP, CPPFLAGS, CXXFLAGS, LDFLAGS, EXAMP_DEBUG_FLAG, FPMATH_FLAGS, LOG_SYNC, SINGLE_THREADED
if IS_WINDOWS:
config.write(
'CC=cl\n'
@ -2446,13 +2428,10 @@ def mk_config():
'OS_DEFINES=/D _WINDOWS\n')
extra_opt = ''
link_extra_opt = ''
HAS_OMP = test_openmp('cl')
if HAS_OMP:
extra_opt = ' /openmp'
else:
extra_opt = ' /D_NO_OMP_'
if HAS_OMP and LOG_SYNC:
if LOG_SYNC:
extra_opt = '%s /DZ3_LOG_SYNC' % extra_opt
if SINGLE_THREADED:
extra_opt = '%s /DSINGLE_THREAD' % extra_opt
if GIT_HASH:
extra_opt = ' %s /D Z3GITHASH=%s' % (extra_opt, GIT_HASH)
if GUARD_CF:
@ -2515,7 +2494,6 @@ def mk_config():
# End of Windows VS config.mk
if is_verbose():
print('64-bit: %s' % is64())
print('OpenMP: %s' % HAS_OMP)
if is_java_enabled():
print('JNI Bindings: %s' % JNI_HOME)
print('Java Compiler: %s' % JAVAC)
@ -2551,15 +2529,10 @@ def mk_config():
CXXFLAGS = '%s -fvisibility=hidden -c' % CXXFLAGS
FPMATH = test_fpmath(CXX)
CXXFLAGS = '%s %s' % (CXXFLAGS, FPMATH_FLAGS)
HAS_OMP = test_openmp(CXX)
if HAS_OMP:
CXXFLAGS = '%s -fopenmp' % CXXFLAGS
LDFLAGS = '%s -fopenmp' % LDFLAGS
SLIBEXTRAFLAGS = '%s -fopenmp' % SLIBEXTRAFLAGS
else:
CXXFLAGS = '%s -D_NO_OMP_' % CXXFLAGS
if HAS_OMP and LOG_SYNC:
if LOG_SYNC:
CXXFLAGS = '%s -DZ3_LOG_SYNC' % CXXFLAGS
if SINGLE_THREADED:
CXXFLAGS = '%s -DSINGLE_THREAD' % CXXFLAGS
if DEBUG_MODE:
CXXFLAGS = '%s -g -Wall' % CXXFLAGS
EXAMP_DEBUG_FLAG = '-g'
@ -2661,7 +2634,6 @@ def mk_config():
print('MinGW32 cross: %s' % (is_cygwin_mingw()))
print('Archive Tool: %s' % AR)
print('Arithmetic: %s' % ARITH)
print('OpenMP: %s' % HAS_OMP)
print('Prefix: %s' % PREFIX)
print('64-bit: %s' % is64())
print('FP math: %s' % FPMATH)
@ -3166,10 +3138,6 @@ def mk_vs_proj_cl_compile(f, name, components, debug):
f.write(' <RuntimeLibrary>MultiThreadedDebugDLL</RuntimeLibrary>\n')
else:
f.write(' <RuntimeLibrary>MultiThreadedDLL</RuntimeLibrary>\n')
if USE_OMP:
f.write(' <OpenMPSupport>true</OpenMPSupport>\n')
else:
f.write(' <OpenMPSupport>false</OpenMPSupport>\n')
f.write(' <DebugInformationFormat>ProgramDatabase</DebugInformationFormat>\n')
f.write(' <AdditionalIncludeDirectories>')
deps = find_all_deps(name, components)

7
scripts/mk_win_dist.cmd
View file

@ -1,4 +1,9 @@
call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars64.bat"
python scripts\mk_win_dist.py
python scripts\mk_win_dist.py --x64-only --dotnet-key=$(Agent.TempDirectory)\z3.snk
call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars32.bat"
python scripts\mk_win_dist.py --x86-only --dotnet-key=$(Agent.TempDirectory)\z3.snk

1
scripts/mk_win_dist.py
View file

@ -89,6 +89,7 @@ def parse_options():
'x86-only',
'x64-only'
])
print(options)
for opt, arg in options:
if opt in ('-b', '--build'):
if arg == 'src':

35
scripts/nightly-macos.yaml Normal file
View file

@ -0,0 +1,35 @@
pool:
vmImage: "macOS-10.14"
steps:
- task: DotNetCoreInstaller@0
displayName: 'Use .NET Core sdk 2.1'
inputs:
version: 2.1.300
- task: DownloadSecureFile@1
inputs:
secureFile: 'z3.snk'
- script: python scripts/mk_unix_dist.py --dotnet-key=$(Agent.TempDirectory)/z3.snk
- script: cp dist/*.zip $(Build.ArtifactStagingDirectory)/.
- task: GitHubRelease@0
inputs:
gitHubConnection: Z3GitHub
repositoryName: 'Z3Prover/z3'
action: 'edit'
target: '$(Build.SourceVersion)'
tagSource: 'manual'
tag: 'NightlyMacOs'
title: 'Nightly MacOs'
releaseNotesSource: 'input'
releaseNotes: 'nightly build'
isDraft: false
isPreRelease: true

35
scripts/nightly-ubuntu.yaml Normal file
View file

@ -0,0 +1,35 @@
pool:
vmImage: "ubuntu-16.04"
steps:
- task: DotNetCoreInstaller@0
displayName: 'Use .NET Core sdk 2.1'
inputs:
version: 2.1.300
- task: DownloadSecureFile@1
inputs:
secureFile: 'z3.snk'
- script: python scripts/mk_unix_dist.py --dotnet-key=$(Agent.TempDirectory)/z3.snk
- script: cp dist/*.zip $(Build.ArtifactStagingDirectory)/.
- task: GitHubRelease@0
inputs:
gitHubConnection: Z3GitHub
repositoryName: 'Z3Prover/z3'
action: 'edit'
target: '$(Build.SourceVersion)'
tagSource: 'manual'
tag: 'NightlyUbuntu'
title: 'Nightly Ubuntu'
releaseNotesSource: 'input'
releaseNotes: 'nightly build'
isDraft: false
isPreRelease: true

35
scripts/nightly-windows.yaml Normal file
View file

@ -0,0 +1,35 @@
pool:
vmImage: "vs2017-win2016"
steps:
- task: DotNetCoreInstaller@0
displayName: 'Use .NET Core sdk 2.1'
inputs:
version: 2.1.300
- task: DownloadSecureFile@1
inputs:
secureFile: 'z3.snk'
- script: scripts\mk_win_dist.cmd
- script: xcopy dist\*.zip $(Build.ArtifactStagingDirectory)\* /y
- task: GitHubRelease@0
inputs:
gitHubConnection: Z3GitHub
repositoryName: 'Z3Prover/z3'
action: 'edit'
target: '$(Build.SourceVersion)'
tagSource: 'manual'
tag: 'NightlyWindows'
title: 'Nightly Windows'
releaseNotesSource: 'input'
releaseNotes: 'nightly build'
isDraft: true
isPreRelease: true

26
src/api/api_context.cpp
View file

@ -119,28 +119,22 @@ namespace api {
context::set_interruptable::set_interruptable(context & ctx, event_handler & i):
m_ctx(ctx) {
#pragma omp critical (set_interruptable)
{
SASSERT(m_ctx.m_interruptable == 0);
m_ctx.m_interruptable = &i;
}
lock_guard lock(ctx.m_mux);
SASSERT(m_ctx.m_interruptable == 0);
m_ctx.m_interruptable = &i;
}
context::set_interruptable::~set_interruptable() {
#pragma omp critical (set_interruptable)
{
m_ctx.m_interruptable = nullptr;
}
lock_guard lock(m_ctx.m_mux);
m_ctx.m_interruptable = nullptr;
}
void context::interrupt() {
#pragma omp critical (set_interruptable)
{
if (m_interruptable)
(*m_interruptable)(API_INTERRUPT_EH_CALLER);
m_limit.cancel();
m().limit().cancel();
}
lock_guard lock(m_mux);
if (m_interruptable)
(*m_interruptable)(API_INTERRUPT_EH_CALLER);
m_limit.cancel();
m().limit().cancel();
}
void context::set_error_code(Z3_error_code err, char const* opt_msg) {

2
src/api/api_context.h
View file

@ -42,6 +42,7 @@ Revision History:
#include "ast/rewriter/seq_rewriter.h"
#include "smt/smt_solver.h"
#include "solver/solver.h"
#include "util/mutex.h"
namespace smtlib {
class parser;
@ -79,6 +80,7 @@ namespace api {
scoped_ptr<ast_manager> m_manager;
scoped_ptr<cmd_context> m_cmd;
add_plugins m_plugins;
mutex m_mux;
arith_util m_arith_util;
bv_util m_bv_util;

62
src/api/api_log.cpp
View file

@ -16,6 +16,7 @@ Revision History:
--*/
#include<fstream>
#include<mutex>
#include "api/z3.h"
#include "api/api_log_macros.h"
#include "util/util.h"
@ -24,6 +25,13 @@ Revision History:
std::ostream * g_z3_log = nullptr;
bool g_z3_log_enabled = false;
#ifdef Z3_LOG_SYNC
static std::mutex g_log_mux;
#define SCOPED_LOCK() std::lock_guard<std::mutex> lock(g_log_mux)
#else
#define SCOPED_LOCK() {}
#endif
extern "C" {
void Z3_close_log_unsafe(void) {
if (g_z3_log != nullptr) {
@ -36,26 +44,20 @@ extern "C" {
bool Z3_API Z3_open_log(Z3_string filename) {
bool res = true;
#ifdef Z3_LOG_SYNC
#pragma omp critical (z3_log)
{
#endif
if (g_z3_log != nullptr)
Z3_close_log_unsafe();
g_z3_log = alloc(std::ofstream, filename);
if (g_z3_log->bad() || g_z3_log->fail()) {
dealloc(g_z3_log);
g_z3_log = nullptr;
res = false;
}
else {
*g_z3_log << "V \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "." << Z3_REVISION_NUMBER << " " << __DATE__ << "\"\n";
g_z3_log->flush();
g_z3_log_enabled = true;
}
#ifdef Z3_LOG_SYNC
SCOPED_LOCK();
if (g_z3_log != nullptr)
Z3_close_log_unsafe();
g_z3_log = alloc(std::ofstream, filename);
if (g_z3_log->bad() || g_z3_log->fail()) {
dealloc(g_z3_log);
g_z3_log = nullptr;
res = false;
}
else {
*g_z3_log << "V \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "." << Z3_REVISION_NUMBER << " " << __DATE__ << "\"\n";
g_z3_log->flush();
g_z3_log_enabled = true;
}
#endif
return res;
}
@ -63,27 +65,15 @@ extern "C" {
void Z3_API Z3_append_log(Z3_string str) {
if (g_z3_log == nullptr)
return;
#ifdef Z3_LOG_SYNC
#pragma omp critical (z3_log)
{
#endif
if (g_z3_log != nullptr)
_Z3_append_log(static_cast<char const *>(str));
#ifdef Z3_LOG_SYNC
}
#endif
SCOPED_LOCK();
if (g_z3_log != nullptr)
_Z3_append_log(static_cast<char const *>(str));
}
void Z3_API Z3_close_log(void) {
if (g_z3_log != nullptr) {
#ifdef Z3_LOG_SYNC
#pragma omp critical (z3_log)
{
#endif
Z3_close_log_unsafe();
#ifdef Z3_LOG_SYNC
}
#endif
SCOPED_LOCK();
Z3_close_log_unsafe();
}
}
}

7
src/ast/rewriter/der.cpp
View file

@ -436,11 +436,8 @@ void der_rewriter::operator()(expr * t, expr_ref & result, proof_ref & result_pr
void der_rewriter::cleanup() {
ast_manager & m = m_imp->m();
#pragma omp critical (th_rewriter)
{
dealloc(m_imp);
m_imp = alloc(imp, m);
}
dealloc(m_imp);
m_imp = alloc(imp, m);
}
void der_rewriter::reset() {

22
src/cmd_context/echo_tactic.cpp
View file

@ -29,12 +29,9 @@ public:
void operator()(goal_ref const & in,
goal_ref_buffer & result) override {
#pragma omp critical (echo_tactic)
{
m_ctx.regular_stream() << m_msg;
if (m_newline)
m_ctx.regular_stream() << std::endl;
}
m_ctx.regular_stream() << m_msg;
if (m_newline)
m_ctx.regular_stream() << std::endl;
skip_tactic::operator()(in, result);
}
};
@ -61,14 +58,11 @@ public:
void operator()(goal_ref const & in,
goal_ref_buffer & result) override {
double val = (*m_p)(*(in.get())).get_value();
#pragma omp critical (probe_value_tactic)
{
if (m_msg)
m_ctx.diagnostic_stream() << m_msg << " ";
m_ctx.diagnostic_stream() << val;
if (m_newline)
m_ctx.diagnostic_stream() << std::endl;
}
if (m_msg)
m_ctx.diagnostic_stream() << m_msg << " ";
m_ctx.diagnostic_stream() << val;
if (m_newline)
m_ctx.diagnostic_stream() << std::endl;
skip_tactic::operator()(in, result);
}
};

38
src/sat/sat_parallel.cpp
View file

@ -129,8 +129,8 @@ namespace sat {
void parallel::exchange(solver& s, literal_vector const& in, unsigned& limit, literal_vector& out) {
if (s.get_config().m_num_threads == 1 || s.m_par_syncing_clauses) return;
flet<bool> _disable_sync_clause(s.m_par_syncing_clauses, true);
#pragma omp critical (par_solver)
{
std::lock_guard<std::mutex> lock(m_mux);
if (limit < m_units.size()) {
// this might repeat some literals.
out.append(m_units.size() - limit, m_units.c_ptr() + limit);
@ -150,8 +150,8 @@ namespace sat {
if (s.get_config().m_num_threads == 1 || s.m_par_syncing_clauses) return;
flet<bool> _disable_sync_clause(s.m_par_syncing_clauses, true);
IF_VERBOSE(3, verbose_stream() << s.m_par_id << ": share " << l1 << " " << l2 << "\n";);
#pragma omp critical (par_solver)
{
std::lock_guard<std::mutex> lock(m_mux);
m_pool.begin_add_vector(s.m_par_id, 2);
m_pool.add_vector_elem(l1.index());
m_pool.add_vector_elem(l2.index());
@ -165,23 +165,19 @@ namespace sat {
unsigned n = c.size();
unsigned owner = s.m_par_id;
IF_VERBOSE(3, verbose_stream() << owner << ": share " << c << "\n";);
#pragma omp critical (par_solver)
{
m_pool.begin_add_vector(owner, n);
for (unsigned i = 0; i < n; ++i) {
m_pool.add_vector_elem(c[i].index());
}
m_pool.end_add_vector();
std::lock_guard<std::mutex> lock(m_mux);
m_pool.begin_add_vector(owner, n);
for (unsigned i = 0; i < n; ++i) {
m_pool.add_vector_elem(c[i].index());
}
m_pool.end_add_vector();
}
void parallel::get_clauses(solver& s) {
if (s.m_par_syncing_clauses) return;
flet<bool> _disable_sync_clause(s.m_par_syncing_clauses, true);
#pragma omp critical (par_solver)
{
_get_clauses(s);
}
std::lock_guard<std::mutex> lock(m_mux);
_get_clauses(s);
}
void parallel::_get_clauses(solver& s) {
@ -241,17 +237,13 @@ namespace sat {
}
void parallel::set_phase(solver& s) {
#pragma omp critical (par_solver)
{
_set_phase(s);
}
std::lock_guard<std::mutex> lock(m_mux);
_set_phase(s);
}
void parallel::get_phase(solver& s) {
#pragma omp critical (par_solver)
{
_get_phase(s);
}
std::lock_guard<std::mutex> lock(m_mux);
_get_phase(s);
}
void parallel::_get_phase(solver& s) {
@ -269,8 +261,8 @@ namespace sat {
bool parallel::get_phase(local_search& s) {
bool copied = false;
#pragma omp critical (par_solver)
{
std::lock_guard<std::mutex> lock(m_mux);
m_consumer_ready = true;
if (m_solver_copy && s.num_non_binary_clauses() > m_solver_copy->m_clauses.size()) {
copied = true;
@ -288,8 +280,8 @@ namespace sat {
bool parallel::copy_solver(solver& s) {
bool copied = false;
#pragma omp critical (par_solver)
{
std::lock_guard<std::mutex> lock(m_mux);
m_consumer_ready = true;
if (m_solver_copy && s.m_clauses.size() > m_solver_copy->m_clauses.size()) {
s.copy(*m_solver_copy, true);

3
src/sat/sat_parallel.h
View file

@ -23,6 +23,8 @@ Revision History:
#include "util/hashtable.h"
#include "util/map.h"
#include "util/rlimit.h"
#include "util/scoped_ptr_vector.h"
#include <mutex>
namespace sat {
@ -60,6 +62,7 @@ namespace sat {
index_set m_unit_set;
literal_vector m_lits;
vector_pool m_pool;
std::mutex m_mux;
// for exchange with local search:
svector<lbool> m_phase;

28
src/sat/sat_solver.cpp
View file

@ -19,6 +19,7 @@ Revision History:
#include <cmath>
#include <thread>
#include "sat/sat_solver.h"
#include "sat/sat_integrity_checker.h"
#include "sat/sat_lookahead.h"
@ -1243,8 +1244,9 @@ namespace sat {
unsigned error_code = 0;
lbool result = l_undef;
bool canceled = false;
#pragma omp parallel for
for (int i = 0; i < num_threads; ++i) {
std::mutex mux;
auto worker_thread = [&](int i) {
try {
lbool r = l_undef;
if (IS_AUX_SOLVER(i)) {
@ -1260,8 +1262,8 @@ namespace sat {
r = check(num_lits, lits);
}
bool first = false;
#pragma omp critical (par_solver)
{
std::lock_guard<std::mutex> lock(mux);
if (finished_id == -1) {
finished_id = i;
first = true;
@ -1296,6 +1298,14 @@ namespace sat {
ex_msg = ex.msg();
ex_kind = DEFAULT_EX;
}
};
vector<std::thread> threads(num_threads);
for (int i = 0; i < num_threads; ++i) {
threads[i] = std::thread([&, i]() { worker_thread(i); });
}
for (auto & th : threads) {
th.join();
}
if (IS_AUX_SOLVER(finished_id)) {
@ -1731,18 +1741,6 @@ namespace sat {
}
if (m_par) m_par->set_phase(*this);
#if 0
static unsigned file_no = 0;
#pragma omp critical (print_sat)
{
++file_no;
std::ostringstream ostrm;
ostrm << "s" << file_no << ".txt";
std::ofstream ous(ostrm.str());
display(ous);
}
#endif
}
bool solver::set_root(literal l, literal r) {

13
src/shell/lp_frontend.cpp
View file

@ -17,6 +17,8 @@ Author:
#include "util/gparams.h"
#include <signal.h>
static std::mutex display_stats_mux;
static lp::lp_solver<double, double>* g_solver = nullptr;
static void display_statistics() {
@ -27,19 +29,17 @@ static void display_statistics() {
static void STD_CALL on_ctrl_c(int) {
signal (SIGINT, SIG_DFL);
#pragma omp critical (g_display_stats)
{
std::lock_guard<std::mutex> lock(display_stats_mux);
display_statistics();
}
raise(SIGINT);
}
static void on_timeout() {
#pragma omp critical (g_display_stats)
{
display_statistics();
exit(0);
}
std::lock_guard<std::mutex> lock(display_stats_mux);
display_statistics();
exit(0);
}
struct front_end_resource_limit : public lp::lp_resource_limit {
@ -92,7 +92,6 @@ void run_solver(lp_params & params, char const * mps_file_name) {
solver->print_model(std::cout);
}
// #pragma omp critical (g_display_stats)
{
display_statistics();
register_on_timeout_proc(nullptr);

9
src/shell/opt_frontend.cpp
View file

@ -25,6 +25,7 @@ static bool g_first_interrupt = true;
static opt::context* g_opt = nullptr;
static double g_start_time = 0;
static unsigned_vector g_handles;
static std::mutex display_stats_mux;
@ -68,8 +69,8 @@ static void STD_CALL on_ctrl_c(int) {
}
else {
signal (SIGINT, SIG_DFL);
#pragma omp critical (g_display_stats)
{
std::lock_guard<std::mutex> lock(display_stats_mux);
display_statistics();
}
raise(SIGINT);
@ -77,11 +78,11 @@ static void STD_CALL on_ctrl_c(int) {
}
static void on_timeout() {
#pragma omp critical (g_display_stats)
{
std::lock_guard<std::mutex> lock(display_stats_mux);
display_statistics();
exit(0);
}
exit(0);
}
static unsigned parse_opt(std::istream& in, opt_format f) {
@ -131,8 +132,8 @@ static unsigned parse_opt(std::istream& in, opt_format f) {
catch (z3_exception & ex) {
std::cerr << ex.msg() << "\n";
}
#pragma omp critical (g_display_stats)
{
std::lock_guard<std::mutex> lock(display_stats_mux);
display_statistics();
register_on_timeout_proc(nullptr);
g_opt = nullptr;

14
src/shell/smtlib_frontend.cpp
View file

@ -32,6 +32,8 @@ Revision History:
#include "tactic/portfolio/smt_strategic_solver.h"
#include "smt/smt_solver.h"
static std::mutex display_stats_mux;
extern bool g_display_statistics;
static clock_t g_start_time;
static cmd_context * g_cmd_context = nullptr;
@ -49,17 +51,15 @@ static void display_statistics() {
}
static void on_timeout() {
#pragma omp critical (g_display_stats)
{
display_statistics();
exit(0);
}
std::lock_guard<std::mutex> lock(display_stats_mux);
display_statistics();
exit(0);
}
static void STD_CALL on_ctrl_c(int) {
signal (SIGINT, SIG_DFL);
#pragma omp critical (g_display_stats)
{
std::lock_guard<std::mutex> lock(display_stats_mux);
display_statistics();
}
raise(SIGINT);
@ -98,8 +98,8 @@ unsigned read_smtlib2_commands(char const * file_name) {
}
#pragma omp critical (g_display_stats)
{
std::lock_guard<std::mutex> lock(display_stats_mux);
display_statistics();
g_cmd_context = nullptr;
}

5
src/smt/asserted_formulas.cpp
View file

@ -435,12 +435,9 @@ void asserted_formulas::commit(unsigned new_qhead) {
TRACE("asserted_formulas", tout << "commit " << new_qhead << "\n";);
m_macro_manager.mark_forbidden(new_qhead - m_qhead, m_formulas.c_ptr() + m_qhead);
m_expr2depth.reset();
bool new_sub = false;
for (unsigned i = m_qhead; i < new_qhead; ++i) {
justified_expr const& j = m_formulas[i];
if (update_substitution(j.get_fml(), j.get_proof())) {
new_sub = true;
}
update_substitution(j.get_fml(), j.get_proof());
}
m_qhead = new_qhead;
}

7
src/smt/smt_kernel.cpp
View file

@ -295,11 +295,8 @@ namespace smt {
ast_manager & _m = m();
smt_params & fps = m_imp->fparams();
params_ref ps = m_imp->params();
#pragma omp critical (smt_kernel)
{
m_imp->~imp();
m_imp = new (m_imp) imp(_m, fps, ps);
}
m_imp->~imp();
m_imp = new (m_imp) imp(_m, fps, ps);
}
bool kernel::inconsistent() {

4
src/smt/tactic/smt_tactic.cpp
View file

@ -59,7 +59,7 @@ public:
}
~smt_tactic() override {
SASSERT(m_ctx == 0);
SASSERT(m_ctx == nullptr);
}
smt_params & fparams() {
@ -132,7 +132,6 @@ public:
new_ctx->set_progress_callback(o.m_callback);
}
o.m_ctx = new_ctx;
}
~scoped_init_ctx() {
@ -208,6 +207,7 @@ public:
m_ctx->collect_statistics(m_stats);
throw;
}
SASSERT(m_ctx);
m_ctx->collect_statistics(m_stats);
proof * pr = m_ctx->get_proof();
TRACE("smt_tactic", tout << r << " " << pr << "\n";);

1
src/smt/theory_array_bapa.cpp
View file

@ -321,7 +321,6 @@ namespace smt {
sz_info& i = *kv.m_value;
if (is_leaf(&i) && (i.m_literal == null_literal || !is_true(i.m_literal))) {
rational value;
expr* set = k->get_arg(0);
expr* sz = k->get_arg(1);
if (!m_arith_value.get_value(sz, value)) {
return l_undef;

2
src/solver/parallel_tactic.cpp
View file

@ -337,7 +337,7 @@ private:
void init() {
parallel_params pp(m_params);
m_num_threads = std::min((unsigned)omp_get_num_procs(), pp.threads_max());
m_num_threads = std::min((unsigned) std::thread::hardware_concurrency(), pp.threads_max());
m_progress = 0;
m_has_undef = false;
m_allsat = false;

68
src/tactic/tactical.cpp
View file

@ -20,8 +20,9 @@ Notes:
#include "util/cancel_eh.h"
#include "util/cooperate.h"
#include "util/scoped_ptr_vector.h"
#include "util/z3_omp.h"
#include "tactic/tactical.h"
#include <thread>
#include <vector>
class binary_tactical : public tactic {
protected:
@ -369,20 +370,20 @@ enum par_exception_kind {
class par_tactical : public or_else_tactical {
std::string ex_msg;
unsigned error_code;
public:
par_tactical(unsigned num, tactic * const * ts):or_else_tactical(num, ts) {}
par_tactical(unsigned num, tactic * const * ts):or_else_tactical(num, ts) {
error_code = 0;
}
~par_tactical() override {}
void operator()(goal_ref const & in, goal_ref_buffer& result) override {
bool use_seq;
#ifdef _NO_OMP_
use_seq = true;
#else
use_seq = 0 != omp_in_parallel();
#endif
use_seq = false;
if (use_seq) {
// execute tasks sequentially
or_else_tactical::operator()(in, result);
@ -407,21 +408,19 @@ public:
unsigned finished_id = UINT_MAX;
par_exception_kind ex_kind = DEFAULT_EX;
std::string ex_msg;
unsigned error_code = 0;
#pragma omp parallel for
for (int i = 0; i < static_cast<int>(sz); i++) {
goal_ref_buffer _result;
std::mutex mux;
auto worker_thread = [&](unsigned i) {
goal_ref_buffer _result;
goal_ref in_copy = in_copies[i];
tactic & t = *(ts.get(i));
try {
t(in_copy, _result);
bool first = false;
#pragma omp critical (par_tactical)
{
std::lock_guard<std::mutex> lock(mux);
if (finished_id == UINT_MAX) {
finished_id = i;
first = true;
@ -429,10 +428,11 @@ public:
}
if (first) {
for (unsigned j = 0; j < sz; j++) {
if (static_cast<unsigned>(i) != j) {
if (i != j) {
managers[j]->limit().cancel();
}
}
ast_translation translator(*(managers[i]), m, false);
for (goal* g : _result) {
result.push_back(g->translate(translator));
@ -459,7 +459,17 @@ public:
ex_msg = z3_ex.msg();
}
}
};
vector<std::thread> threads(sz);
for (unsigned i = 0; i < sz; ++i) {
threads[i] = std::thread([&, i]() { worker_thread(i); });
}
for (unsigned i = 0; i < sz; ++i) {
threads[i].join();
}
if (finished_id == UINT_MAX) {
switch (ex_kind) {
case ERROR_EX: throw z3_error(error_code);
@ -499,11 +509,7 @@ public:
void operator()(goal_ref const & in, goal_ref_buffer& result) override {
bool use_seq;
#ifdef _NO_OMP_
use_seq = true;
#else
use_seq = 0 != omp_in_parallel();
#endif
use_seq = false;
if (use_seq) {
// execute tasks sequentially
and_then_tactical::operator()(in, result);
@ -554,9 +560,9 @@ public:
par_exception_kind ex_kind = DEFAULT_EX;
unsigned error_code = 0;
std::string ex_msg;
std::mutex mux;
#pragma omp parallel for
for (int i = 0; i < static_cast<int>(r1_size); i++) {
auto worker_thread = [&](unsigned i) {
ast_manager & new_m = *(managers[i]);
goal_ref new_g = g_copies[i];
@ -568,8 +574,8 @@ public:
ts2[i]->operator()(new_g, r2);
}
catch (tactic_exception & ex) {
#pragma omp critical (par_and_then_tactical)
{
std::lock_guard<std::mutex> lock(mux);
if (!failed && !found_solution) {
curr_failed = true;
failed = true;
@ -579,8 +585,8 @@ public:
}
}
catch (z3_error & err) {
#pragma omp critical (par_and_then_tactical)
{
std::lock_guard<std::mutex> lock(mux);
if (!failed && !found_solution) {
curr_failed = true;
failed = true;
@ -590,8 +596,8 @@ public:
}
}
catch (z3_exception & z3_ex) {
#pragma omp critical (par_and_then_tactical)
{
std::lock_guard<std::mutex> lock(mux);
if (!failed && !found_solution) {
curr_failed = true;
failed = true;
@ -614,8 +620,8 @@ public:
if (is_decided_sat(r2)) {
// found solution...
bool first = false;
#pragma omp critical (par_and_then_tactical)
{
std::lock_guard<std::mutex> lock(mux);
if (!found_solution) {
failed = false;
found_solution = true;
@ -655,6 +661,14 @@ public:
}
}
}
};
vector<std::thread> threads(r1_size);
for (unsigned i = 0; i < r1_size; ++i) {
threads[i] = std::thread([&, i]() { worker_thread(i); });
}
for (unsigned i = 0; i < r1_size; ++i) {
threads[i].join();
}
if (failed) {

45
src/util/cooperate.cpp
View file

@ -17,48 +17,35 @@ Notes:
--*/
#ifndef _NO_OMP_
#ifndef SINGLE_THREAD
#include "util/cooperate.h"
#include "util/trace.h"
#include "util/debug.h"
#include "util/z3_omp.h"
#include <atomic>
#include <mutex>
#include <thread>
struct cooperation_lock {
omp_nest_lock_t m_lock;
char const * m_task;
volatile int m_owner_thread;
cooperation_lock() {
omp_set_nested(1);
omp_init_nest_lock(&m_lock);
m_task = nullptr;
m_owner_thread = -1;
}
~cooperation_lock() {
omp_destroy_nest_lock(&m_lock);
}
};
static cooperation_lock g_lock;
static std::mutex lock;
static std::atomic<std::thread::id> owner_thread;
bool cooperation_ctx::g_cooperate = false;
void cooperation_ctx::checkpoint(char const * task) {
SASSERT(cooperation_ctx::enabled());
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));
std::thread::id tid = std::this_thread::get_id();
if (owner_thread == tid) {
owner_thread = std::thread::id();
lock.unlock();
}
// this critical section is used to force the owner thread to give a chance to
// another thread to get the lock
#pragma omp critical (z3_cooperate)
{
omp_set_nest_lock(&(g_lock.m_lock));
TRACE("cooperate_detail", tout << task << ", tid: " << tid << "\n";);
CTRACE("cooperate", g_lock.m_task != task, tout << "moving to task: " << task << "\n";);
g_lock.m_owner_thread = tid;
}
std::this_thread::yield();
lock.lock();
TRACE("cooperate_detail", tout << task << ", tid: " << tid << "\n";);
owner_thread = tid;
}
#endif

7
src/util/cooperate.h
View file

@ -16,10 +16,9 @@ Author:
Notes:
--*/
#ifndef COOPERATE_H_
#define COOPERATE_H_
#pragma once
#ifndef _NO_OMP_
#ifndef SINGLE_THREAD
class cooperation_ctx {
static bool g_cooperate;
@ -35,5 +34,3 @@ inline void cooperate(char const * task) {
#else
inline void cooperate(char const *) {}
#endif
#endif

79
src/util/gparams.cpp
View file

@ -19,6 +19,9 @@ Notes:
#include "util/gparams.h"
#include "util/dictionary.h"
#include "util/trace.h"
#include "util/mutex.h"
static mutex gparams_mux;
extern void gparams_register_modules();
@ -110,14 +113,12 @@ public:
}
void reset() {
#pragma omp critical (gparams)
{
m_params.reset();
for (auto & kv : m_module_params) {
dealloc(kv.m_value);
}
m_module_params.reset();
lock_guard lock(gparams_mux);
m_params.reset();
for (auto & kv : m_module_params) {
dealloc(kv.m_value);
}
m_module_params.reset();
}
// -----------------------------------------------
@ -327,8 +328,8 @@ public:
void set(char const * name, char const * value) {
bool error = false;
std::string error_msg;
#pragma omp critical (gparams)
{
lock_guard lock(gparams_mux);
try {
symbol m, p;
normalize(name, m, p);
@ -379,8 +380,8 @@ public:
std::string r;
bool error = false;
std::string error_msg;
#pragma omp critical (gparams)
{
lock_guard lock(gparams_mux);
try {
symbol m, p;
normalize(name, m, p);
@ -426,8 +427,8 @@ public:
params_ref get_module(symbol const & module_name) {
params_ref result;
params_ref * ps = nullptr;
#pragma omp critical (gparams)
{
lock_guard lock(gparams_mux);
if (m_module_params.find(module_name, ps)) {
result.copy(*ps);
}
@ -446,8 +447,8 @@ public:
// -----------------------------------------------
void display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) {
#pragma omp critical (gparams)
{
lock_guard lock(gparams_mux);
out << "Global parameters\n";
get_param_descrs().display(out, indent + 4, smt2_style, include_descr);
out << "\n";
@ -469,44 +470,40 @@ public:
}
void display_modules(std::ostream & out) {
#pragma omp critical (gparams)
{
for (auto & kv : get_module_param_descrs()) {
out << "[module] " << kv.m_key;
char const * descr = nullptr;
if (get_module_descrs().find(kv.m_key, descr)) {
out << ", description: " << descr;
}
out << "\n";
lock_guard lock(gparams_mux);
for (auto & kv : get_module_param_descrs()) {
out << "[module] " << kv.m_key;
char const * descr = nullptr;
if (get_module_descrs().find(kv.m_key, descr)) {
out << ", description: " << descr;
}
out << "\n";
}
}
void display_module(std::ostream & out, symbol const & module_name) {
bool error = false;
std::string error_msg;
#pragma omp critical (gparams)
{
try {
param_descrs * d = nullptr;
if (!get_module_param_descrs().find(module_name, d)) {
std::stringstream strm;
strm << "unknown module '" << module_name << "'";
throw exception(strm.str());
}
out << "[module] " << module_name;
char const * descr = nullptr;
if (get_module_descrs().find(module_name, descr)) {
out << ", description: " << descr;
}
out << "\n";
d->display(out, 4, false);
lock_guard lock(gparams_mux);
try {
param_descrs * d = nullptr;
if (!get_module_param_descrs().find(module_name, d)) {
std::stringstream strm;
strm << "unknown module '" << module_name << "'";
throw exception(strm.str());
}
catch (z3_exception & ex) {
// Exception cannot cross critical section boundaries.
error = true;
error_msg = ex.msg();
out << "[module] " << module_name;
char const * descr = nullptr;
if (get_module_descrs().find(module_name, descr)) {
out << ", description: " << descr;
}
out << "\n";
d->display(out, 4, false);
}
catch (z3_exception & ex) {
// Exception cannot cross critical section boundaries.
error = true;
error_msg = ex.msg();
}
if (error)
throw exception(std::move(error_msg));
@ -515,8 +512,8 @@ public:
void display_parameter(std::ostream & out, char const * name) {
bool error = false;
std::string error_msg;
#pragma omp critical (gparams)
{
lock_guard lock(gparams_mux);
try {
symbol m, p;
normalize(name, m, p);

39
src/util/memory_manager.cpp
View file

@ -7,10 +7,10 @@ Copyright (c) 2015 Microsoft Corporation
#include<iostream>
#include<stdlib.h>
#include<climits>
#include "util/mutex.h"
#include "util/trace.h"
#include "util/memory_manager.h"
#include "util/error_codes.h"
#include "util/z3_omp.h"
#include "util/debug.h"
// The following two function are automatically generated by the mk_make.py script.
// The script collects ADD_INITIALIZER and ADD_FINALIZER commands in the .h files.
@ -35,7 +35,8 @@ out_of_memory_error::out_of_memory_error():z3_error(ERR_MEMOUT) {
}
static volatile bool g_memory_out_of_memory = false;
static mutex g_memory_mux;
static atomic<bool> g_memory_out_of_memory(false);
static bool g_memory_initialized = false;
static long long g_memory_alloc_size = 0;
static long long g_memory_max_size = 0;
@ -54,10 +55,7 @@ void memory::exit_when_out_of_memory(bool flag, char const * msg) {
}
static void throw_out_of_memory() {
#pragma omp critical (z3_memory_manager)
{
g_memory_out_of_memory = true;
}
g_memory_out_of_memory = true;
if (g_exit_when_out_of_memory) {
std::cerr << g_out_of_memory_msg << "\n";
@ -90,8 +88,8 @@ mem_usage_report g_info;
void memory::initialize(size_t max_size) {
bool initialize = false;
#pragma omp critical (z3_memory_manager)
{
lock_guard lock(g_memory_mux);
// only update the maximum size if max_size != UINT_MAX
if (max_size != UINT_MAX)
g_memory_max_size = max_size;
@ -115,12 +113,7 @@ void memory::initialize(size_t max_size) {
}
bool memory::is_out_of_memory() {
bool r = false;
#pragma omp critical (z3_memory_manager)
{
r = g_memory_out_of_memory;
}
return r;
return g_memory_out_of_memory;
}
void memory::set_high_watermark(size_t watermark) {
@ -131,12 +124,8 @@ void memory::set_high_watermark(size_t watermark) {
bool memory::above_high_watermark() {
if (g_memory_watermark == 0)
return false;
bool r;
#pragma omp critical (z3_memory_manager)
{
r = g_memory_watermark < g_memory_alloc_size;
}
return r;
lock_guard lock(g_memory_mux);
return g_memory_watermark < g_memory_alloc_size;
}
// The following methods are only safe to invoke at
@ -163,8 +152,8 @@ void memory::finalize() {
unsigned long long memory::get_allocation_size() {
long long r;
#pragma omp critical (z3_memory_manager)
{
lock_guard lock(g_memory_mux);
r = g_memory_alloc_size;
}
if (r < 0)
@ -174,8 +163,8 @@ unsigned long long memory::get_allocation_size() {
unsigned long long memory::get_max_used_memory() {
unsigned long long r;
#pragma omp critical (z3_memory_manager)
{
lock_guard lock(g_memory_mux);
r = g_memory_max_used_size;
}
return r;
@ -258,8 +247,8 @@ static void synchronize_counters(bool allocating) {
bool out_of_mem = false;
bool counts_exceeded = false;
#pragma omp critical (z3_memory_manager)
{
lock_guard lock(g_memory_mux);
g_memory_alloc_size += g_memory_thread_alloc_size;
g_memory_alloc_count += g_memory_thread_alloc_count;
if (g_memory_alloc_size > g_memory_max_used_size)
@ -339,8 +328,8 @@ void memory::deallocate(void * p) {
size_t * sz_p = reinterpret_cast<size_t*>(p) - 1;
size_t sz = *sz_p;
void * real_p = reinterpret_cast<void*>(sz_p);
#pragma omp critical (z3_memory_manager)
{
lock_guard lock(g_memory_mux);
g_memory_alloc_size -= sz;
}
free(real_p);
@ -349,8 +338,8 @@ void memory::deallocate(void * p) {
void * memory::allocate(size_t s) {
s = s + sizeof(size_t); // we allocate an extra field!
bool out_of_mem = false, counts_exceeded = false;
#pragma omp critical (z3_memory_manager)
{
lock_guard lock(g_memory_mux);
g_memory_alloc_size += s;
g_memory_alloc_count += 1;
if (g_memory_alloc_size > g_memory_max_used_size)
@ -379,8 +368,8 @@ void* memory::reallocate(void *p, size_t s) {
void * real_p = reinterpret_cast<void*>(sz_p);
s = s + sizeof(size_t); // we allocate an extra field!
bool out_of_mem = false, counts_exceeded = false;
#pragma omp critical (z3_memory_manager)
{
lock_guard lock(g_memory_mux);
g_memory_alloc_size += s - sz;
g_memory_alloc_count += 1;
if (g_memory_alloc_size > g_memory_max_used_size)

10
src/util/mpff.cpp
View file

@ -376,7 +376,7 @@ void mpff_manager::set(mpff & n, unsynch_mpz_manager & m, mpz const & v) {
set_core(n, m, v);
}
#ifndef _NO_OMP_
#ifndef SINGLE_THREAD
void mpff_manager::set(mpff & n, synch_mpz_manager & m, mpz const & v) {
set_core(n, m, v);
}
@ -399,7 +399,7 @@ void mpff_manager::set(mpff & n, unsynch_mpq_manager & m, mpq const & v) {
set_core(n, m, v);
}
#ifndef _NO_OMP_
#ifndef SINGLE_THREAD
void mpff_manager::set(mpff & n, synch_mpq_manager & m, mpq const & v) {
set_core(n, m, v);
}
@ -1081,7 +1081,7 @@ void mpff_manager::significand(mpff const & n, unsynch_mpz_manager & m, mpz & t)
significand_core(n, m, t);
}
#ifndef _NO_OMP_
#ifndef SINGLE_THREAD
void mpff_manager::significand(mpff const & n, synch_mpz_manager & m, mpz & t) {
significand_core(n, m, t);
}
@ -1115,7 +1115,7 @@ void mpff_manager::to_mpz(mpff const & n, unsynch_mpz_manager & m, mpz & t) {
to_mpz_core(n, m, t);
}
#ifndef _NO_OMP_
#ifndef SINGLE_THREAD
void mpff_manager::to_mpz(mpff const & n, synch_mpz_manager & m, mpz & t) {
to_mpz_core(n, m, t);
}
@ -1162,7 +1162,7 @@ void mpff_manager::to_mpq(mpff const & n, unsynch_mpq_manager & m, mpq & t) {
to_mpq_core(n, m, t);
}
#ifndef _NO_OMP_
#ifndef SINGLE_THREAD
void mpff_manager::to_mpq(mpff const & n, synch_mpq_manager & m, mpq & t) {
to_mpq_core(n, m, t);
}

10
src/util/mpff.h
View file

@ -58,7 +58,7 @@ class mpz;
class mpq;
template<bool SYNCH> class mpz_manager;
template<bool SYNCH> class mpq_manager;
#ifndef _NO_OMP_
#ifndef SINGLE_THREAD
typedef mpz_manager<true> synch_mpz_manager;
typedef mpq_manager<true> synch_mpq_manager;
#else
@ -218,7 +218,7 @@ public:
\brief Return the significand as a mpz numeral.
*/
void significand(mpff const & n, unsynch_mpz_manager & m, mpz & r);
#ifndef _NO_OMP_
#ifndef SINGLE_THREAD
void significand(mpff const & n, synch_mpz_manager & m, mpz & r);
#endif
@ -386,7 +386,7 @@ public:
void set(mpff & n, mpff const & v);
void set(mpff & n, unsynch_mpz_manager & m, mpz const & v);
void set(mpff & n, unsynch_mpq_manager & m, mpq const & v);
#ifndef _NO_OMP_
#ifndef SINGLE_THREAD
void set(mpff & n, synch_mpq_manager & m, mpq const & v);
void set(mpff & n, synch_mpz_manager & m, mpz const & v);
#endif
@ -429,7 +429,7 @@ public:
*/
void to_mpz(mpff const & n, unsynch_mpz_manager & m, mpz & t);
#ifndef _NO_OMP_
#ifndef SINGLE_THREAD
/**
\brief Convert n into a mpz numeral.
@ -447,7 +447,7 @@ public:
*/
void to_mpq(mpff const & n, unsynch_mpq_manager & m, mpq & t);
#ifndef _NO_OMP_
#ifndef SINGLE_THREAD
/**
\brief Convert n into a mpq numeral.

8
src/util/mpfx.cpp
View file

@ -272,7 +272,7 @@ void mpfx_manager::set(mpfx & n, unsynch_mpz_manager & m, mpz const & v) {
set_core(n, m, v);
}
#ifndef _NO_OMP_
#ifndef SINGLE_THREAD
void mpfx_manager::set(mpfx & n, synch_mpz_manager & m, mpz const & v) {
set_core(n, m, v);
}
@ -311,7 +311,7 @@ void mpfx_manager::set(mpfx & n, unsynch_mpq_manager & m, mpq const & v) {
set_core(n, m, v);
}
#ifndef _NO_OMP_
#ifndef SINGLE_THREAD
void mpfx_manager::set(mpfx & n, synch_mpq_manager & m, mpq const & v) {
set_core(n, m, v);
}
@ -718,7 +718,7 @@ void mpfx_manager::to_mpz(mpfx const & n, unsynch_mpz_manager & m, mpz & t) {
to_mpz_core(n, m, t);
}
#ifndef _NO_OMP_
#ifndef SINGLE_THREAD
void mpfx_manager::to_mpz(mpfx const & n, synch_mpz_manager & m, mpz & t) {
to_mpz_core(n, m, t);
}
@ -744,7 +744,7 @@ void mpfx_manager::to_mpq(mpfx const & n, unsynch_mpq_manager & m, mpq & t) {
to_mpq_core(n, m, t);
}
#ifndef _NO_OMP_
#ifndef SINGLE_THREAD
void mpfx_manager::to_mpq(mpfx const & n, synch_mpq_manager & m, mpq & t) {
to_mpq_core(n, m, t);
}

8
src/util/mpfx.h
View file

@ -51,7 +51,7 @@ class mpz;
class mpq;
template<bool SYNCH> class mpz_manager;
template<bool SYNCH> class mpq_manager;
#ifndef _NO_OMP_
#ifndef SINGLE_THREAD
typedef mpz_manager<true> synch_mpz_manager;
typedef mpq_manager<true> synch_mpq_manager;
#else
@ -318,7 +318,7 @@ public:
void set(mpfx & n, mpfx const & v);
void set(mpfx & n, unsynch_mpz_manager & m, mpz const & v);
void set(mpfx & n, unsynch_mpq_manager & m, mpq const & v);
#ifndef _NO_OMP_
#ifndef SINGLE_THREAD
void set(mpfx & n, synch_mpz_manager & m, mpz const & v);
void set(mpfx & n, synch_mpq_manager & m, mpq const & v);
#endif
@ -366,7 +366,7 @@ public:
*/
void to_mpz(mpfx const & n, unsynch_mpz_manager & m, mpz & t);
#ifndef _NO_OMP_
#ifndef SINGLE_THREAD
/**
\brief Convert n into a mpz numeral.
@ -380,7 +380,7 @@ public:
*/
void to_mpq(mpfx const & n, unsynch_mpq_manager & m, mpq & t);
#ifndef _NO_OMP_
#ifndef SINGLE_THREAD
/**
\brief Convert n into a mpq numeral.
*/

2
src/util/mpn.cpp
View file

@ -29,11 +29,9 @@ static_assert(sizeof(mpn_double_digit) == 2 * sizeof(mpn_digit), "size alignment
const mpn_digit mpn_manager::zero = 0;
mpn_manager::mpn_manager() {
omp_init_nest_lock(&m_lock);
}
mpn_manager::~mpn_manager() {
omp_destroy_nest_lock(&m_lock);
}
int mpn_manager::compare(mpn_digit const * a, size_t const lnga,

13
src/util/mpn.h
View file

@ -20,18 +20,21 @@ Revision History:
#define MPN_H_
#include<ostream>
#include<mutex>
#include "util/util.h"
#include "util/buffer.h"
#include "util/z3_omp.h"
typedef unsigned int mpn_digit;
class mpn_manager {
#ifndef _NO_OMP_
omp_nest_lock_t m_lock;
#ifndef SINGLE_THREAD
std::recursive_mutex m_lock;
#define MPN_BEGIN_CRITICAL() m_lock.lock()
#define MPN_END_CRITICAL() m_lock.unlock()
#else
#define MPN_BEGIN_CRITICAL() {}
#define MPN_END_CRITICAL() {}
#endif
#define MPN_BEGIN_CRITICAL() omp_set_nest_lock(&m_lock);
#define MPN_END_CRITICAL() omp_unset_nest_lock(&m_lock);
public:
mpn_manager();

2
src/util/mpq.cpp
View file

@ -428,7 +428,7 @@ void mpq_manager<SYNCH>::rat_sub(mpq const & a, mpq const & b, mpq & c) {
}
#ifndef _NO_OMP_
#ifndef SINGLE_THREAD
template class mpq_manager<true>;
#endif
template class mpq_manager<false>;

2
src/util/mpq.h
View file

@ -816,7 +816,7 @@ public:
bool is_even(mpq const & a) { return is_int(a) && is_even(a.m_num); }
};
#ifndef _NO_OMP_
#ifndef SINGLE_THREAD
typedef mpq_manager<true> synch_mpq_manager;
#else
typedef mpq_manager<false> synch_mpq_manager;

2
src/util/mpq_inf.cpp
View file

@ -39,7 +39,7 @@ std::string mpq_inf_manager<SYNCH>::to_string(mpq_inf const & a) {
}
#ifndef _NO_OMP_
#ifndef SINGLE_THREAD
template class mpq_inf_manager<true>;
#endif
template class mpq_inf_manager<false>;

2
src/util/mpq_inf.h
View file

@ -279,7 +279,7 @@ public:
mpq_manager<SYNCH>& get_mpq_manager() { return m; }
};
#ifndef _NO_OMP_
#ifndef SINGLE_THREAD
typedef mpq_inf_manager<true> synch_mpq_inf_manager;
#else
typedef mpq_inf_manager<false> synch_mpq_inf_manager;

6
src/util/mpz.cpp
View file

@ -139,8 +139,6 @@ uint64_t u64_gcd(uint64_t u, uint64_t v) {
template<bool SYNCH>
mpz_manager<SYNCH>::mpz_manager():
m_allocator("mpz_manager") {
if (SYNCH)
omp_init_nest_lock(&m_lock);
#ifndef _MP_GMP
if (sizeof(digit_t) == sizeof(uint64_t)) {
// 64-bit machine
@ -197,8 +195,6 @@ mpz_manager<SYNCH>::~mpz_manager() {
mpz_clear(m_int64_max);
mpz_clear(m_int64_min);
#endif
if (SYNCH)
omp_destroy_nest_lock(&m_lock);
}
#ifndef _MP_GMP
@ -2470,7 +2466,7 @@ bool mpz_manager<SYNCH>::divides(mpz const & a, mpz const & b) {
return r;
}
#ifndef _NO_OMP_
#ifndef SINGLE_THREAD
template class mpz_manager<true>;
#endif
template class mpz_manager<false>;

15
src/util/mpz.h
View file

@ -20,12 +20,12 @@ Revision History:
#define MPZ_H_
#include<string>
#include<mutex>
#include "util/util.h"
#include "util/small_object_allocator.h"
#include "util/trace.h"
#include "util/scoped_numeral.h"
#include "util/scoped_numeral_vector.h"
#include "util/z3_omp.h"
#include "util/mpn.h"
unsigned u_gcd(unsigned u, unsigned v);
@ -135,9 +135,14 @@ inline void swap(mpz & m1, mpz & m2) { m1.swap(m2); }
template<bool SYNCH = true>
class mpz_manager {
mutable small_object_allocator m_allocator;
mutable omp_nest_lock_t m_lock;
#define MPZ_BEGIN_CRITICAL() if (SYNCH) omp_set_nest_lock(&m_lock);
#define MPZ_END_CRITICAL() if (SYNCH) omp_unset_nest_lock(&m_lock);
#ifndef SINGLE_THREAD
mutable std::recursive_mutex m_lock;
#define MPZ_BEGIN_CRITICAL() if (SYNCH) m_lock.lock()
#define MPZ_END_CRITICAL() if (SYNCH) m_lock.unlock()
#else
#define MPZ_BEGIN_CRITICAL() {}
#define MPZ_END_CRITICAL() {}
#endif
mutable mpn_manager m_mpn_manager;
#ifndef _MP_GMP
@ -702,7 +707,7 @@ public:
bool decompose(mpz const & n, svector<digit_t> & digits);
};
#ifndef _NO_OMP_
#ifndef SINGLE_THREAD
typedef mpz_manager<true> synch_mpz_manager;
#else
typedef mpz_manager<false> synch_mpz_manager;

35
src/util/mutex.h Normal file
View file

@ -0,0 +1,35 @@
/*++
Copyright (c) 2019 Microsoft Corporation
Module Name:
mutex.h
Abstract:
Auxiliary macros for mutual exclusion
--*/
#pragma once
#ifdef SINGLE_THREAD
template<typename T> using atomic = T;
struct mutex {
void lock() {}
void unlock() {}
};
struct lock_guard {
lock_guard(mutex &) {}
};
#else
#include <atomic>
#include <mutex>
template<typename T> using atomic = std::atomic<T>;
typedef std::mutex mutex;
typedef std::lock_guard<std::mutex> lock_guard;
#endif

6
src/util/prime_generator.cpp
View file

@ -17,6 +17,7 @@ Notes:
--*/
#include "util/prime_generator.h"
#include "util/mutex.h"
#define PRIME_LIST_MAX_SIZE 1<<20
@ -109,6 +110,8 @@ prime_iterator::prime_iterator(prime_generator * g):m_idx(0) {
}
}
static mutex g_prime_iterator;
uint64_t prime_iterator::next() {
unsigned idx = m_idx;
m_idx++;
@ -117,7 +120,7 @@ uint64_t prime_iterator::next() {
}
else {
uint64_t r;
#pragma omp critical (prime_iterator)
lock_guard lock(g_prime_iterator);
{
r = (*m_generator)(idx);
}
@ -128,4 +131,3 @@ uint64_t prime_iterator::next() {
void prime_iterator::finalize() {
g_prime_generator.finalize();
}

8
src/util/rational.cpp
View file

@ -17,11 +17,9 @@ Revision History:
--*/
#include<sstream>
#include "util/mutex.h"
#include "util/util.h"
#include "util/rational.h"
#ifdef _WINDOWS
#include<strsafe.h>
#endif
synch_mpq_manager * rational::g_mpq_manager = nullptr;
rational rational::m_zero;
@ -42,9 +40,11 @@ static void mk_power_up_to(vector<rational> & pws, unsigned n) {
}
}
static mutex g_powers_of_two;
rational rational::power_of_two(unsigned k) {
rational result;
#pragma omp critical (powers_of_two)
lock_guard lock(g_powers_of_two);
{
if (k >= m_powers_of_two.size())
mk_power_up_to(m_powers_of_two, k+1);

44
src/util/rlimit.cpp
View file

@ -18,6 +18,10 @@ Revision History:
--*/
#include "util/rlimit.h"
#include "util/common_msgs.h"
#include "util/mutex.h"
static mutex g_rlimit_mux;
reslimit::reslimit():
m_cancel(0),
@ -69,48 +73,34 @@ char const* reslimit::get_cancel_msg() const {
}
void reslimit::push_child(reslimit* r) {
#pragma omp critical (reslimit_cancel)
{
m_children.push_back(r);
}
lock_guard lock(g_rlimit_mux);
m_children.push_back(r);
}
void reslimit::pop_child() {
#pragma omp critical (reslimit_cancel)
{
m_children.pop_back();
}
lock_guard lock(g_rlimit_mux);
m_children.pop_back();
}
void reslimit::cancel() {
#pragma omp critical (reslimit_cancel)
{
set_cancel(m_cancel+1);
}
lock_guard lock(g_rlimit_mux);
set_cancel(m_cancel+1);
}
void reslimit::reset_cancel() {
#pragma omp critical (reslimit_cancel)
{
set_cancel(0);
}
lock_guard lock(g_rlimit_mux);
set_cancel(0);
}
void reslimit::inc_cancel() {
#pragma omp critical (reslimit_cancel)
{
set_cancel(m_cancel+1);
}
lock_guard lock(g_rlimit_mux);
set_cancel(m_cancel+1);
}
void reslimit::dec_cancel() {
#pragma omp critical (reslimit_cancel)
{
if (m_cancel > 0) {
set_cancel(m_cancel-1);
}
lock_guard lock(g_rlimit_mux);
if (m_cancel > 0) {
set_cancel(m_cancel-1);
}
}

7
src/util/rlimit.h
View file

@ -16,11 +16,11 @@ Author:
Revision History:
--*/
#ifndef RLIMIT_H_
#define RLIMIT_H_
#pragma once
#include "util/vector.h"
class reslimit {
volatile unsigned m_cancel;
bool m_suspend;
@ -88,6 +88,3 @@ struct scoped_limits {
~scoped_limits() { for (unsigned i = 0; i < m_sz; ++i) m_limit.pop_child(); }
void push_child(reslimit* lim) { m_limit.push_child(lim); ++m_sz; }
};
#endif

8
src/util/symbol.cpp
View file

@ -17,12 +17,14 @@ Revision History:
--*/
#include "util/symbol.h"
#include "util/mutex.h"
#include "util/str_hashtable.h"
#include "util/region.h"
#include "util/string_buffer.h"
#include "util/z3_omp.h"
#include <cstring>
static mutex g_symbol_lock;
symbol symbol::m_dummy(TAG(void*, nullptr, 2));
const symbol symbol::null;
@ -36,8 +38,7 @@ public:
char const * get_str(char const * d) {
const char * result;
#pragma omp critical (cr_symbol)
{
lock_guard lock(g_symbol_lock);
str_hashtable::entry * e;
if (m_table.insert_if_not_there_core(d, e)) {
// new entry
@ -55,7 +56,6 @@ public:
result = e->get_data();
}
SASSERT(m_table.contains(result));
}
return result;
}
};

25
src/util/util.cpp
View file

@ -17,12 +17,17 @@ Revision History:
--*/
#ifdef _WINDOWS
#include <windows.h>
#endif
#include <thread>
#include "util/util.h"
#ifndef SINGLE_THREAD
#include <mutex>
#include <thread>
static std::mutex g_verbose_mux;
void verbose_lock() { g_verbose_mux.lock(); }
void verbose_unlock() { g_verbose_mux.unlock(); }
#endif
static unsigned g_verbosity_level = 0;
void set_verbosity_level(unsigned lvl) {
@ -39,23 +44,13 @@ void set_verbose_stream(std::ostream& str) {
g_verbose_stream = &str;
}
#ifndef _NO_OMP_
#ifdef _WINDOWS
static int g_thread_id = 0;
#else
#ifndef SINGLE_THREAD
static std::thread::id g_thread_id = std::this_thread::get_id();
#endif
static bool g_is_threaded = false;
bool is_threaded() {
if (g_is_threaded) return true;
#ifdef _WINDOWS
int thid = GetCurrentThreadId();
g_is_threaded = g_thread_id != thid && g_thread_id != 0;
g_thread_id = thid;
#else
g_is_threaded = std::this_thread::get_id() != g_thread_id;
#endif
return g_is_threaded;
}
#endif

59
src/util/util.h
View file

@ -16,12 +16,10 @@ Author:
Revision History:
--*/
#ifndef UTIL_H_
#define UTIL_H_
#pragma once
#include "util/debug.h"
#include "util/memory_manager.h"
#include "util/z3_omp.h"
#include<iostream>
#include<climits>
#include<limits>
@ -47,14 +45,10 @@ static_assert(sizeof(int64_t) == 8, "64 bits");
#endif
#ifdef _WINDOWS
#define SSCANF sscanf_s
// #define SPRINTF sprintf_s
#define SPRINTF_D(_buffer_, _i_) sprintf_s(_buffer_, Z3_ARRAYSIZE(_buffer_), "%d", _i_)
#define SPRINTF_U(_buffer_, _u_) sprintf_s(_buffer_, Z3_ARRAYSIZE(_buffer_), "%u", _u_)
#define _Exit exit
#else
#define SSCANF sscanf
// #define SPRINTF sprintf
#define SPRINTF_D(_buffer_, _i_) sprintf(_buffer_, "%d", _i_)
#define SPRINTF_U(_buffer_, _u_) sprintf(_buffer_, "%u", _u_)
#endif
@ -174,7 +168,7 @@ void set_verbosity_level(unsigned lvl);
unsigned get_verbosity_level();
std::ostream& verbose_stream();
void set_verbose_stream(std::ostream& str);
#ifdef _NO_OMP_
#ifdef SINGLE_THREAD
# define is_threaded() false
#else
bool is_threaded();
@ -191,24 +185,19 @@ bool is_threaded();
} \
} } ((void) 0)
#ifdef _MSC_VER
#define DO_PRAGMA(x) __pragma(x)
#define PRAGMA_LOCK __pragma(omp critical (verbose_lock))
#else
#define DO_PRAGMA(x) _Pragma(#x)
#define PRAGMA_LOCK _Pragma("omp critical (verbose_lock)")
#endif
#ifdef _NO_OMP_
#ifdef SINGLE_THREAD
#define LOCK_CODE(CODE) CODE;
#else
#define LOCK_CODE(CODE) \
{ \
PRAGMA_LOCK \
{ \
CODE; \
} \
}
void verbose_lock();
void verbose_unlock();
#define LOCK_CODE(CODE) \
{ \
verbose_lock(); \
CODE; \
verbose_unlock(); \
}
#endif
template<typename T>
@ -292,20 +281,6 @@ inline std::ostream & operator<<(std::ostream & out, std::pair<T1, T2> const & p
return out;
}
template<typename IT>
bool has_duplicates(const IT & begin, const IT & end) {
for (IT it1 = begin; it1 != end; ++it1) {
IT it2 = it1;
++it2;
for (; it2 != end; ++it2) {
if (*it1 == *it2) {
return true;
}
}
}
return false;
}
#ifndef _WINDOWS
#ifndef __declspec
#define __declspec(X)
@ -376,12 +351,6 @@ void shuffle(unsigned sz, T * array, random_gen & gen) {
}
}
#ifdef _EXTERNAL_RELEASE
#define INTERNAL_CODE(CODE) ((void) 0)
#else
#define INTERNAL_CODE(CODE) { CODE } ((void) 0)
#endif
void fatal_error(int error_code);
void set_fatal_error_handler(void (*pfn)(int error_code));
@ -420,7 +389,3 @@ inline size_t megabytes_to_bytes(unsigned mb) {
r = SIZE_MAX;
return r;
}
#endif /* UTIL_H_ */

1
src/util/z3_exception.cpp
View file

@ -16,7 +16,6 @@ Author:
Notes:
--*/
#include<sstream>
#include<stdarg.h>
#include<sstream>
#include "util/z3_exception.h"

38
src/util/z3_omp.h
View file

@ -1,38 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
z3_omp.h
Abstract:
Wrapper for OMP functions and data-structures
Author:
Leonardo (leonardo) 2012-01-05
Notes:
--*/
#ifndef Z3_OMP_H_
#define Z3_OMP_H_
#ifndef _NO_OMP_
#include<omp.h>
#else
#define omp_in_parallel() false
#define omp_set_num_threads(SZ) ((void)0)
#define omp_get_thread_num() 0
#define omp_get_num_procs() 1
#define omp_set_nested(V) ((void)0)
#define omp_init_nest_lock(L) ((void) 0)
#define omp_destroy_nest_lock(L) ((void) 0)
#define omp_set_nest_lock(L) ((void) 0)
#define omp_unset_nest_lock(L) ((void) 0)
struct omp_nest_lock_t {
};
#endif
#endif