Sail spawns z3 a bajillion times

[jevinskie]

When building the ARMv9.3 model I noticed sail wasn’t using much CPU and sampled it to find that it was spawning/exec’ing z3 probably 100k—1 million times, sometimes with a temp file and sometimes using pipes. Undoubtedly this slows things down (the degree to which I haven’t determined and cannot until I try implementing my idea), especially since it seems to be using OCaml’s equivalent of libc’s system() that also (uselessly?) spawns the shell just to spawn the z3 executable. I’m taking a stab at using z3’s OCaml bindings to do everything in process.

Is there a reason this hasn’t been done already, perhaps related to memoization? Would such a change be welcomed for upstreaming?

[Alasdair]

The problem I've had with Z3's API in the past is it makes it much harder to distribute the software, as it ties you to a specific version of Z3. By using the Z3 binary we just work on whatever creaky version of CentOS or similarly vintage linux distro someone is using.

Avoiding using a temp file would be good. I vaguely remember there was some reason I didn't use pipes, but it was so long ago I can't remember the details (maybe it was something timeout related...). I know using a temp file can be slow if the temp directory isn't backed by tmpfs.

[PeterSewell]

Presumably Sail's caching means this matters less than one might think, too, except on a first build.

On Sat, 23 Dec 2023 at 09:52, Alasdair Armstrong @.***> wrote:

The problem I've had with Z3's API in the past is it makes it much harder to distribute the software, as it ties you to a specific version of Z3. By using the Z3 binary we just work on whatever creaky version of CentOS or similarly vintage linux distro someone is using.

Avoiding using a temp file would be good. I vaguely remember there was some reason I didn't use pipes, but it was so long ago I can't remember the details (maybe it was something timeout related...). I know using a temp file can be slow if the temp directory isn't backed by tmpfs.

— Reply to this email directly, view it on GitHub https://github.com/rems-project/sail/issues/410#issuecomment-1868256344, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABFMZZTR5KFM2CL54Y5ULD3YK2SVLAVCNFSM6AAAAABBAVQDROVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTQNRYGI2TMMZUGQ . You are receiving this because you are subscribed to this thread.Message ID: @.***>

[Alasdair]

Having faster initial builds would be nice. Avoiding using the shell by using Unix.open_process_args_full is something we can easily do now we aren't in the OCaml 4.06 days anymore at least.

[Alasdair]

After trying open_process_args_full it seemed to fail in CI despite working on my machine. Not sure why yet.