Repository navigation
Containerization safe mode - #30
Conversation
…o containerization-safe-mode
daniel-larraz
left a comment
daniel-larraz
left a comment
There was a problem hiding this comment.
I found 7 problems in this PR. The first (safeMode null check) breaks every existing caller, even with safe mode off; the rest affect safe mode.
daniel-larraz
left a comment
daniel-larraz
left a comment
There was a problem hiding this comment.
Follow-up review of 920aae8.
Fixed: safeMode null checks, z3Bin null handling, per-instance CPU/memory/swap limits, and the absolute-path check for KIND2 (now applied to the interpreter path too). Thanks!
Partly fixed: solver mounts (target names don't match the fixed paths in getOptions; smtinterpol can't work) and swap/memory consistency (the swap setter isn't checked, and units are 1000-based).
Not fixed: commas in mounted paths. The new space escaping also breaks paths that contain spaces, which worked before.
New: setApiDebug() in callKind2 writes a debug file on every run.
Details are in the inline comments.
daniel-larraz
left a comment
daniel-larraz
left a comment
There was a problem hiding this comment.
Follow-up review of 58e981a.
Everything from the last round is addressed: mount paths are now CSV-quoted (commas and spaces both work), solvers and Kind 2 are mounted at the fixed paths getOptions uses, smtinterpol's paths match and the image now includes Java, the swap setter is checked against the memory limit, units are 1024-based, and the leftover setApiDebug() call is gone. Thanks!
One remaining bug in memoryValueToBytes (uppercase units) and a stale comment. Details are in the inline comments.
Adds configurable CPU, memory, and swap limits for Kind 2 executions running in safe mode. The language server now reads the following environment variables: - `KIND2_SAFE_MODE_CPU` - `KIND2_SAFE_MODE_MEMORY` - `KIND2_SAFE_MODE_SWAP` When safe mode is enabled, these values are applied to each `Kind2Api` instance before executing Kind 2. The gateway also forwards these settings to the language server and provides defaults of `2.0` CPUs, `2g` of physical memory, and `2g` of combined memory and swap. The README has been updated with documentation and examples for configuring these limits on Linux/macOS, PowerShell, and Command Prompt. ## Changes - Added safe mode CPU, memory, and swap environment variables to the gateway. - Added parsing and propagation of those values in the language server. - Applied configured resource limits through the Kind 2 Java API. - Added logging of the active safe mode resource limits. - Documented the new configuration options and defaults in the README. This PR is dependent on [LSP PR 30](kind2-mc/kind2-java-api#30), as the API needs to handle the usage limit method calls. --------- Co-authored-by: Daniel Larraz <daniel-larraz@users.noreply.github.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
2 participants
Adds Docker-backed safe mode execution to the Kind 2 Java API.
When safe mode is enabled, Kind 2 executions are launched inside a Docker container with configurable CPU, memory, and swap limits. The configured Kind 2 executable and solver binaries are mounted into the container and exposed through fixed container paths.
Interpreter execution has also been updated to support safe mode. Generated interpreter input files, and Lustre files when using the URI-based interpreter API, are mounted read-only into the container before Kind 2 is started.
Changes
safeModeis enabled.