Imperial College London
Portrait Picture

DrAzaleaRaad

Faculty of Engineering, Department of Computing

Senior Lecturer
 
 
 
//

Contact

 

+44 (0)20 7594 8271azalea.raad Website

 
 
//

Location

 

426Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@inproceedings{Raad:2019:10.1007/978-3-030-11245-5_1,
author = {Raad, A and Lahav, O and Vafeiadis, V},
doi = {10.1007/978-3-030-11245-5_1},
pages = {1--23},
publisher = {Springer},
title = {On the semantics of snapshot isolation},
url = {http://dx.doi.org/10.1007/978-3-030-11245-5_1},
year = {2019}
}
Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - Snapshot isolation (SI) is a standard transactional consistency model used in databases, distributed systems and software transactional memory (STM). Its semantics is formally defined both declaratively as an acyclicity axiom, and operationally as a concurrent algorithm with memory bearing timestamps.We develop two simpler equivalent operational definitions of SI as lock-based reference implementations that do not use timestamps. Our first locking implementation is prescient in that requires a priori knowledge of the data accessed by a transaction and carries out transactional writes eagerly (in-place). Our second implementation is non-prescient and performs transactional writes lazily by recording them in a local log and propagating them to memory at commit time. Whilst our first implementation is simpler and may be better suited for developing a program logic for SI transactions, our second implementation is more practical due to its non-prescience. We show that both implementations are sound and complete against the declarative SI specification and thus yield equivalent operational definitions for SI.We further consider, for the first time formally, the use of SI in a context with racy non-transactional accesses, as can arise in STM implementations of SI. We introduce robust snapshot isolation (RSI), an adaptation of SI with similar semantics and guarantees in this mixed setting. We present a declarative specification of RSI as an acyclicity axiom and analogously develop two operational models as lock-based reference implementations (one eager, one lazy). We show that these operational models are both sound and complete against the declarative RSI model.
AU  - Raad,A
AU  - Lahav,O
AU  - Vafeiadis,V
DO  - 10.1007/978-3-030-11245-5_1
EP  - 23
PB  - Springer
PY  - 2019///
SN  - 0302-9743
SP  - 1
TI  - On the semantics of snapshot isolation
UR  - http://dx.doi.org/10.1007/978-3-030-11245-5_1
UR  - https://doi.org/10.1007/978-3-030-11245-5
UR  - http://hdl.handle.net/10044/1/96916
ER  -
Download