Reasoning about Asynchronous Method Calls and Inheritance


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.

In Proc. Norsk Informatikkonferanse (NIK 2004), Tapir 2004.