Verifying local transformations on relaxed memory models

S. Burckhardt, M. Musuvathi, V. Singh, in:, R. Gupta (Ed.), Springer, 2010, pp. 104–123.

Download
No fulltext has been uploaded. References only!

Conference Paper | Published | English
Author
Burckhardt, Sebastian; Musuvathi, Madanlal; Singh, VasuIST Austria
Editor
Gupta, Rajiv
Series Title
LNCS
Abstract
The problem of locally transforming or translating programs without altering their semantics is central to the construction of correct compilers. For concurrent shared-memory programs this task is challenging because (1) concurrent threads can observe transformations that would be undetectable in a sequential program, and (2) contemporary multiprocessors commonly use relaxed memory models that complicate the reasoning. In this paper, we present a novel proof methodology for verifying that a local program transformation is sound with respect to a specific hardware memory model, in the sense that it is not observable in any context. The methodology is based on a structural induction and relies on a novel compositional denotational semantics for relaxed memory models that formalizes (1) the behaviors of program fragments as a set of traces, and (2) the effect of memory model relaxations as local trace rewrite operations. To apply this methodology in practice, we implemented a semi- automated tool called Traver and used it to verify/falsify several compiler transformations for a number of different hardware memory models.
Publishing Year
Date Published
2010-04-21
Volume
6011
Page
104 - 123
Conference
CC: Compiler Construction
Conference Location
Pahos, Cyprus
Conference Date
2010-03-20 – 2010-03-28
IST-REx-ID

Cite this

Burckhardt S, Musuvathi M, Singh V. Verifying local transformations on relaxed memory models. In: Gupta R, ed. Vol 6011. Springer; 2010:104-123. doi:10.1007/978-3-642-11970-5_7
Burckhardt, S., Musuvathi, M., & Singh, V. (2010). Verifying local transformations on relaxed memory models. In R. Gupta (Ed.) (Vol. 6011, pp. 104–123). Presented at the CC: Compiler Construction, Pahos, Cyprus: Springer. https://doi.org/10.1007/978-3-642-11970-5_7
Burckhardt, Sebastian, Madanlal Musuvathi, and Vasu Singh. “Verifying Local Transformations on Relaxed Memory Models.” edited by Rajiv Gupta, 6011:104–23. Springer, 2010. https://doi.org/10.1007/978-3-642-11970-5_7.
S. Burckhardt, M. Musuvathi, and V. Singh, “Verifying local transformations on relaxed memory models,” presented at the CC: Compiler Construction, Pahos, Cyprus, 2010, vol. 6011, pp. 104–123.
Burckhardt S, Musuvathi M, Singh V. 2010. Verifying local transformations on relaxed memory models. CC: Compiler Construction, LNCS, vol. 6011. 104–123.
Burckhardt, Sebastian, et al. Verifying Local Transformations on Relaxed Memory Models. Edited by Rajiv Gupta, vol. 6011, Springer, 2010, pp. 104–23, doi:10.1007/978-3-642-11970-5_7.

Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar