Java monitors as implemented in the java.util.concurrent.locks package provide no-priority nonblocking monitors. That is, threads signalled after blocking on a condition queue do not proceed immediately, but they have to wait until both the signalling thread and also other threads that might have requested the lock release it. This can be a source of errors (if threads that get in the middle leave the monitor in a state incompatible with the signalled thread re-entry) or inefficiency (if repeated evaluation of preconditions is used to ensure safe re-entry). A concise implementation of priority nonblocking monitors in Java is presented. Curiously, our monitors are implemented on top of the standard no-priority implementation. In order to verify the correctness of our solution, a formal transition model (that includes a formalisation of Java locks and conditions) has been defined and checked using Uppaal. This formal model can be reused for model checking concurrent Java programs which make use of the standard locks library (without reentrancy). The talk will also present ongoing work on a full correctness proof using deductive methods.

This is joint work with Angel Herranz.

As the speaker is aware that the topic might be too specific, a little abstruse, that there might possibly be some overexposure to concurrency in recent presentations and that the original spirit of the theory lunch is hardly recognizable for some time now, an alternate 15 min. crash course on termination, abstract interpretation and process calculi could replace the talk above.