search

rems-project / cerberus

Cerberus C semantics
https://www.cl.cam.ac.uk/~pes20/cerberus/
Other
42 stars 19 forks source link

[CN] the solver is using a lot of pipes #369

Open kmemarian opened 2 weeks ago

kmemarian commented 2 weeks ago

When running the CN ci tests (tests/run-cn.sh) on macOS (tested on 14.5) 10 tests fail because the cn process runs out of file descriptors (the macOS's default soft limit appears to be 256):

10 tests failed:
   ./cn/tree16/as_partial_map/tree16.c ./cn/tree16/as_mutual_dt/tree16.c ./cn/fun_ptr_three_opts.c ./cn/list_rev01.c ./cn/append.c ./cn/reverse.c ./cn/mutual_rec/mutual_rec.c ./cn/fun_ptr_known.c ./cn/mergesort.c ./cn/fun_ptr_extern.c

I think that the issue is a result of:

  1. every call to Simple_smt.new_solver opens 3 pipes as a result of the call to Unix.open_process_args_full.
  2. every call to Solver.model_evaluator _ _ (called from Solver.provable) creates a new solver, whose lifetime extends until the end of the execution of CN (?).
septract commented 2 weeks ago

cc @yav

yav commented 2 weeks ago

I don't see a way around (1), but we could change (2) to start a solver only when it needs to evaluate in the context of a model, and end the solver when it is done. It will likely make model evaluation a bit slower because we'll pay the start up cost multiple times, but I am not sure if that matters.

Another option for (2) would be to change the API to bracket calls to the model evaluator (e..g, something like with_model_evaluator f where f will be given a solver setup with the particular model.

Thoughts?