EOF error when running multiple programs with `synthesize` queries

[kach]

Hi Rosette team,

TL;DR: When I run multiple different Rosette programs in parallel, synthesize queries reliably fail with the error read-solution: unrecognized solver output: #<eof>.

Longer explanation: I'm working on a small project which uses Rosette to synthesize small programs (via the (synthesize #:forall … #:guarantee …) query). In my project, I am interested in how different specifications lead to different synthesized programs. So, to test my system, I would like to run the synthesizer about ~30 times with various different specifications.

Each synthesis query takes about an hour, so it would be extremely convenient to run all 30 queries in parallel on a machine with many cores. I can do this by launching 30 jobs using the following Bash command:

for i in `seq 0 29`; do racket synthesize.rkt $i & done

Unfortunately, when I do that I get the following error:

read-solution: unrecognized solver output: #<eof>
  context...:
   /home/kach/.local/share/racket/8.10/pkgs/rosette/rosette/solver/smt/base-solver.rkt:136:0: read-solution
   /home/kach/.local/share/racket/8.10/pkgs/rosette/rosette/solver/smt/base-solver.rkt:95:0: solver-check
   /home/kach/.local/share/racket/8.10/pkgs/rosette/rosette/query/core.rkt:157:2: guess
   /home/kach/.local/share/racket/8.10/pkgs/rosette/rosette/query/core.rkt:151:0: cegis
   /home/kach/.local/share/racket/8.10/pkgs/rosette/rosette/query/core.rkt:129:6
   /home/kach/.local/share/racket/8.10/pkgs/rosette/rosette/base/form/control.rkt:16:25

This error occurs using both z3 and cvc4 solver backends, but does not occur if I run the tasks in serial.

I'm wondering if there is some issue with how Rosette launches the subprocess for the solver, which manifests itself only when there are other Rosette processes running at the same time. For example, is there maybe a temporary file that gets corrupted if multiple processes are modifying it at once?

For reference, this occurs with the latest Rosette via (raco pkg install) on Ubuntu 22.04.3 LTS.

Thank you for your help! I love Rosette! 🙂

Best wishes, Kartik

[sorawee]

I cannot reproduce the issue. Could you provide the Z3 version that you are using, along with the content of synthesize.rkt?

[kach]

Hi Sorawee - Thank you for trying to reproduce the issue! I'm using Z3 version 4.8.8 - 64 bit (the one bundled with Rosette). Could I send you synthesize.rkt by email? It is quite a large program with several files, and I would prefer not to post it publicly right now.

[sorawee]

Yes! My email is sorawee.pwase@gmail.com

[kach]

Okay, will follow up by email!

[sorawee]

Issue resolved (the underlying issue is that the resource ran out).