feat: spawn tasks for cosimulation to provide (theoretically) $nproc parallelism

[bollu]

Description:

This makes running cosimulation faster. This is nice for faster CI runs, where cosimulation appears to be the bottleneck.

Testing:

What tests have been run? Did make all succeed for your changes? Was conformance testing successful on an Aarch64 machine?

License:

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

[bollu]

When taking a walk, I realized that this can be made much cleaner by naming the files on the lean end. the Lean code knows how many tasks have been queued so far, and this can be passed as an argument to both disasm as well as cosim to name their files.

[shigoel]

I like where this is going!

[bollu]

Yay, it's in fact faster.

Old:

-- https://github.com/leanprover/LNSym/actions/runs/10378815072/job/28735781299#step:8:10474
real 585.45
user 405.94
sys 226.58

new (from this commit):

-- https://github.com/bollu/LNSym/actions/runs/10394146295/job/28783282692
real 451.05
user 650.40
sys 419.80

[bollu]

@alexkeizer comments addressed!

[shigoel]

Looks good!

For future work: I had a chat with @bollu and he suggested most time is spent assembling the reference binaries, so it could be an idea to cache those on disk. That would at least speed up local runs of conformance testing (and CI if we jump through the extra hoop of CI caching)

Another idea, which perhaps is out of scope right now, would be to do away with all these files. We could define one C/Asm function per instruction (which could be autogenerated from a list of instructions), and use shared object libraries to directly call these external functions in Lean.