|Time+Place:||Tuesday 28/07/2015 14:30 Room 601 Taub Bld.|
|Title:||'Cause I'm Strong Enough: Reasoning about Consistency Choices in Distributed Systems|
|Speaker:|| Prof. Alexey Gotsman - SPECIAL LECTURE - Note unusual location
|| Affiliation: || IMDEA Software Institute, Madrid
|| Host: || Hagit Attiya
Large-scale distributed systems often rely on replicated databases that allow a programmer to request different data consistency guarantees for different operations, and thereby control their performance. Using such databases is far from trivial: requesting stronger consistency in too many places may hurt performance, and requesting it in too few places may violate correctness. To help programmers in this task, we propose the first proof rule for establishing that a particular choice of consistency guarantees for various operations on a replicated database is enough to ensure the preservation of a given data integrity invariant. Our rule is modular: it allows reasoning about the behaviour of every operation separately under some assumption on the behaviour of other operations. This leads to simple reasoning, which we have automated in an SMT-based tool. Short Bio: Alexey Gotsman is an Assistant Research Professor at the IMDEA Software Institute in Madrid, Spain. His research interests are in programming models and verification techniques for concurrent and distributed software.