TaDA: A Logic for Time and Data Abstraction
File(s)tada-a-logic-for-time-and-data-abstraction.pdf (435.21 KB)
Accepted version
Author(s)
da Rocha Pinto, P
Gardner, P
Dinsdale-Young, T
Type
Conference Paper
Abstract
To avoid data races, concurrent operations should either be at distinct times or on distinct data. Atomicity is the abstraction that an operation takes effect at a single, discrete instant in time, with linearisability being a well-known correctness condition which asserts that concurrent operations appear to behave atomically. Disjointness is the abstraction that operations act on distinct data resource, with concurrent separation logics enabling reasoning about threads that appear to operate independently on disjoint resources. We present TaDA, a program logic that combines the benefits of abstract atomicity and abstract disjointness. Our key contribution is the introduction of atomic triples, which offer an expressive approach to specifying program modules. By building up examples, we show that TaDA supports elegant modular reasoning in a way that was not previously possible.
Date Issued
2014
Date Acceptance
2014-07-28
Citation
ECOOP 2014 – Object-Oriented Programming, 2014, pp.207-231
ISBN
978-3-662-44201-2
ISSN
0302-9743
Publisher
Springer
Start Page
207
End Page
231
Journal / Book Title
ECOOP 2014 – Object-Oriented Programming
Copyright Statement
© 2014, Springer-Verlag Berlin Heidelberg. The final publication is available at Springer via https://dx.doi.org/10.1007/978-3-662-44202-9_9
Source
European Conference on Object-Oriented Programming, ECOOP 2014
Start Date
2014-07-28
Finish Date
2014-08-01
Coverage Spatial
Uppsala, Sweden