Introduction
Isabelle Service Manager (ISM) is a supervisor and transparent load balancer intended to orchestrate the isabelle server.
It was created to augment the ProofBuddy backend by providing a transparent isabelle server load balancer to scale beyond a single Isabelle server instance. ISM also aims to ensure Isabelle server instances are isolated from the rest of the server environment with minimal overhead.
The main goals are:
- Availability: Ensure the backend can always create new sessions. This will eventually include clustered operation of ISM.
- Resilience: Ensure server failures and corrupt states are detected and handled
- Security: Ensure servers are isolated from each other and the host.
Additionally, ISM aims to achieve a low latency overhead and resource usage.
Documentation
The ISM documentation is split into two parts:
- internals: Documentation for developers and operators
- users: Documentation for developers connecting via clients
Both parts have different target audiences and expect a different set of preexisting knowledge.
The users documentation assumes familiarity with:
- Isabelle: server and related components
- (for
isalink) Golang: Basic knowledge about language - (for
isa-bench): Basic knowledge around JavaScript and k6
The internals documentation assumes familiarity with:
- Isabelle: server and related components
- Golang: Basic Language knowledge around concurrent and network programming
- Linux: Basic knowledge around the network stack, cgroups, namespaces (user, network) and security
- systemd: Basic knowledge around services and cgroups integration