Current multiprocessors provide weak or relaxed memory models. Existing program logics assume sequential consistency, and are therefore typically unsound for weak memory. We introduce a novel Rely-Guarantee style proof system for reasoning about x86 assembly programs running against the weak x86-TSO memory model. Interesting features of the logic include processor assertions which can refer to the local state of other processors (including their program counters), and a syntactic operation of closing an assertion under write buffer interference. We use the expressivity of the proof system to construct a new correctness proof for an x86-TSO version of Simpson's four slot algorithm. Mechanization in the Hol theorem prover provides a flexible tool to support semi-automated verification. © 2010 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Ridge, T. (2010). A rely-guarantee proof system for x86-TSO. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6217 LNCS, pp. 55–70). https://doi.org/10.1007/978-3-642-15057-9_4
Mendeley helps you to discover research relevant for your work.