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.

Sign up for GitHub

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

Jump to bottom

Example: Two-layered Cache #1549

Open

mt40 wants to merge 1 commit into informalsystems:main from mt40:main

mt40 commented Nov 11, 2024

Continued from this thread: #1548 (comment)

This is a design of an imagined Two-layered Cache with the following behaviors:

2 layer, N keys, 1 server/cache process, 1 client process

read from Layer 1, if not exists then Layer 2

if key is found in Layer 2, write back to Layer 1

expire time passed = key not exist

Correctness:

strong consistency: any read returns the latest written value

validity: any read returns a non-expired value

Model checking output:

Launching Apalache server
[ok] No violation found (187959ms).
You may increase --max-steps.
Use --verbosity to produce more (or less) output.
Shutting down Apalache server


          Create twolayeredcache

44efe35

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet