Sharpen the Spec, Cut the Code A Case for Generative File System with SYSSPEC

Sharpen the Spec, Cut the Code: A Case for Generative File System with SYSSPEC link

Design

• (1) Functionality specifications, which use concepts like Hoare logic (pre/post-conditions) and invariants to describe the behavior of individual modules.
  • Specification methods
    • pre- and post-conditions, following Hoare Logic, define the contractual obligations for each function by specifying the required state before execution and the guaranteed state upon completion.
    • invariants are properties that must hold true across all state transitions, ensuring the module’s integrity
    • a system algorithm outlines the high-level logic for how a function should achieve its state transition, guiding the LLM’s implementation strategy. A high-level intent is often sufficient. The intent can be regarded as a lightweight system algorithm that, expressed in natural language, guides the LLM in generating the desired implementation.
• (2) Modularity specifications, which decompose the system into distinct components and use a rely-guarantee discipline [21] to ensure they can be composed correctly and developed independently.
  • (1) module implementations must respect their declared dependencies (Rely)
  • (2) provide guarantees about their behavior (Guarantee)
  • (3) compose through logical implication of these contracts
• (3) Concurrency specifications, which explicitly define locking protocols and other concurrency-related behaviors that are notoriously difficult for LLMs to infer on their own.
  • During code generation, our toolchain first directs the LLM to generate a correct sequential version of the code, focusing only on the primary functionality.
  • In a second pass, using the dedicated concurrency specification to instrument the code with the required locking and other concurrent behaviors

The SYSSPEC Toolchain

• SpecCompiler
  • Two-phase prompting
    • First phase, it generates a correct sequential implementation of the module, focusing only on its core functionality.
    • Second phase, it uses the dedicated concurrency specification to instrument this sequential code with the necessary locking and concurrent behaviors.
  • Retry-with-feedback loop used within each phase: a CodeGen agent generates the implementation, and a separate, reasoning-focused SpecEval agent reviews the output against the specification. If the SpecEval agent identifies a flaw, it does not simply report failure; instead, it generates specific, actionable feedback (e.g., “The case where function foo() fails is not handled”). This feedback is then appended to the original prompt, and the CodeGen agent retries. This refinement cycle continues until the generated code satisfies the specification or an attempt-limit is reached.