Re: [isabelle] A few thoughts about Java multithreading model in relation to type-safety

Hi Tambet,

in Isabelle, I have formalized a notion of type safety for the Java multithreading model with deadlocks in the JinjaThreads article in the Archive of Formal Proofs (

There, I do allow deadlocks in showing type safety in the style of progress and preservation: The progress is restricted to non-deadlocked cases. Note that not only deadlocks via locking violate the progress property. Java's wait-notify-mechanism and joining of threads can similarly cause problems with progress. Suppose a thread is in a wait set - waiting to be notified or interrupted - but there is only one other thread which joins on the thread in the wait set. I would also call this a deadlock.


Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Gebäude 50.41, Raum 023
76131 Karlsruhe

Telefon: +49 721 608-8352
Fax: +49 721 608-8457
E-Mail: andreas.lochbihler at
KIT - Universität des Landes Baden-Württemberg und nationales Großforschungszentrum in der Helmholtz-Gemeinschaft

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.