Litmus: running tests against hardware

Jade Alglave; Luc Maranget; Susmit Sarkar; Peter Sewell

doi:10.1007/978-3-642-19835-9_5

Litmus: running tests against hardware

Jade Alglave, Luc Maranget, Susmit Sarkar, Peter Sewell

School of Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

Shared memory multiprocessors typically expose subtle, poorly understood and poorly specified relaxed-memory semantics to programmers. To understand them, and to develop formal models to use in program verification, we find it essential to take an empirical approach, testing what results parallel programs can actually produce when executed on the hardware. We describe a key ingredient of our approach, our litmus tool, which takes small 'litmus test' programs and runs them for many iterations to find interesting behaviour. It embodies various techniques for making such interesting behaviour appear more frequently.

Original language	English
Title of host publication	Tools and algorithms for the construction and analysis of systems
Subtitle of host publication	17th International Conference, TACAS 2011, held as part of the Joint European Conference on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26 - April3, 2011, Proceedings
Editors	Parosh Aziz Abdulla, K. Rustan M. Leino
Place of Publication	Heidelberg
Publisher	Springer-Verlag
Pages	41-44
Number of pages	4
ISBN (Electronic)	9783642198359
ISBN (Print)	9783642198342
DOIs	https://doi.org/10.1007/978-3-642-19835-9_5
Publication status	Published - 18 Mar 2011
Event	17th International Conference of Tools and Algorithms for the Construction and Analysis of Systems - Saarbrucken, Germany Duration: 26 Mar 2011 → 3 Apr 2011

Publication series

Name	Lecture notes in computer science
Volume	6605
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	17th International Conference of Tools and Algorithms for the Construction and Analysis of Systems
Country/Territory	Germany
City	Saarbrucken
Period	26/03/11 → 3/04/11

Access to Document

10.1007/978-3-642-19835-9_5

Cite this

Alglave, J., Maranget, L., Sarkar, S., & Sewell, P. (2011). Litmus: running tests against hardware. In P. A. Abdulla, & K. R. M. Leino (Eds.), Tools and algorithms for the construction and analysis of systems: 17th International Conference, TACAS 2011, held as part of the Joint European Conference on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26 - April3, 2011, Proceedings (pp. 41-44). (Lecture notes in computer science; Vol. 6605). Springer-Verlag. https://doi.org/10.1007/978-3-642-19835-9_5

Alglave, Jade ; Maranget, Luc ; Sarkar, Susmit et al. / Litmus : running tests against hardware. Tools and algorithms for the construction and analysis of systems: 17th International Conference, TACAS 2011, held as part of the Joint European Conference on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26 - April3, 2011, Proceedings . editor / Parosh Aziz Abdulla ; K. Rustan M. Leino. Heidelberg : Springer-Verlag, 2011. pp. 41-44 (Lecture notes in computer science).

@inproceedings{8ee6cf4f85a148f4a353fa66eedfafd9,

title = "Litmus: running tests against hardware",

abstract = "Shared memory multiprocessors typically expose subtle, poorly understood and poorly specified relaxed-memory semantics to programmers. To understand them, and to develop formal models to use in program verification, we find it essential to take an empirical approach, testing what results parallel programs can actually produce when executed on the hardware. We describe a key ingredient of our approach, our litmus tool, which takes small 'litmus test' programs and runs them for many iterations to find interesting behaviour. It embodies various techniques for making such interesting behaviour appear more frequently.",

author = "Jade Alglave and Luc Maranget and Susmit Sarkar and Peter Sewell",

note = "Funding: The authors acknowledge funding from EPSRC grants EP/F036345, EP/H005633, and EP/H027351, from ANR project parsec (ANR-06-SETIN-010), and from INRIA associated team MM.; 17th International Conference of Tools and Algorithms for the Construction and Analysis of Systems ; Conference date: 26-03-2011 Through 03-04-2011",

year = "2011",

month = mar,

day = "18",

doi = "10.1007/978-3-642-19835-9_5",

language = "English",

isbn = "9783642198342",

series = "Lecture notes in computer science",

publisher = "Springer-Verlag",

pages = "41--44",

editor = "Abdulla, {Parosh Aziz} and Leino, {K. Rustan M.}",

booktitle = "Tools and algorithms for the construction and analysis of systems",

address = "Germany",

}

Alglave, J, Maranget, L, Sarkar, S & Sewell, P 2011, Litmus: running tests against hardware. in PA Abdulla & KRM Leino (eds), Tools and algorithms for the construction and analysis of systems: 17th International Conference, TACAS 2011, held as part of the Joint European Conference on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26 - April3, 2011, Proceedings . Lecture notes in computer science, vol. 6605, Springer-Verlag, Heidelberg, pp. 41-44, 17th International Conference of Tools and Algorithms for the Construction and Analysis of Systems, Saarbrucken, Germany, 26/03/11. https://doi.org/10.1007/978-3-642-19835-9_5

Litmus: running tests against hardware. / Alglave, Jade; Maranget, Luc; Sarkar, Susmit et al.
Tools and algorithms for the construction and analysis of systems: 17th International Conference, TACAS 2011, held as part of the Joint European Conference on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26 - April3, 2011, Proceedings . ed. / Parosh Aziz Abdulla; K. Rustan M. Leino. Heidelberg: Springer-Verlag, 2011. p. 41-44 (Lecture notes in computer science; Vol. 6605).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Litmus

T2 - 17th International Conference of Tools and Algorithms for the Construction and Analysis of Systems

AU - Alglave, Jade

AU - Maranget, Luc

AU - Sarkar, Susmit

AU - Sewell, Peter

N1 - Funding: The authors acknowledge funding from EPSRC grants EP/F036345, EP/H005633, and EP/H027351, from ANR project parsec (ANR-06-SETIN-010), and from INRIA associated team MM.

PY - 2011/3/18

Y1 - 2011/3/18

N2 - Shared memory multiprocessors typically expose subtle, poorly understood and poorly specified relaxed-memory semantics to programmers. To understand them, and to develop formal models to use in program verification, we find it essential to take an empirical approach, testing what results parallel programs can actually produce when executed on the hardware. We describe a key ingredient of our approach, our litmus tool, which takes small 'litmus test' programs and runs them for many iterations to find interesting behaviour. It embodies various techniques for making such interesting behaviour appear more frequently.

AB - Shared memory multiprocessors typically expose subtle, poorly understood and poorly specified relaxed-memory semantics to programmers. To understand them, and to develop formal models to use in program verification, we find it essential to take an empirical approach, testing what results parallel programs can actually produce when executed on the hardware. We describe a key ingredient of our approach, our litmus tool, which takes small 'litmus test' programs and runs them for many iterations to find interesting behaviour. It embodies various techniques for making such interesting behaviour appear more frequently.

UR - https://doi.org/10.1007/978-3-642-19835-9

U2 - 10.1007/978-3-642-19835-9_5

DO - 10.1007/978-3-642-19835-9_5

M3 - Conference contribution

SN - 9783642198342

T3 - Lecture notes in computer science

SP - 41

EP - 44

BT - Tools and algorithms for the construction and analysis of systems

A2 - Abdulla, Parosh Aziz

A2 - Leino, K. Rustan M.

PB - Springer-Verlag

CY - Heidelberg

Y2 - 26 March 2011 through 3 April 2011

ER -

Alglave J, Maranget L, Sarkar S, Sewell P. Litmus: running tests against hardware. In Abdulla PA, Leino KRM, editors, Tools and algorithms for the construction and analysis of systems: 17th International Conference, TACAS 2011, held as part of the Joint European Conference on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26 - April3, 2011, Proceedings . Heidelberg: Springer-Verlag. 2011. p. 41-44. (Lecture notes in computer science). Epub 2011 Mar 14. doi: 10.1007/978-3-642-19835-9_5

Litmus: running tests against hardware

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this