From ad0b75b18995785b3e6f2c7e4657e7e6af916088 Mon Sep 17 00:00:00 2001
From: Hans-Peter Deifel <hans-peter.deifel@fau.de>
Date: Sat, 25 Mar 2017 22:11:34 +0100
Subject: [PATCH] tests: Run reasoner in new process for each formula
As it stands, cool leaks tons of memory with each `isSat` call. Until
this is fixed, the new `--slow` testsuite would need at least 16GB of
memory if all formulas are decided in one process. Thus, we now call
isSat in a new child-process and allow the OS to reclaim memory after
the child exits.
NB: This uses the Unix.fork API, which is not available on Windows.
---
src/testsuite/Testsuite.ml | 11 +++++++++--
1 file changed, 9 insertions(+), 2 deletions(-)
diff --git a/src/testsuite/Testsuite.ml b/src/testsuite/Testsuite.ml
index f23799a..537e97e 100644
--- a/src/testsuite/Testsuite.ml
+++ b/src/testsuite/Testsuite.ml
@@ -38,8 +38,15 @@ let runSatCheck (_,logic,input) =
Some 0
in
let (tbox, f) = CoAlgFormula.importQuery input in
- let res = CoAlgReasoner.isSat logic nomTable tbox f in
- if res then Sat else Unsat
+ (* isSat leaks tons of memory. Call it in new process to allow the OS to
+ reclaim that memory between calls. *)
+ match Unix.fork () with
+ | 0 -> let res = CoAlgReasoner.isSat logic nomTable tbox f in
+ if res then exit 0 else exit 1
+ | -1 -> raise (CoAlgFormula.CoAlgException "fork() failed")
+ | _ -> match Unix.wait () with
+ | (_,Unix.WEXITED 0) -> Sat
+ | _ -> Unsat
with | Stream.Error _ -> ParseError
| CoAlgFormula.CoAlgException _ -> ParseError
--
GitLab