Parameterised linearizability
Many concurrent libraries are parameterised, meaning that they imple- ment generic algorithms that take another library as a parameter. In such cases, the standard way of stating the correctness of concurrent libraries via linearisab- ility is inapplicable. We generalise linearisability to parameter...
| Main Authors: | , , |
|---|---|
| 格式: | Conference item |
| 出版: |
Springer
2014
|
| _version_ | 1826303141531877376 |
|---|---|
| author | Yang, H Cerone, A Gotsman, A |
| author_facet | Yang, H Cerone, A Gotsman, A |
| author_sort | Yang, H |
| collection | OXFORD |
| description | Many concurrent libraries are parameterised, meaning that they imple- ment generic algorithms that take another library as a parameter. In such cases, the standard way of stating the correctness of concurrent libraries via linearisab- ility is inapplicable. We generalise linearisability to parameterised libraries and investigate subtle trade-offs between the assumptions that such libraries can make about their environment and the conditions that linearisability has to impose on different types of interactions with it. We prove that the resulting parameterised linearisability is closed under instantiating parameter libraries and composing several non-interacting libraries, and furthermore implies observational refine- ment. These results allow modularising the reasoning about concurrent programs using parameterised libraries and confirm the appropriateness of the proposed definitions. We illustrate the applicability of our results by proving the correct- ness of a parameterised library implementing flat combining |
| first_indexed | 2024-03-07T05:58:08Z |
| format | Conference item |
| id | oxford-uuid:eb3be0ec-b48f-4c2e-b97b-b1dc3c20fbdb |
| institution | University of Oxford |
| last_indexed | 2024-03-07T05:58:08Z |
| publishDate | 2014 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:eb3be0ec-b48f-4c2e-b97b-b1dc3c20fbdb2022-03-27T11:08:07ZParameterised linearizabilityConference itemhttp://purl.org/coar/resource_type/c_5794uuid:eb3be0ec-b48f-4c2e-b97b-b1dc3c20fbdbSymplectic Elements at OxfordSpringer2014Yang, HCerone, AGotsman, AMany concurrent libraries are parameterised, meaning that they imple- ment generic algorithms that take another library as a parameter. In such cases, the standard way of stating the correctness of concurrent libraries via linearisab- ility is inapplicable. We generalise linearisability to parameterised libraries and investigate subtle trade-offs between the assumptions that such libraries can make about their environment and the conditions that linearisability has to impose on different types of interactions with it. We prove that the resulting parameterised linearisability is closed under instantiating parameter libraries and composing several non-interacting libraries, and furthermore implies observational refine- ment. These results allow modularising the reasoning about concurrent programs using parameterised libraries and confirm the appropriateness of the proposed definitions. We illustrate the applicability of our results by proving the correct- ness of a parameterised library implementing flat combining |
| spellingShingle | Yang, H Cerone, A Gotsman, A Parameterised linearizability |
| title | Parameterised linearizability |
| title_full | Parameterised linearizability |
| title_fullStr | Parameterised linearizability |
| title_full_unstemmed | Parameterised linearizability |
| title_short | Parameterised linearizability |
| title_sort | parameterised linearizability |
| work_keys_str_mv | AT yangh parameterisedlinearizability AT ceronea parameterisedlinearizability AT gotsmana parameterisedlinearizability |