Tags:complexity and resource bound analysis, lock-free data structures and rely-guarantee reasoning
Abstract:
We present a thread-modular proof method for complexity and resource bound analysis of concurrent, shared-memory programs, lifting Jones' rely-guarantee reasoning to assumptions and commitments capable of expressing bounds. We automate reasoning in this logic by reducing bound analysis of concurrent programs to the sequential case. Our work is motivated by its application to lock-free data structures, fine-grained concurrent algorithms whose time complexity has to our knowledge not been inferred automatically before.
Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms