Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Blazy, S., Leroy, X.: Mechanized semantics for the Clight subset of the C language. CoRR, abs/0901.3619 (2009)
Clint, M., Hoare, C.A.R.: Program proving: Jumps and functions. Acta Informatica 1, 214–224 (1972)
Coleman, J.W.: Expression decomposition in a Rely/Guarantee context. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol. 5295, pp. 146–160. Springer, Heidelberg (2008)
Cohen, E., Schirmer, N.: A better reduction theorem for store buffers. Technical report (2009)
Floyd, R.W.: Assigning meanings to programs. In: Proc. American Mathematical Society Symposia in Applied Mathematics, vol. 19 (1967)
Henderson, N.: Proving the correctness of Simpson’s 4-slot ACM using an assertional Rely-Guarantee proof method. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 244–263. Springer, Heidelberg (2003)
Hoare: An axiomatic basis for computer programming. CACM: Communications of the ACM 12 (1969)
Jones, C.B.: Development Methods for Computer Programmes Including a Notion of Interference. PhD thesis, Prgr. Res. Grp. 25, Oxford Univ., Comp. Lab., UK (June 1981)
Linux Kernel mailing list, thread “spin_unlock optimization(i386)”, 119 messages (November 20 - December 7, 1999), http://www.gossamer-threads.com/lists/engine?post=105365;list=linux (Accessed 2009/11/18)
Myreen, M.O., Slind, K., Gordon, M.J.C.: Machine-code verification for multiple architectures: An application of decompilation into logic. In: Proc. FMCAD (2008)
Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO. In: Urban, C. (ed.) TPHOLs 2009. LNCS, vol. 5674, pp. 391–407. Springer, Heidelberg (2009)
Owens, S.: Reasoning about the implementation of concurrency abstractions on x86-TSO. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 478–503. Springer, Heidelberg (2010)
Park, Dill: An executable specification, analyzer and verifier for RMO (relaxed memory order). In: SPAA: Annual ACM Symposium on Parallel Algorithms and Architectures (1995)
Ridge, T.: Operational reasoning for concurrent Caml programs and weak memory models. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 278–293. Springer, Heidelberg (2007)
Rushby, J.: Model checking Simpson’s four-slot fully asynchronous communication mechanism (2002)
Simpson, H.R.: Four-slot fully asynchronous communication mechanism. IEE Proceedings, Computers and Digital Techniques 137(1), 17–30 (1990)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ridge, T. (2010). A Rely-Guarantee Proof System for x86-TSO. In: Leavens, G.T., O’Hearn, P., Rajamani, S.K. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2010. Lecture Notes in Computer Science, vol 6217. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15057-9_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-15057-9_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15056-2
Online ISBN: 978-3-642-15057-9
eBook Packages: Computer ScienceComputer Science (R0)