Litmus: Running Tests against Hardware

Jade Alglave, Luc Maranget, Susmit Sarkar, Peter Sewell

Research output: Chapter in Book/Report/Conference proceedingConference contribution

66 Citations (Scopus)

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 languageEnglish
Title of host publicationTOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS
EditorsPA Abdulla, KRM Leino
Place of PublicationBERLIN
PublisherSpringer-Verlag
Pages41-44
Number of pages4
ISBN (Print)978-3-642-19834-2
Publication statusPublished - 2011
Event17th International Conference of Tools and Algorithms for the Construction and Analysis of Systems - Saarbrucken, Germany
Duration: 26 Mar 20113 Apr 2011

Publication series

NameLecture Notes in Computer Science
PublisherSPRINGER-VERLAG BERLIN
Volume6605
ISSN (Print)0302-9743

Conference

Conference17th International Conference of Tools and Algorithms for the Construction and Analysis of Systems
Country/TerritoryGermany
CitySaarbrucken
Period26/03/113/04/11

Fingerprint

Dive into the research topics of 'Litmus: Running Tests against Hardware'. Together they form a unique fingerprint.

Cite this