TaDA: A logic for time and data abstraction (extended version)
File(s)DTR14-7.pdf (608.76 KB)
Published version
Author(s)
da Rocha Pinto, P
Dinsdale-Young, T
Gardner, P
Type
Report
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-01-01
Citation
Departmental Technical Report: 14/7, 2014, pp.1-46
Publisher
Department of Computing, Imperial College London
Start Page
1
End Page
46
Journal / Book Title
Departmental Technical Report: 14/7
Copyright Statement
© 2014 The Author(s). This report is available open access under a CC-BY-NC-ND (https://creativecommons.org/licenses/by-nc-nd/4.0/)
Publication Status
Published
Article Number
14/7