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:2016:10.1007/978-3-662-49498-1_8,
author = {da, Rocha Pinto P and Dinsdale-Young, T and Gardner, PA and Sutherland, J and da, Rocha Pinto P and Dinsdale-Young, T and Gardner, P and Sutherland, J},
doi = {10.1007/978-3-662-49498-1_8},
pages = {176--201},
publisher = {Springer Berlin Heidelberg},
title = {Modular Termination Verification for Non-blocking Concurrency},
url = {http://dx.doi.org/10.1007/978-3-662-49498-1_8},
year = {2016}
}
Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - We present Total-TaDA, a program logic for verifying the total correctness of concurrent programs: that such programs both terminate and produce the correct result. With Total-TaDA, we can specify constraints on a thread’s concurrent environment that are necessary to guarantee termination. This allows us to verify total correctness for non-blocking algorithms, e.g. a counter and a stack. Our specifications can express lock- and wait-freedom. More generally, they can express that one operation cannot impede the progress of another, a new non-blocking property we call non-impedance. Moreover, our approach is modular. We can verify the operations of a module independently, and build up modules on top of each other.
AU  - da,Rocha Pinto P
AU  - Dinsdale-Young,T
AU  - Gardner,PA
AU  - Sutherland,J
AU  - da,Rocha Pinto P
AU  - Dinsdale-Young,T
AU  - Gardner,P
AU  - Sutherland,J
DO  - 10.1007/978-3-662-49498-1_8
EP  - 201
PB  - Springer Berlin Heidelberg
PY  - 2016///
SN  - 0302-9743
SP  - 176
TI  - Modular Termination Verification for Non-blocking Concurrency
UR  - http://dx.doi.org/10.1007/978-3-662-49498-1_8
UR  - http://hdl.handle.net/10044/1/31740
ER  -
Download