Static Application-Level Race Detection in STM Haskell using Contracts

Romain Demeyer, Wim Vanhoof

Résultats de recherche: Contribution dans un livre/un catalogue/un rapport/dans les actes d'une conférenceArticle dans les actes d'une conférence/un colloque

21 Téléchargements (Pure)

Résumé

Writing concurrent programs is a hard task, even when using high-level synchronization primitives such as transactional memories together with a functional language with well-controlled side-effects such as Haskell, because the interferences generated by the processes to each other can occur at different levels and in a very subtle way. The problem occurs when a thread leaves or exposes the shared data in an inconsistent state with respect to the application logic or the real meaning of the data. In this paper, we propose to associate contracts to transactions and we define a program transformation that makes it possible to extend static contract checking in the context of STM Haskell. As a result, we are able to check statically that each transaction of a STM Haskell program handles the shared data in a such way that a given consistency property, expressed in the form of a user-defined boolean function, is preserved. This ensures that bad interference will not occur during the execution of the concurrent program.
langue originaleAnglais
titreElectronic Proceedings in Theoretical Computer Science EPTCS
EditeurOpen Publishing Association
Les DOIs
Etat de la publicationPublié - 10 déc. 2013
Evénement5th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES 2013) - Roma, Italie
Durée: 23 mars 2012 → …

Série de publications

NomEPTCS
EditeurOpen Publishing Association

Colloque

Colloque5th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES 2013)
Pays/TerritoireItalie
La villeRoma
période23/03/12 → …

Empreinte digitale

Examiner les sujets de recherche de « Static Application-Level Race Detection in STM Haskell using Contracts ». Ensemble, ils forment une empreinte digitale unique.

Contient cette citation