From a07fbf029a0172cb9f26c501127b8a91b07b0a6a Mon Sep 17 00:00:00 2001 From: Daniel Dunbar Date: Sat, 13 Sep 2014 18:28:59 -0700 Subject: [Solver] Tune down the shared memory region size on Darwin. - See comment, this is a gross workaround for Darwin's very small default limit on shared memory size. I'm not sure how big of a counterexample users can actually expect STP to solve in practice -- if there is a practical use for larger ones it would probably be good for us to write a fallback strategy. --- lib/Solver/Solver.cpp | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) (limited to 'lib') diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index d4e572cf..3903ab0d 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -518,8 +518,17 @@ public: }; static unsigned char *shared_memory_ptr; -static const unsigned shared_memory_size = 1<<20; static int shared_memory_id = 0; +// Darwin by default has a very small limit on the maximum amount of shared +// memory, which will quickly be exhausted by KLEE running its tests in +// parallel. For now, we work around this by just requesting a smaller size -- +// in practice users hitting this limit on counterexample sizes probably already +// are hitting more serious scalability issues. +#ifdef __APPLE__ +static const unsigned shared_memory_size = 1<<16; +#else +static const unsigned shared_memory_size = 1<<20; +#endif static void stp_error_handler(const char* err_msg) { fprintf(stderr, "error: STP Error: %s\n", err_msg); -- cgit 1.4.1