The financial technology sector is undergoing a transformation in moving to open-source and collaborative approaches as it works to address increasing compliance and assurance needs in its software stacks. Programming languages and validation technologies are a foundational part of this change. Based on this viewpoint,…
Production distributed systems are challenging to formally verify, in particular when they are based on distributed protocols that are not rigorously described or fully understood. In this paper, we derive models and properties for two core distributed protocols used in eventually consistent production key-value stores…
Finite-state machines (FSMs) are among the oldest models employed in the formalization and analysis of both software and hardware. Owing to their simplicity, there exist various implementations to support their practical application in mainstream programming languages. Through such software libraries, programmers can explicitly define states,…
To cope with large data sets, distributed data stores partition their data across servers. However, real-world systems usually do not provide useful transactional semantics for operations accessing multiple partitions due to the delays involved in achieving multi-partition consistency. Read Atomic Multi-Partition (RAMP) transactions have recently…
The promise of high scalability and availability has prompted many companies to replace traditional relational database management systems (RDBMS) with NoSQL key-value stores. This comes at the cost of relaxed consistency guarantees: key-value stores only guarantee eventual consistency in principle. In practice, however, many key-value…
Distributed key-value stores are quickly becoming a key component of cloud computing systems. In order to improve read/write latency, distributed key-value stores offer weak notions of consistency to clients by using many complex design decisions. However, it is challenging to formally analyze consistency behaviors of…
Discrete event simulations can be used to analyze natural and artificial phenomena. To this end, one provides models whose behaviors are characterized by discrete events in a discrete timeline. By running such a simulation, one can then observe its properties. This suggests the possibility of…
