Reasoning about Java's reentrant locks

Abstract : This paper presents a verification technique for a concurrent Java-like language with reentrant locks. The verification technique is based on permission-accounting separation logic. As usual, each lock is associated with a resource invariant, when acquiring the lock the resources are obtained by the thread holding the lock, and when releasing the lock, the resources are released. To accommodate for reentrancy, the notion of lockset is introduced: a multiset of locks held by a thread. Keeping track of the lockset enables the logic to ensure that resources are not re-acquired upon reentrancy, thus avoiding the introduction of new resources in the system. To be able to express flexible locking policies, we combine the verification logic with value-parametrized classes. Verified programs satisfy the following properties: data race freedom, absence of null-dereferencing and partial correctness. The verification technique is illustrated on several examples, including a challenging lock-coupling algorithm.
Type de document :
Communication dans un congrès
Springer-Verlag. The Sixth ASIAN Symposium on Programming Languages and Systems (APLAS 2008), Dec 2008, Bangalore, India. 2008, Lecture Notes in Computer Science
Liste complète des métadonnées

Littérature citée [20 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00320115
Contributeur : Clément Hurlin <>
Soumis le : mercredi 10 septembre 2008 - 11:49:35
Dernière modification le : samedi 27 janvier 2018 - 01:30:46
Document(s) archivé(s) le : lundi 8 octobre 2012 - 13:03:07

Fichiers

aplas.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00320115, version 1

Collections

Citation

Christian Haack, Marieke Huisman, Clément Hurlin. Reasoning about Java's reentrant locks. Springer-Verlag. The Sixth ASIAN Symposium on Programming Languages and Systems (APLAS 2008), Dec 2008, Bangalore, India. 2008, Lecture Notes in Computer Science. 〈inria-00320115〉

Partager

Métriques

Consultations de la notice

151

Téléchargements de fichiers

216