Consistent Local-First Software: Enforcing Safety and Invariants for Local-First Applications
Local-first software embraces data replication as a means to achieve scalability and offline availability. A crucial ingredient of local-first software are mergeable data types, like conflict-free replicated data types (CRDTs), which feature eventual consistency by enabling processes to access data locally and later merge it with other replicas in an asynchronous manner. Notably, the merging process needs to adhere to application constraints for correctness. Ensuring such application-level invariants poses a challenge, as developers must reason about the replicated program state and resort to manual synchronization of specific application components to enforce the invariant. This paper introduces ConLoc (Consistent Local-First Software), a novel system designed to automatically enforce safety and maintain invariants in local-first applications. ConLoc effectively addresses the issue of preserving invariants in the execution of programs with replicated data types, including CRDTs. Our approach is able to verify the correctness of many CRDTs examined in the literature and in implementations, such the ones used in the Riak database. ConLoc ensures that applications are automatically synchronized correctly, resulting in substantial latency and throughput improvements when compared to sequential execution, while upholding the same set of invariants.
Tue 24 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:30 | Verification and ValidationDemonstrations / Ideas, Visions and Reflections / Research Papers / Journal First at Cosmos 3A Chair(s): Alex Orso Georgia Institute of Technology | ||
10:30 10mTalk | TraceMOP: An Explicit-Trace Runtime Verification Tool for Java Demonstrations | ||
10:40 10mTalk | VO-GCSE: Verification Optimization through Global Common Subexpression Elimination Demonstrations Rafael Menezes University of Manchester, Norbert Tihanyi Technology Innovation Institute, Ridhi Jain Technology Innovation Institute (TII), Abu Dhabi, UAE, Alexander Levin Nvidia, Rosiane de Freitas Federal University of Amazonas, Lucas C. Cordeiro University of Manchester, UK and Federal University of Amazonas, Brazil | ||
10:50 10mTalk | GIVUP: Automated Generation and Verification of Textual Process Descriptions Demonstrations Quentin Nivon University Grenoble Alpes, Gwen Salaün University of Grenoble Alpes, Frederic Lang Univ. Grenoble Alpes, Inria, CNRS, Grenoble INP, LIG, Grenoble, France | ||
11:00 10mTalk | NeuroStrata: Harnessing Neuro-Symbolic Paradigms for Improved Testability and Verifiability of Autonomous CPS Ideas, Visions and Reflections Xi Zheng Macquarie University, Ziyang Li University of Pennsylvania, Ivan Ruchkin University of Florida, Ruzica Piskac Yale University, Miroslav Pajic Duke University | ||
11:10 20mTalk | Scene Flow Specifications: Encoding and Monitoring Rich Temporal Safety Properties of Autonomous Systems Research Papers Trey Woodlief University of Virginia, United States, Felipe Toledo , Matthew B Dwyer University of Virginia, Sebastian Elbaum University of Virginia DOI | ||
11:30 20mTalk | QSF: Multi-Objective Optimization based Efficient Solving for Floating-Point Constraints Research Papers Xu Yang College of Computer Science and Technology, National University of Defense Technology, Zhenbang Chen College of Computer, National University of Defense Technology, Wei Dong National University of Defense Technology, Ji Wang National University of Defense Technology DOI | ||
11:50 20mTalk | Consistent Local-First Software: Enforcing Safety and Invariants for Local-First Applications Journal First Mirko Köhler TU Darmstadt, George Zakhour University of St. Gallen, Pascal Weisenburger University of St. Gallen, Guido Salvaneschi University of St. Gallen | ||
12:10 20mTalk | ChangeGuard: Validating Code Changes via Pairwise Learning-Guided Execution Research Papers Lars Gröninger University of Stuttgart, Beatriz Souza Universität Stuttgart, Michael Pradel University of Stuttgart DOI | ||
Cosmos 3A is the first room in the Cosmos 3 wing.
When facing the main Cosmos Hall, access to the Cosmos 3 wing is on the left, close to the stairs. The area is accessed through a large door with the number “3”, which will stay open during the event.