Skip to main content
SpringerLink
Log in

Isolation Types and Multi-core Architectures

  • Conference paper
Book cover Formal Verification of Object-Oriented Software (FoVeOOS 2011)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 7421))

Abstract

Programs distributed between two or more cores on a multi-core processor are significantly slowed down when both repeatedly access the same cache line—unless both accesses consist of reads. The hardware performs best when programs satisfy a ‘memory isolation’ property whereby each line of writable memory is available to only one processor at a time. Multi-core memory isolation encapsulates a multiple-reader/single-writer usage, with a cost incurred when changing one writer for another.

This tutorial-style work starts with a historical perspective and then shows how existing work on Kilim and its isolation-type system provides a programming-language form to express such memory isolation including ownership transfer.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 49.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Armstrong, J., Virding, R., Wikström, C., Williams, M.: Concurrent programming in Erlang. Prentice Hall (1996)

    Google Scholar 

  2. Bornat, R., Calcagno, C., O’Hearn, P., Parkinson, M.J.: Permission accounting in separation logic. In: POPL 2005: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 259–270. ACM Press (2005)

    Google Scholar 

  3. Boyland, J., Noble, J., Retert, W.: Capabilities for Sharing: A Generalisation of Uniqueness and Read-Only. In: Lindskov Knudsen, J. (ed.) ECOOP 2001. LNCS, vol. 2072, pp. 2–27. Springer, Heidelberg (2001)

    Google Scholar 

  4. Boyland, J.: Checking Interference with Fractional Permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55–72. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  5. Clarke, D.G., Potter, J.M., Noble, J.: Ownership types for flexible alias protection. In: OOPSLA 1998: Proceedings of the 13th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, pp. 48–64. ACM Press, New York (1998)

    Chapter  Google Scholar 

  6. Dietl, W., Müller, P.: Universes: Lightweight ownership for JML. Journal of Object Technology 4(8), 5–32 (2005)

    Article  Google Scholar 

  7. Ennals, R., Sharp, R., Mycroft, A.: Linear Types for Packet Processing. In: Schmidt, D.A. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 204–218. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  8. Fähndrich, M., Aiken, M., Hawblitzel, C., Hodson, O., Hunt, G., Larus, J.R., Levi, S.: Language support for fast and reliable message-based communication in singularity OS. In: EuroSys 2006: Proceedings of the 2006 EuroSys Conference, pp. 177–190. ACM Press (2006)

    Google Scholar 

  9. Haller, P., Odersky, M.: Capabilities for Uniqueness and Borrowing. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 354–378. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  10. Haller, P.: Isolated actors for race-free concurrent programming. Thèse no. 4874, École Polytechnique Fédérale de Lausanne (2010), http://biblion.epfl.ch/EPFL/theses/2010/4874/EPFL_TH4874.pdf

  11. Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Transactions on Computers 28(9), 690–691 (1979)

    Article  MATH  Google Scholar 

  12. Srinivasan, S., Mycroft, A.: Kilim: Isolation-Typed Actors for Java (a million actors, safe zero-copy communication). In: Ryan, M. (ed.) ECOOP 2008. LNCS, vol. 5142, pp. 104–128. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  13. Srinivasan, S.: Kilim: A server framework with lightweight actors, isolation types and zero-copy messaging. Technical Report 769, Computer Laboratory, University of Cambridge (2010) ISSN 1476-2986, http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-769.html

Download references

Author information

Authors and Affiliations

  1. Computer Laboratory, University of Cambridge, William Gates Building, JJ Thomson Avenue, Cambridge, CB3 0FD, UK

    Alan Mycroft

Authors
  1. Alan Mycroft
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute for Theoretical Informatics, Karlsruhe Institute of Technology, Am Fasanengarten 5, 76131, Karlsruhe, Germany

    Bernhard Beckert

  2. Dipartimento di Informatica, Università di Torino, Italy

    Ferruccio Damiani

  3. Royal Institute of Technology, Stockholm, Sweden

    Dilian Gurov

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Mycroft, A. (2012). Isolation Types and Multi-core Architectures. In: Beckert, B., Damiani, F., Gurov, D. (eds) Formal Verification of Object-Oriented Software. FoVeOOS 2011. Lecture Notes in Computer Science, vol 7421. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31762-0_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-31762-0_4

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-31761-3

  • Online ISBN: 978-3-642-31762-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation