Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [9 references]  Display  Hide  Download
Contributor : Clément Hurlin Connect in order to contact the contributor
Submitted on : Tuesday, January 15, 2008 - 3:11:48 PM
Last modification on : Friday, February 4, 2022 - 3:17:56 AM
Long-term archiving on: : Tuesday, April 13, 2010 - 5:43:19 PM


Files produced by the author(s)


  • HAL Id : inria-00204771, version 1



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. ⟨inria-00204771⟩



Record views


Files downloads