Permission Specifications for Common Multithreaded Programming Patterns

Marieke Huisman 1 Clément Hurlin 1
1 EVEREST - Environments for Verification and Security of Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : Multithreading is the next challenge for program verification. To support modular verification of multithreaded programs, one should know when data might be accessed or updated by the different threads in the system. We propose a permission-based annotation system that is designed to do exactly this, i.e. it specifies when a thread can read or write a variable. The annotation system ensures that threads have exclusive access to a variable whenever they have the possibility to write it, thus avoiding data races. Moreover, the annotation system allows to change permissions dynamically throughout the execution. The information from the permission annotations can be used for further verification of the program. This paper shows how the annotation system can be used to specify variable access in several typical multithreaded programming patterns.
Type de document :
Communication dans un congrès
Book in the honor of Henk Barendregt for his 60th birthday, Dec 2007, Nimègue, Netherlands. 2007
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00204771
Contributeur : Clément Hurlin <>
Soumis le : mardi 15 janvier 2008 - 15:11:48
Dernière modification le : samedi 27 janvier 2018 - 01:30:52
Document(s) archivé(s) le : mardi 13 avril 2010 - 17:43:19

Fichiers

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

Identifiants

  • HAL Id : inria-00204771, version 1

Collections

Citation

Marieke Huisman, Clément Hurlin. Permission Specifications for Common Multithreaded Programming Patterns. Book in the honor of Henk Barendregt for his 60th birthday, Dec 2007, Nimègue, Netherlands. 2007. 〈inria-00204771〉

Partager

Métriques

Consultations de la notice

97

Téléchargements de fichiers

82