Verification of Concurrent Objects with Asynchronous Method Calls

Abstract

Current object-oriented approaches to distributed programs may be criticized in several respects. First, method calls are generally synchronous, which leads to much waiting in distributed and unstable networks. Second, the common model of thread concurrency makes reasoning about program behavior very challenging. A model based on concurrent objects communicating by means of asynchronous method calls has been proposed to combine object orientation and distribution in a more satisfactory way. This paper introduces a reasoning system for this model, focusing on simplicity and modularity. We believe that a simple and compositional proof system is paramount to allow verification of real programs. The proposed proof rules are derived from the Hoare rules of a standard sequential language by means of a semantic encoding preserving soundness and relative completeness.