Abstract
Processor cores within modern multicore systems often communicate via shared memory and use (local) store buffers to improve performance. A penalty for this improvement is the loss of Sequential Consistency to weaker memory guarantees that increase the number of possible program behaviours, and hence, require a greater amount of programming effort. This paper formalises the effect of Total Store Order (TSO) memory — a weak memory model that allows a write followed by a read in the program order to be reordered during execution. Although the precise effects of TSO are well-known, a high-level formalisation of programs that execute under TSO has not been developed. We present an interval-based semantics for programs that execute under TSO memory and include methods for fine-grained expression evaluation, capturing the non-determinism of both concurrency and TSO-related reorderings.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Adve, S.V., Gharachorloo, K.: Shared memory consistency models: A tutorial. IEEE Computer 29(12), 66–76 (1996)
Alglave, J., Kroening, D., Nimal, V., Tautschnig, M.: Software verification for weak memory via program transformation. CoRR, abs/1207.7264 (2012)
Arvind, A., Maessen, J.-W.: Memory model = instruction reordering + store atomicity. SIGARCH Comput. Archit. News 34(2), 29–40 (2006)
Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: On the verification problem for weak memory models. In: POPL, pp. 7–18. ACM, New York (2010)
Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55–72. Springer, Heidelberg (2003)
Burckhardt, S., Alur, R., Martin, M.M.K.: Checkfence: Checking consistency of concurrent data types on relaxed memory models. In: PLDI, pp. 12–21 (2007)
Inc. CORPORATE SPARC International. The SPARC architecture manual: version 8. Prentice-Hall, Inc., Upper Saddle River, NJ, USA (1992)
Dongol, B., Derrick, J.: Proving linearisability via coarse-grained abstraction. CoRR, abs/1212.5116 (2012)
Dongol, B., Derrick, J., Hayes, I.J.: Fractional permissions and non-deterministic evaluators in interval temporal logic. ECEASST 53 (2012)
Dongol, B., Hayes, I.J.: Deriving real-time action systems controllers from multiscale system specifications. In: Gibbons, J., Nogueira, P. (eds.) MPC 2012. LNCS, vol. 7342, pp. 102–131. Springer, Heidelberg (2012)
Dongol, B., Hayes, I.J.: Rely/guarantee reasoning for teleo-reactive programs over multiple time bands. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol. 7321, pp. 39–53. Springer, Heidelberg (2012)
Dongol, B., Hayes, I.J., Meinicke, L., Solin, K.: Towards an algebra for real-time programs. In: Kahl, W., Griffin, T.G. (eds.) RAMICS 2012. LNCS, vol. 7560, pp. 50–65. Springer, Heidelberg (2012)
Hayes, I.J., Burns, A., Dongol, B., Jones, C.: Comparing degrees of non-determinism in expression evaluation. The Computer Journal (accepted January 4, 2013)
Herlihy, M., Moss, J.E.B.: Transactional memory: Architectural support for lock-free data structures. In: Jay Smith, A. (ed.) ISCA, pp. 289–300. ACM (1993)
Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463–492 (1990)
Intel, Santa Clara, CA, USA. Intel 64 and IA-32 Architectures Software Developer’s Manual Volume 3A: System Programming Guide, Part 1 (May 2012)
Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Prog. Lang. and Syst. 5(4), 596–619 (1983)
Jones, C.B., Pierce, K.: Elucidating concurrent algorithms via layers of abstraction and reification. Formal Aspects of Computing 23, 289–306 (2011)
Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Computers 28(9), 690–691 (1979)
Morgan, C.: Programming from Specifications. Prentice-Hall (1990)
Moszkowski, B.C.: A complete axiomatization of Interval Temporal Logic with infinite time. In: LICS, pp. 241–252 (2000)
AMD64 Architecture Programmer’s Manual Volume 2: System Programming (2012), http://support.amd.com/us/Processor_TechDocs/24593_APM_v2.pdf
Park, S., Dill, D.L.: An executable specification, analyzer and verifier for RMO (relaxed memory order). In: SPAA, pp. 34–41 (1995)
Sewell, P., Sarkar, S., Owens, S., Nardelli, F.Z., Myreen, M.O.: x86-TSO: A rigorous and usable programmer’s model for x86 multiprocessors. Commun. ACM 53(7), 89–97 (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dongol, B., Travkin, O., Derrick, J., Wehrheim, H. (2013). A High-Level Semantics for Program Execution under Total Store Order Memory. In: Liu, Z., Woodcock, J., Zhu, H. (eds) Theoretical Aspects of Computing – ICTAC 2013. ICTAC 2013. Lecture Notes in Computer Science, vol 8049. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39718-9_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-39718-9_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39717-2
Online ISBN: 978-3-642-39718-9
eBook Packages: Computer ScienceComputer Science (R0)