Parameterised linearizability

Conference item

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

Authors: Yang, H; Cerone, A; Gotsman, A

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Springer
• Host title: Automata, Languages, and Programming: 41st International Colloquium, ICALP 2014, Copenhagen, Denmark, July 8-11, 2014, Proceedings, Part II
• Volume: Lecture Notes in Computer Science: 8573
• Pages: 98-109
• Publication date: 2014-01-01
• DOI: 10.1007/978-3-662-43951-7_9
• ISSN: 0302-9743
• ISBN: 9783662439517
• Keywords: Discrete Mathematics in Computer Science; Information Systems Applications (incl. Internet); Computer Communication Networks; Computation by Abstract Devices; Information Storage and Retrieval; Algorithm Analysis and Problem Complexity