We propose an approach for the modular specification and verification of total correctness properties of object-oriented programs. The core of our approach is a specification style that prescribes a way to assign a level expression to each method such that each callee’s level is below the caller’s, even in the presence of dynamic binding. The specification style yields specifications that properly hide implementation details. The main idea is to use multisets of method names as levels, and to associate with each object levels that abstractly reflect the way the object is built from other objects. A method’s level is then defined in terms of the method’s own name and the levels associated with the objects passed as arguments. We first present the specification style in the context of programs that do not modify object fields. We then combine it with separation logic and abstract predicate families to obtain an approach for programs with heap mutation. In a third step, we address concurrency, by incorporating an existing approach for verifying deadlock freedom of channels and locks. Our main contribution here is to achieve information hiding by using the proposed termination levels for lock ordering as well. Also, we introduce call permissions to enable elegant verification of termination of programs where threads cause work in other threads, such as in thread pools or fine-grained concurrent algorithms involving compare-and-swap loops. We explain how our approach can be used also to verify the liveness of nonterminating programs.

@article{paperbot318,
  title = {Modular Termination Verification of Single-Threaded and Multithreaded Programs},
  author = {Bart Jacobs and Dragan Bosnacki and Ruurd Kuiper},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = {40},
  number = {3},
  year = {2018},
  doi = {10.1145/3210258}
}