| ||||
| ||||
![]() Title:Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms Conference:FMCAD 2018 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 ![]() Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms | ||||
Copyright © 2002 – 2025 EasyChair |