Liveness−preserving Atomicity Abstraction
Modern concurrent algorithms are usually encapsulated in libraries, and complex algorithms are often constructed using libraries of simpler ones. We present the first theorem that allows harnessing this structure to give compositional liveness proofs to concurrent algorithms and their clients. We sh...
| Main Authors: | , |
|---|---|
| Format: | Conference item |
| Published: |
Springer−Verlag
2011
|
| _version_ | 1797098746045005824 |
|---|---|
| author | Gotsman, A Yang, H |
| author_facet | Gotsman, A Yang, H |
| author_sort | Gotsman, A |
| collection | OXFORD |
| description | Modern concurrent algorithms are usually encapsulated in libraries, and complex algorithms are often constructed using libraries of simpler ones. We present the first theorem that allows harnessing this structure to give compositional liveness proofs to concurrent algorithms and their clients. We show that, while proving a liveness property of a client using a concurrent library, we can soundly replace the library by another one related to the original library by a generalisation of a well-known notion of linearizability. We apply this result to show formally that lock-freedom, an often-used liveness property of non-blocking algorithms, is compositional for linearizable libraries, and provide an example illustrating our proof technique. |
| first_indexed | 2024-03-07T05:14:02Z |
| format | Conference item |
| id | oxford-uuid:dc892876-859e-434c-8bb6-6f0495e00b94 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T05:14:02Z |
| publishDate | 2011 |
| publisher | Springer−Verlag |
| record_format | dspace |
| spelling | oxford-uuid:dc892876-859e-434c-8bb6-6f0495e00b942022-03-27T09:18:33ZLiveness−preserving Atomicity AbstractionConference itemhttp://purl.org/coar/resource_type/c_5794uuid:dc892876-859e-434c-8bb6-6f0495e00b94Department of Computer ScienceSpringer−Verlag2011Gotsman, AYang, HModern concurrent algorithms are usually encapsulated in libraries, and complex algorithms are often constructed using libraries of simpler ones. We present the first theorem that allows harnessing this structure to give compositional liveness proofs to concurrent algorithms and their clients. We show that, while proving a liveness property of a client using a concurrent library, we can soundly replace the library by another one related to the original library by a generalisation of a well-known notion of linearizability. We apply this result to show formally that lock-freedom, an often-used liveness property of non-blocking algorithms, is compositional for linearizable libraries, and provide an example illustrating our proof technique. |
| spellingShingle | Gotsman, A Yang, H Liveness−preserving Atomicity Abstraction |
| title | Liveness−preserving Atomicity Abstraction |
| title_full | Liveness−preserving Atomicity Abstraction |
| title_fullStr | Liveness−preserving Atomicity Abstraction |
| title_full_unstemmed | Liveness−preserving Atomicity Abstraction |
| title_short | Liveness−preserving Atomicity Abstraction |
| title_sort | liveness preserving atomicity abstraction |
| work_keys_str_mv | AT gotsmana livenesspreservingatomicityabstraction AT yangh livenesspreservingatomicityabstraction |