[{"language":[{}],"publication_status":"published","volume":6011,"oa_version":"None","abstract":[{"lang":"eng"}],"intvolume":" 6011","month":"04","alternative_title":[],"creator":{"login":"apreinsp","id":"4435EBFC-F248-11E8-B48F-1D18A9856A87"},"extern":"1","date_updated":"2021-01-12T07:56:39Z","_id":"4395","status":"public","conference":{"name":"CC: Compiler Construction","start_date":"2010-03-20","end_date":"2010-03-28","location":"Pahos, Cyprus"},"type":"conference","dc":{"type":["info:eu-repo/semantics/conferenceObject","doc-type:conferenceObject","text","http://purl.org/coar/resource_type/c_5794"],"publisher":["Springer"],"date":["2010"],"identifier":["https://research-explorer.ista.ac.at/record/4395"],"description":["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."],"relation":["info:eu-repo/semantics/altIdentifier/doi/10.1007/978-3-642-11970-5_7"],"source":["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"],"title":["Verifying local transformations on relaxed memory models","LNCS"],"rights":["info:eu-repo/semantics/closedAccess"],"language":["eng"],"creator":["Burckhardt, Sebastian","Musuvathi, Madanlal","Singh, Vasu","Gupta, Rajiv"]},"day":"21","date_created":"2018-12-11T12:08:38Z","date_published":"2010-04-21T00:00:00Z","uri_base":"https://research-explorer.ista.ac.at","page":"104 - 123","quality_controlled":"1","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","citation":{"mla":"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.","apa":"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","ieee":"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.","short":"S. Burckhardt, M. Musuvathi, V. Singh, in:, R. Gupta (Ed.), Springer, 2010, pp. 104–123.","chicago":"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.","ista":"Burckhardt S, Musuvathi M, Singh V. 2010. Verifying local transformations on relaxed memory models. CC: Compiler Construction, LNCS, vol. 6011, 104–123."},"dini_type":"doc-type:conferenceObject","editor":[{"last_name":"Gupta","first_name":"Rajiv"}],"publist_id":"1063","author":[{"last_name":"Burckhardt","first_name":"Sebastian"},{"last_name":"Musuvathi","first_name":"Madanlal"},{"last_name":"Singh","first_name":"Vasu","id":"4DAE2708-F248-11E8-B48F-1D18A9856A87"}]}]