Litmus: Running Tests against Hardware
Résumé
Shared memory multiprocessors typically expose subtle, poorly understood and poorly specied relaxed-memory semantics to programmers. To understand them, and to develop formal models to use in program verication, we nd 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 nd interesting behaviour. It embodies various techniques for making such interesting behaviour appear more frequently