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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Armstrong, J., Virding, R., Wikström, C., Williams, M.: Concurrent programming in Erlang. Prentice Hall (1996)
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)
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)
Boyland, J.: Checking Interference with Fractional Permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55–72. Springer, Heidelberg (2003)
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)
Dietl, W., Müller, P.: Universes: Lightweight ownership for JML. Journal of Object Technology 4(8), 5–32 (2005)
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)
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)
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)
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
Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Transactions on Computers 28(9), 690–691 (1979)
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)
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
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)