Model checking linearizability via refinement

• Main Authors: LIU, Yang, CHEN, Wei, LIU, Yanhong A., SUN, Jun
• Format: text
• Language: English
• Published: Institutional Knowledge at Singapore Management University 2009
• Subjects: Model Check; Shared Variable; Linear Temporal Logic; Label Transition System; Linearization Action; Programming Languages and Compilers; Software Engineering
• Online Access: https://ink.library.smu.edu.sg/sis_research/5040; https://ink.library.smu.edu.sg/context/sis_research/article/6043/viewcontent/linear.pdf
• Institution: Singapore Management University

Linearizability is an important correctness criterion for implementations of concurrent objects. Automatic checking of linearizability is challenging because it requires checking that 1) all executions of concurrent operations be serializable, and 2) the serialized executions be correct with respect...