Multi-Grained Specifications for Distributed System Model Checking and Verification
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914972590669824 |
|---|---|
| author | Ouyang, Lingzhi Sun, Xudong Tang, Ruize Huang, Yu Jivrajani, Madhav Ma, Xiaoxing Xu, Tianyin |
| author_facet | Ouyang, Lingzhi Sun, Xudong Tang, Ruize Huang, Yu Jivrajani, Madhav Ma, Xiaoxing Xu, Tianyin |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2409_14301 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Multi-Grained Specifications for Distributed System Model Checking and Verification Ouyang, Lingzhi Sun, Xudong Tang, Ruize Huang, Yu Jivrajani, Madhav Ma, Xiaoxing Xu, Tianyin Distributed, Parallel, and Cluster Computing Software Engineering 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. |
| title | Multi-Grained Specifications for Distributed System Model Checking and Verification |
| topic | Distributed, Parallel, and Cluster Computing Software Engineering |
| url | https://arxiv.org/abs/2409.14301 |