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

@techreport{da:2014:10.25561/95035,
author = {da, Rocha Pinto P and Dinsdale-Young, T and Gardner, P},
booktitle = {Departmental Technical Report: 14/7},
doi = {10.25561/95035},
publisher = {Department of Computing, Imperial College London},
title = {TaDA: A logic for time and data abstraction (extended version)},
url = {http://dx.doi.org/10.25561/95035},
year = {2014}
}
Download

RIS format (EndNote, RefMan)

TY  - RPRT
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  - Dinsdale-Young,T
AU  - Gardner,P
DO  - 10.25561/95035
PB  - Department of Computing, Imperial College London
PY  - 2014///
TI  - TaDA: A logic for time and data abstraction (extended version)
T1  - Departmental Technical Report: 14/7
UR  - http://dx.doi.org/10.25561/95035
UR  - http://hdl.handle.net/10044/1/95035
ER  -
Download