VConMC: Enabling Consistency Verification for Distributed Systems Using Implementation-Level Model Checkers and Consistency Oracles
Many cloud services are relying on distributed key-value stores such as ZooKeeper, Cassandra, HBase, etc. However, distributed key-value stores are notoriously difficult to design and implement without any mistakes. Because data consistency is the contract for clients that defines what the correct v...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2024-03-01
|
| Series: | Electronics |
| Subjects: | |
| Online Access: | https://www.mdpi.com/2079-9292/13/6/1153 |
| _version_ | 1797241289747464192 |
|---|---|
| author | Beom-Heyn Kim |
| author_facet | Beom-Heyn Kim |
| author_sort | Beom-Heyn Kim |
| collection | DOAJ |
| description | Many cloud services are relying on distributed key-value stores such as ZooKeeper, Cassandra, HBase, etc. However, distributed key-value stores are notoriously difficult to design and implement without any mistakes. Because data consistency is the contract for clients that defines what the correct values to read are for a given history of operations under a specific consistency model, consistency violations can confuse client applications by showing invalid values. As a result, serious consequences such as data loss, data corruption, and unexpected behavior of client applications can occur. Software bugs are one of main reasons why consistency violations may occur. Formal verification techniques may be used to make designs correct and minimize the risks of having bugs in the implementation. However, formal verification is not a panacea due to limitations such as the cost of verification, inability to verify existing implementations, and human errors involved. Implementation-level model checking has been heavily explored by researchers for the past decades to formally verify whether the underlying implementation of distributed systems have bugs or not. Nevertheless, previous proposals are limited because their invariant checking is not versatile enough to check for the wide spectrum of consistency models, from eventual consistency to strong consistency. In this work, consistency oracles are employed for consistency invariant checking that can be used by implementation-level model checkers to formally verify data consistency model implementations of distributed key-value stores. To integrate consistency oracles with implementation-level distributed system model checkers, the partial-order information obtained via API is leveraged to avoid the exhaustive search during consistency invariant checking. Our evaluation results show that, by using the proposed method for consistency invariant checking, our prototype model checker, VConMC, can detect consistency violations caused by several real-world software bugs in a well-known distributed key-value store, ZooKeeper. |
| first_indexed | 2024-04-24T18:20:58Z |
| format | Article |
| id | doaj.art-1dc61dd6865c4f8ab8fcd85173e34ffe |
| institution | Directory Open Access Journal |
| issn | 2079-9292 |
| language | English |
| last_indexed | 2024-04-24T18:20:58Z |
| publishDate | 2024-03-01 |
| publisher | MDPI AG |
| record_format | Article |
| series | Electronics |
| spelling | doaj.art-1dc61dd6865c4f8ab8fcd85173e34ffe2024-03-27T13:35:07ZengMDPI AGElectronics2079-92922024-03-01136115310.3390/electronics13061153VConMC: Enabling Consistency Verification for Distributed Systems Using Implementation-Level Model Checkers and Consistency OraclesBeom-Heyn Kim0Department of Computer Science and Engineering, Hanyang University, Ansan 15588, Republic of KoreaMany cloud services are relying on distributed key-value stores such as ZooKeeper, Cassandra, HBase, etc. However, distributed key-value stores are notoriously difficult to design and implement without any mistakes. Because data consistency is the contract for clients that defines what the correct values to read are for a given history of operations under a specific consistency model, consistency violations can confuse client applications by showing invalid values. As a result, serious consequences such as data loss, data corruption, and unexpected behavior of client applications can occur. Software bugs are one of main reasons why consistency violations may occur. Formal verification techniques may be used to make designs correct and minimize the risks of having bugs in the implementation. However, formal verification is not a panacea due to limitations such as the cost of verification, inability to verify existing implementations, and human errors involved. Implementation-level model checking has been heavily explored by researchers for the past decades to formally verify whether the underlying implementation of distributed systems have bugs or not. Nevertheless, previous proposals are limited because their invariant checking is not versatile enough to check for the wide spectrum of consistency models, from eventual consistency to strong consistency. In this work, consistency oracles are employed for consistency invariant checking that can be used by implementation-level model checkers to formally verify data consistency model implementations of distributed key-value stores. To integrate consistency oracles with implementation-level distributed system model checkers, the partial-order information obtained via API is leveraged to avoid the exhaustive search during consistency invariant checking. Our evaluation results show that, by using the proposed method for consistency invariant checking, our prototype model checker, VConMC, can detect consistency violations caused by several real-world software bugs in a well-known distributed key-value store, ZooKeeper.https://www.mdpi.com/2079-9292/13/6/1153cloud servicedistributed key-value storemodel checkingsoftware testingdata consistency |
| spellingShingle | Beom-Heyn Kim VConMC: Enabling Consistency Verification for Distributed Systems Using Implementation-Level Model Checkers and Consistency Oracles Electronics cloud service distributed key-value store model checking software testing data consistency |
| title | VConMC: Enabling Consistency Verification for Distributed Systems Using Implementation-Level Model Checkers and Consistency Oracles |
| title_full | VConMC: Enabling Consistency Verification for Distributed Systems Using Implementation-Level Model Checkers and Consistency Oracles |
| title_fullStr | VConMC: Enabling Consistency Verification for Distributed Systems Using Implementation-Level Model Checkers and Consistency Oracles |
| title_full_unstemmed | VConMC: Enabling Consistency Verification for Distributed Systems Using Implementation-Level Model Checkers and Consistency Oracles |
| title_short | VConMC: Enabling Consistency Verification for Distributed Systems Using Implementation-Level Model Checkers and Consistency Oracles |
| title_sort | vconmc enabling consistency verification for distributed systems using implementation level model checkers and consistency oracles |
| topic | cloud service distributed key-value store model checking software testing data consistency |
| url | https://www.mdpi.com/2079-9292/13/6/1153 |
| work_keys_str_mv | AT beomheynkim vconmcenablingconsistencyverificationfordistributedsystemsusingimplementationlevelmodelcheckersandconsistencyoracles |