| HAL-Inria | Publications, software ... of Inria's scientists |
A Generic Formalised Framework for Reasoning About Weak Memory Models
Abstract : This paper describes Coq libraries devoted to the semantic of relaxed memory models. These libraries formalise a framework which covers a large class of industrial models. Implementing this framework inside a proof assistant has significantly helped improving its design and crafting the most concise and relevant specifications. Similarly the use of a proof assistant has been instrumental in the study of the semantic of synchronisation primitives, which we illustrate by the formal proof of a barrier placement theorem. We explain the choices we made to re-design our Coq libraries, and in particular what we gained from adopting a small-scale reflection methodology.
Cited literature [21 references]
https://hal.inria.fr/inria-00604656
Contributor : Assia Mahboubi Connect in order to contact the contributor
Submitted on : Wednesday, June 29, 2011 - 2:31:55 PM
Last modification on : Tuesday, January 11, 2022 - 11:16:20 AM
Long-term archiving on: : Monday, November 12, 2012 - 9:46:59 AM
Contributor : Assia Mahboubi Connect in order to contact the contributor
Submitted on : Wednesday, June 29, 2011 - 2:31:55 PM
Last modification on : Tuesday, January 11, 2022 - 11:16:20 AM
Long-term archiving on: : Monday, November 12, 2012 - 9:46:59 AM
File
itp.pdf
Files produced by the author(s)