Imperial College London
Alternate

ProfessorPhilippaGardner

Faculty of Engineering, Department of Computing

Professor of Theoretical Computer Science
 
 
 
//

Contact

 

+44 (0)20 7594 8292p.gardner Website

 
 
//

Location

 

453Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@inproceedings{da:2014:10.1007/978-3-662-44202-9_9,
author = {da, Rocha Pinto P and Gardner, P and Dinsdale-Young, T},
doi = {10.1007/978-3-662-44202-9_9},
pages = {207--231},
publisher = {Springer},
title = {TaDA: A Logic for Time and Data Abstraction},
url = {http://dx.doi.org/10.1007/978-3-662-44202-9_9},
year = {2014}
}
Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - 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.
AU  - da,Rocha Pinto P
AU  - Gardner,P
AU  - Dinsdale-Young,T
DO  - 10.1007/978-3-662-44202-9_9
EP  - 231
PB  - Springer
PY  - 2014///
SN  - 0302-9743
SP  - 207
TI  - TaDA: A Logic for Time and Data Abstraction
UR  - http://dx.doi.org/10.1007/978-3-662-44202-9_9
UR  - http://hdl.handle.net/10044/1/23810
ER  -
Download