On the semantics of snapshot isolation

File Description SizeFormat 
SI-VMCAI-2019.pdfAccepted version958.35 kBAdobe PDFView/Open
Title: On the semantics of snapshot isolation
Authors: Raad, A
Lahav, O
Vafeiadis, V
Item Type: Conference Paper
Abstract: 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.
Editors: Enea, C
Piskac, R
Issue Date: 11-Jan-2019
Date of Acceptance: 1-Jan-2019
URI: http://hdl.handle.net/10044/1/96916
DOI: 10.1007/978-3-030-11245-5_1
ISBN: 978-3-030-11244-8
ISSN: 0302-9743
Publisher: Springer
Start Page: 1
End Page: 23
Journal / Book Title: Lecture Notes in Computer Science
Volume: 11388
Copyright Statement: © 2019 Springer Nature Switzerland AG. The final publication is available at Springer via https://link.springer.com/chapter/10.1007/978-3-030-11245-5_1
Conference Name: 20th International Conference, VMCAI
Keywords: Artificial Intelligence & Image Processing
Publication Status: Published
Start Date: 2019-01-13
Finish Date: 2019-01-15
Conference Place: Cascais, Portugal
Online Publication Date: 2019-01-11
Appears in Collections:Computing