Reasoning about Asynchronous Method Calls and Inheritance

Abstract

This paper considers the problem of reusing synchronization constraints for concurrent objects with asynchronous method calls. Our approach extends the Creol language with a specialized composition operator expressing synchronized merge. The use of synchronized merge allows synchronization classes to be added and combined with general purpose classes by means of multiple inheritance. The paper presents proof rules for synchronized merge and several examples.