search

runtimeverification / k

K Framework Tools 7.0
BSD 3-Clause "New" or "Revised" License
450 stars 149 forks source link

Launch and manage `kserver` when needed #4218

Open ehildenb opened 1 year ago

ehildenb commented 1 year ago

It would be good for pyk to be smarter about launching/managing kserver process, or at least expose functionality for the user to do so when there is a chance that they may need it. Examples include when the user will do lots of proofs, and they need to parse each specification and we want to use a shared pool of z3 processes (see https://github.com/runtimeverification/k/issues/3551), or we want ot limit the startup time of calls to kast.

Ideally, pyk would be smart enough to only start one kserver per project/directory/definition, whatever the relevant granularity is. I think kserver is actually only specific to th eversion of K itself, not to the definition, so maybe we could have a way of launching kservers in a specific temporary directory where they are labelled by K version. Then when we go to launch more kservers, we check first "is one already launched for this version of K?", and if so, just use the existing one.

tothtamas28 commented 1 year ago

Would a simple context manager work?

with kserver():
    kompile('defn-1.k')
    kompile('defn-2.k')
    ...
ehildenb commented 1 year ago

That should probably be fine, yes.

radumereuta commented 1 year ago

I'm not sure if the version specific kserver is true. @dwightguth might know more. Better to check. Keep in mind that kserver also has a level of caching. If something changes in the definition, then you need to restart kserver in order to clear the caches.

ehildenb commented 1 year ago

Does spawn-kserver take any arguments? How can it be definition specific if it doesn't take arguments about which definition to be caching? I thought it was juts keeping a warmed up JVM around?

dwightguth commented 1 year ago

I believe the only thing it's caching currently is the deserialized definition, which it just caches whenever you load it the first time based on its path on disk.