Analysing and Optimising Parallel Snapshot Isolation

Large-scale Internet services often rely on distributed databases that provide consistency models for transactions weaker than serialisability.  Unfortunately, we currently lack a systematic understanding of when programmers can use such models without violating correctness.  And when an application is correct on a given consistency model, we do not know whether the model can safely be weakened even further to improve performance.

I will present work in progress to address these issues.  In the talk I will concentrate on a promising consistency model of Parallel Snapshot Isolation (PSI), which weakens the classical snapshot isolation in a way that allows more efficient distributed implementations.  I will present a formalisation of PSI, a criterion for ensuring correctness of applications using it, and a way of optimising the applications to improving performance.

This is joint work with Andrea Cerone (IMDEA), Giovanni Bernardi (IMDEA) and Hongseok Yang (Oxford).

Speaker biography

Alexey Gotsman is a tenure-track Assistant Research Professor at the IMDEA Software Institute.  Before joining IMDEA, he was a postdoctoral fellow at the University of Cambridge, where he also completed his PhD.  His research interests are in software verification, particularly in developing reasoning techniques and automated verification tools for real-world concurrent systems software.