Static Application-Level Race Detection in STM Haskell using Contracts

Research output: Contribution to journalArticle

11 Downloads (Pure)

Abstract

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.
Original languageEnglish
JournalEPTCS
DOIs
Publication statusPublished - 10 Dec 2013

Fingerprint

Boolean functions
Synchronization
Data storage equipment

Keywords

  • cs.LO
  • cs.DC
  • cs.PL

Cite this

@article{71ea35f0ed634b01a76db3fa76aefcf4,
title = "Static Application-Level Race Detection in STM Haskell using Contracts",
abstract = "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.",
keywords = "cs.LO, cs.DC, cs.PL",
author = "Romain Demeyer and Wim Vanhoof",
note = "In Proceedings PLACES 2013, arXiv:1312.2218. rde@info.fundp.ac.be; wim.vanhoof@unamur.be",
year = "2013",
month = "12",
day = "10",
doi = "10.4204/EPTCS.137.10",
language = "English",
journal = "EPTCS",
issn = "2075-2180",
publisher = "Open Publishing Association",

}

Static Application-Level Race Detection in STM Haskell using Contracts. / Demeyer, Romain; Vanhoof, Wim.

In: EPTCS, 10.12.2013.

Research output: Contribution to journalArticle

TY - JOUR

T1 - Static Application-Level Race Detection in STM Haskell using Contracts

AU - Demeyer, Romain

AU - Vanhoof, Wim

N1 - In Proceedings PLACES 2013, arXiv:1312.2218. rde@info.fundp.ac.be; wim.vanhoof@unamur.be

PY - 2013/12/10

Y1 - 2013/12/10

N2 - 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.

AB - 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.

KW - cs.LO

KW - cs.DC

KW - cs.PL

U2 - 10.4204/EPTCS.137.10

DO - 10.4204/EPTCS.137.10

M3 - Article

JO - EPTCS

JF - EPTCS

SN - 2075-2180

ER -