Multi-Grained Specifications for Distributed System Model Checking and Verification

• URL: http://arxiv.org/abs/2409.14301v3
• Date: Fri, 27 Sep 2024 08:15:53 GMT
• Title: Multi-Grained Specifications for Distributed System Model Checking and Verification
• Abstract summary: We use TLA+ to model fine-grained behaviors of ZooKeeper and the TLC model checker to verify its correctness properties. We show that writing multi-grained specifications is a viable practice and can cope with model-code gaps without untenable state space.
• Score: 9.14614889088682
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: This paper presents our experience specifying and verifying the correctness of ZooKeeper, a complex and evolving distributed coordination system. We use TLA+ to model fine-grained behaviors of ZooKeeper and use the TLC model checker to verify its correctness properties; we also check conformance between the model and code. The fundamental challenge is to balance the granularity of specifications and the scalability of model checking -- fine-grained specifications lead to state-space explosion, while coarse-grained specifications introduce model-code gaps. To address this challenge, we write specifications with different granularities for composable modules, and compose them into mixed-grained specifications based on specific scenarios. For example, to verify code changes, we compose fine-grained specifications of changed modules and coarse-grained specifications that abstract away details of unchanged code with preserved interactions. We show that writing multi-grained specifications is a viable practice and can cope with model-code gaps without untenable state space, especially for evolving software where changes are typically local and incremental. We detected six severe bugs that violate five types of invariants and verified their code fixes; the fixes have been merged to ZooKeeper. We also improve the protocol design to make it easy to implement correctly.

Related papers

• Specification-delta-driven data governance: an empirical study of the «spec-delta» as the unit of change in lakehouse data platforms [0.0]
  Spec Driven Development SDD has consolidated the idea that the specification rather than the code should be the primary artefact governing AI assisted work.<n>This work formalises the spec-delta concept, proposes a taxonomy of data platform changes according to their suitability for incremental specification.<n>The paper explicitly reserves a demonstration-and-laboratory section for instantiation on a real lakehouse environment.
  arXiv  Detail & Related papers  (2026-08-20T09:38:48Z)
• Specula: Scaling formal specifications for autonomous model checking of system code [8.484545401876316]
  Specula is a push-button agentic system that generates high-quality formal specifications for large, complex system code.<n>Specula employs large language model (LLM) based coding agents to autonomously develop TLA+ specifications.
  arXiv  Detail & Related papers  (2026-07-28T06:33:15Z)
• Evaluating LLMs on Java Code Snippet Adaptation Using a Mutation-Injection Framework [9.514883757685725]
  Developers frequently reuse code by copying fragments and adapting them to fit new contexts.<n>Existing benchmarks for evaluating large language models (LLMs) on code adaptation either rely on explicit step-by-step instructions, cover only narrow change types such as variable wiring, or operate exclusively at function-level granularity.<n>We investigate instruction-free code snippet adaptation in which an LLM must adapt a code fragment to fit its target context without any explicit edit guidance.
  arXiv  Detail & Related papers  (2026-06-26T21:34:33Z)
• SpecAlign: Efficient Specification-Grounded Alignment of Large Language Models via Synthetic Data [46.83043333985018]
  We propose specification-grounded alignment, a new alignment paradigm that treats provider-authored model specifications as the primary alignment target.<n>We introduce SpecAlign, a framework that synthesizes alignment data directly from specification documents.
  arXiv  Detail & Related papers  (2026-06-15T06:30:52Z)
• What Semantics Survive the Connector? Diagnosing VLM-to-DiT Alignment in Video Editing [59.40855219373921]
  Flow matching based video generative models rely on prepended Vision-Language Models to handle complex, instruction-based video editing.<n>The prevailing assumption is that a connector module can seamlessly align the VLM's rich multi-modal reasoning with the original text embedding space of DiTs.<n>We propose a controlled data processing pipeline based on video composition that results in TRACE-Edit, a diagnostic dataset focusing on relation-based editing.
  arXiv  Detail & Related papers  (2026-05-20T06:42:15Z)
• FMBench: Adaptive Large Language Model Output Formatting [49.52930069696333]
  We present FMBench, a benchmark for adaptive Markdown output formatting.<n>Experiments on two model families show that SFT consistently improves semantic alignment.<n>Results also reveal an inherent trade-off between semantic and structural objectives.
  arXiv  Detail & Related papers  (2026-02-06T04:42:06Z)
• Every Step Counts: Decoding Trajectories as Authorship Fingerprints of dLLMs [63.82840470917859]
  We show that the decoding mechanism of dLLMs can be used as a powerful tool for model attribution.<n>We propose a novel information extraction scheme called the Directed Decoding Map (DDM), which captures structural relationships between decoding steps and better reveals model-specific behaviors.
  arXiv  Detail & Related papers  (2025-10-02T06:25:10Z)
• LOCOFY Large Design Models -- Design to code conversion solution [0.0]
  We introduce the Large Design Models paradigm specifically trained on designs and webpages to enable seamless conversion from design-to-code.<n>We have developed a training and inference pipeline by incorporating data engineering and appropriate model architecture modification.<n>Our models illustrated exceptional end-to-end design-to-code conversion accuracy using a novel preview match score metric.
  arXiv  Detail & Related papers  (2025-07-22T03:54:57Z)
• LayoutRAG: Retrieval-Augmented Model for Content-agnostic Conditional Layout Generation [34.39449499558055]
  Controllable layout generation aims to create plausible visual arrangements of element bounding boxes within a graphic design.<n>We propose to carry out layout generation through retrieving by conditions and reference-guided generation.<n>Our method successfully produces high-quality layouts that meet the given conditions and outperforms existing state-of-the-art models.
  arXiv  Detail & Related papers  (2025-06-03T09:47:03Z)
• Robust Learning of Diverse Code Edits [10.565439872488328]
  Software engineering activities frequently involve edits to existing code. Code language models (LMs) lack the ability to handle diverse types of code-edit requirements.
  arXiv  Detail & Related papers  (2025-03-05T16:39:04Z)
• Multi-Convformer: Extending Conformer with Multiple Convolution Kernels [64.4442240213399]
  We introduce Multi-Convformer that uses multiple convolution kernels within the convolution module of the Conformer in conjunction with gating. Our model rivals existing Conformer variants such as CgMLP and E-Branchformer in performance, while being more parameter efficient. We empirically compare our approach with Conformer and its variants across four different datasets and three different modelling paradigms and show up to 8% relative word error rate(WER) improvements.
  arXiv  Detail & Related papers  (2024-07-04T08:08:12Z)
• Validating Traces of Distributed Programs Against TLA+ Specifications [0.0]
  We present a framework for relating traces of distributed programs to high-level specifications written in TLA+. The problem is reduced to a constrained model checking problem, realized using the TLC model checker. We have applied our approach to several distributed programs, detecting discrepancies between the specifications and the implementations in all cases.
  arXiv  Detail & Related papers  (2024-04-24T01:33:07Z)
• Towards Aligned Layout Generation via Diffusion Model with Aesthetic Constraints [53.66698106829144]
  We propose a unified model to handle a broad range of layout generation tasks. The model is based on continuous diffusion models. Experiment results show that LACE produces high-quality layouts.
  arXiv  Detail & Related papers  (2024-02-07T11:12:41Z)
• Fine-grained Controllable Video Generation via Object Appearance and Context [74.23066823064575]
  We propose fine-grained controllable video generation (FACTOR) to achieve detailed control. FACTOR aims to control objects' appearances and context, including their location and category. Our method achieves controllability of object appearances without finetuning, which reduces the per-subject optimization efforts for the users.
  arXiv  Detail & Related papers  (2023-12-05T17:47:33Z)
• Spreadsheet-based Configuration of Families of Real-Time Specifications [0.0]
  This work exploits variability of the formal model being analysed and the requirements being checked, to facilitate the model-checking of variations of real-time specifications. The configuration of the variability of the formal specifications is described in MS Excel spreadsheets with a particular structure, making it easy to use also by developers. We propose the extension of our previous work by exploiting analysis over valid combination of features, while preserving the simplicity of a spreadsheet-based interface with the model checker.
  arXiv  Detail & Related papers  (2023-10-31T12:16:56Z)
• Requirements Analysis of Variability Constraints in a Configurable Flight Software System [0.0]
  We report on our experience with the variability-related requirements constraints of a flight software framework used by multiple space missions. We propose a new software variability model, similar to a product-line feature model, in the flight software framework.
  arXiv  Detail & Related papers  (2023-09-06T22:56:39Z)
• SSMG: Spatial-Semantic Map Guided Diffusion Model for Free-form Layout-to-Image Generation [68.42476385214785]
  We propose a novel Spatial-Semantic Map Guided (SSMG) diffusion model that adopts the feature map, derived from the layout, as guidance. SSMG achieves superior generation quality with sufficient spatial and semantic controllability compared to previous works. We also propose the Relation-Sensitive Attention (RSA) and Location-Sensitive Attention (LSA) mechanisms.
  arXiv  Detail & Related papers  (2023-08-20T04:09:12Z)
• Adaptive Spot-Guided Transformer for Consistent Local Feature Matching [64.30749838423922]
  We propose Adaptive Spot-Guided Transformer (ASTR) for local feature matching. ASTR models the local consistency and scale variations in a unified coarse-to-fine architecture.
  arXiv  Detail & Related papers  (2023-03-29T12:28:01Z)
• Auditing AI models for Verified Deployment under Semantic Specifications [65.12401653917838]
  AuditAI bridges the gap between interpretable formal verification and scalability. We show how AuditAI allows us to obtain controlled variations for verification and certified training while addressing the limitations of verifying using only pixel-space perturbations.
  arXiv  Detail & Related papers  (2021-09-25T22:53:24Z)
• CARE: Coherent Actionable Recourse based on Sound Counterfactual Explanations [0.0]
  This paper introduces CARE, a modular explanation framework that addresses the model- and user-level desiderata. As a model-agnostic approach, CARE generates multiple, diverse explanations for any black-box model.
  arXiv  Detail & Related papers  (2021-08-18T15:26:59Z)
• Unsupervised Learning of General-Purpose Embeddings for Code Changes [6.652641137999891]
  We propose an approach for obtaining embeddings of code changes during pre-training. We evaluate them on two different downstream tasks - applying changes to code and commit message generation. Our model outperforms the model that uses full edit sequences by 5.9 percentage points in accuracy.
  arXiv  Detail & Related papers  (2021-06-03T19:08:53Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.