Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms
Thomas Pani, Georg Weißenbacher, Florian Zuleger · 2018
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.