Paper Info
Title
Characterizing progress properties of concurrent objects via contextual refinements
Abstract
Implementations of concurrent objects should guarantee linearizability and a progress property such as wait-freedom, lock-freedom, obstruction-freedom, starvation-freedom, or deadlock-freedom. Conventional informal or semi-formal definitions of these progress properties describe conditions under which a method call is guaranteed to complete, but it is unclear how these definitions can be utilized to formally verify system software in a layered and modular way. In this paper, we propose a unified framework based on contextual refinements to show exactly how progress properties affect the behaviors of client programs. We give formal operational definitions of all common progress properties and prove that for linearizable objects, each progress property is equivalent to a specific type of contextual refinement that preserves termination. The equivalence ensures that verification of such a contextual refinement for a concurrent object guarantees both linearizability and the corresponding progress property. Contextual refinement also enables us to verify safety and liveness properties of client programs at a high abstraction level by soundly replacing concrete method implementations with abstract atomic operations.
Year
DOI
Venue
2013
10.1007/978-3-642-40184-8_17
CONCUR
Keywords
Field
DocType
concurrent object,client program,contextual refinement,common progress property,progress property,corresponding progress property,method call,concrete method implementation,liveness property,characterizing progress property,abstract atomic operation
Linearizability,System software,Computer science,Theoretical computer science,Implementation,Equivalence (measure theory),Modular design,Abstraction layer,Operational definition,Liveness
Conference
Citations 
PageRank 
References 
10
0.53
17
Authors
4
Name
Order
Citations
PageRank
Hongjin Liang1875.88
Jan Hoffmann2100.53
Xinyu Feng344330.52
Zhong Shao489768.80