Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Per-session kore-rpc server state #3702

Closed
wants to merge 4 commits into from

Conversation

goodlyrottenapple
Copy link
Member

@goodlyrottenapple goodlyrottenapple commented Dec 6, 2023

In order to use the kore-rpc server concurrently in a safe way, we modify the server to create a new server state per each session. This way, each client will get the same initial server state and calls to add-module will always be safe, because the added modules are per session and not shared between different clients. This of course means that each client has to send the required modules to the server separately.

Part of runtimeverification/hs-backend-booster#383

@goodlyrottenapple goodlyrottenapple requested review from jberthold and geo2a and removed request for jberthold December 6, 2023 16:46
Copy link
Member

@jberthold jberthold left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM .. .although unclear how kore-rpc-client should change to use that

@tothtamas28
Copy link
Contributor

The ability to share modules between clients in a controlled way can be very useful, I'd prefer a solution that enables that. Did you consider the proposal under runtimeverification/hs-backend-booster#383 (comment)?

@goodlyrottenapple
Copy link
Member Author

The ability to share modules between clients in a controlled way can be very useful, I'd prefer a solution that enables that.

Is this due to performance? Do you expect these modules to be very big?

Did you consider the proposal under runtimeverification/hs-backend-booster#383 (comment)?

I was working under the assumption that we simply want to avoid module clashes and tweaking the global state to only be a session state seemed like a much simpler solution. Using IDs and especially importing modules via IDs whilst maintaining module names completely disjoint from said IDs seemed a much more substantial change to both back-ends.

@tothtamas28
Copy link
Contributor

Is this due to performance? Do you expect these modules to be very big?

No, it's for ease of programming against the API.

Using IDs and especially importing modules via IDs whilst maintaining module names completely disjoint from said IDs seemed a much more substantial change to both back-ends.

Implementation effort should of course be taken into consideration. Can you post your feedback on the design issue so that we can iterate on it?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

4 participants