2020-09-14
Automated Validation of State-Based Client-Centric Isolation with TLA+
Publication
Publication
Clear consistency guarantees on data are paramount for the design and implementation of distributed systems. When implementing distributed applications, developers require approaches to verify the data consistency guarantees of an implementation choice. Crooks et al. define a state-based and client-centric model of database isolation. This paper formalizes this state-based model in Open image in new window , reproduces their examples and shows how to model check runtime traces and algorithms with this formalization. The formalized model in Open image in new window enables semi-automatic model checking for different implementation alternatives for transactional operations and allows checking of conformance to isolation levels. We reproduce examples of the original paper and confirm the isolation guarantees of the combination of the well-known 2-phase locking and 2-phase commit algorithms. Using model checking this formalization can also help finding bugs in incorrect specifications. This improves feasibility of automated checking of isolation guarantees in synthesized synchronization implementations and it provides an environment for experimenting with new designs.
| Additional Metadata | |
|---|---|
| ING Bank | |
| doi.org/10.1007/978-3-030-67220-1_4 | |
| Lecture Notes in Computer Science | |
| International Conference on Software Engineering and Formal Methods | |
| Organisation | Software Analysis and Transformation |
|
Soethout, T., van der Storm, T., & Vinju, J. (2020). Automated Validation of State-Based Client-Centric Isolation with TLA+. In Proceedings SEFM 2020 (pp. 43–57). doi:10.1007/978-3-030-67220-1_4 |
|
