Sven Stork
Joshua Sunshine
Alcides Fonseca
Jonathan Aldrich
Skip Abstract Section
Abstract
Writing concurrent applications is extremely challenging, not only in terms of producing bug-free and maintainable software, but also for enabling developer productivity. In this article we present the Æminium concurrent-by-default programming language. Using Æminium programmers express data dependencies rather than control flow between instructions. Dependencies are expressed using permissions, which are used by the type system to automatically parallelize the application. The Æminium approach provides a modular and composable mechanism for writing concurrent applications, preventing data races in a provable way. This allows programmers to shift their attention from low-level, error-prone reasoning about thread interleaving and synchronization to focus on the core functionality of their applications. We study the semantics of Æminium through μÆminium, a sound core calculus that leverages permission flow to enable concurrent-by-default execution. After discussing our prototype implementation we present several case studies of our system. Our case studies show up to 6.5X speedup on an eight-core machine when leveraging data group permissions to manage access to shared state, and more than 70% higher throughput in a Web server application.
- Acar, U. A., Charguéraud, A., and Rainey, M. 2011. Oracle scheduling: Controlling granularity in implicitly parallel languages. In Proceedings of the ACM International Conference on Object Oriented Programming Systems, Languages, and Applications (OOPSLA’11). Google Scholar
Digital Library
- Adve, S. V. and Boehm, H.-J. 2010. Memory models: A case for rethinking parallel languages and hardware. Comm. ACM 53, 8, 90--101. Google ScholarDigital Library
- Aldrich, J., Sunshine, J., Saini, D., and Sparks, Z. 2009. Typestate-oriented programming. In Proceedings of the ACM International Conference on Object Oriented Programming Systems, Languages, and Applications (OOPSLA’09). Google ScholarDigital Library
- Aldrich, J., Beckman, N. E., Bocchino, R., Naden, K., Saini, D., Stork, S., and Sunshine, J. 2012. The plaid language: Typed core specification. Tech. rep. CMU-ISR-12-103, Carnegie Mellon University.Google Scholar
- Allen, E., Chase, D., Hallett, J., Luchangco, V., Maessen, J., Ryu, S., Steele Jr, G., and Tobinhochstadt, S. 2008. The fortress language specification version 1.0. Tech. rep., Sun Microsystems.Google Scholar
- Anderson, Z., Gay, D., Ennals, R., and Brewer, E. 2008. Sharc: Checking data sharing strategies for multithreaded C. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’08). ACM Press, New York, 149--158. Google ScholarDigital Library
- Beckman, N. E., Bierhoff, K., and Aldrich, J. 2008. Verifying correct usage of atomic blocks and typestate. In Proceedings of the ACM International Conference on Object Oriented Programming Systems, Languages and Applications (OOPSLA’08). Google ScholarDigital Library
- Blelloch, G. E. and Greiner, J. 1996. A provable time and space efficient implementation of NESL. In Proceedings of the 1st ACM SIGPLAN International Conference on Functional Programming (ICFP’96). 213--225. Google ScholarDigital Library
- Blumofe, R. D., Joerg, C. F., Kuszmaul, B. C., Leiserson, C. E., Randall, K. H., and Zhou, Y. 1995. Cilk: An efficient multithreaded runtime system. In Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP’95). Google ScholarDigital Library
- Bocchino, Jr., R. L., Adve, V. S., Dig, D., Adve, S. V., Heumann, S., Komuravelli, R., Overbey, J., Simmons, P., Sung, H., and Vakilian, M. 2009. A type and effect system for deterministic parallel Java. In Proceedings of the ACM International Conference on Object Oriented Programming Systems, Languages and Applications (OOPSLA’09). Google ScholarDigital Library
- Bocchino, Jr., R., Heumann, S., Honarmand, N., Adve, S., Adve, V., Welc, A., and Shpeisman, T. 2011. Safe nondeterminism in a deterministic-by-default parallel language. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’11). 535--548. Google ScholarDigital Library
- Boehm, H.-J. 2009. Transactional memory should be an implementation technique, not a programming interface. Tech. rep. HPL-2009-45, HP Laboratories.Google Scholar
- Boyapati, C., Lee, R., and Rinard, M. 2002. Ownership types for safe programming: Preventing data races and deadlocks. In Proceedings of the ACM International Conference on Object Oriented Programming Systems, Languages and Applications (OOPSLA’02). 211--230. Google ScholarDigital Library
- Boyland, J. 2003. Checking interference with fractional permissions. In Proceedings of the 10th International Symposium on Static Analysis. Google ScholarDigital Library
- Clarke, D. G., Potter, J. M., and Noble, J. 1998. Ownership types for flexible alias protection. In Proceedings of the ACM International Conference on Object Oriented Programming Systems, Languages and Applications (OOPSLA’98). 48--64. Google ScholarDigital Library
- Click, C. and Paleczny, M. 1995. A simple graph-based intermediate representation. In Papers from the ACM SIGPLAN Workshop on Intermediate Representations (IR’95). ACM Press, New York, 35--49. Google ScholarDigital Library
- Craik, A. and Kelly, W. 2010. Using ownership to reason about inherent parallelism in object-oriented programs. In Proceedings of the 19th Joint European Conference on Theory and Practice of Software, and the International Conference on Compiler Construction (CC’10/ETAPS’10). 145--164. Google ScholarDigital Library
- Fahndrich, M. and Deline, R. 2002. Adoption and focus: Practical linear types for imperative programming. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’02). Vol. 37, ACM Press, New York, 13--24. Google ScholarDigital Library
- Galilée, F., Cavalheiro, G. G., Louis Roch, J., and Doreille, M. 1998. Athapascan-1: On-line building data flow graph in a parallel language. In Proceedings of the International Conference on Parallel Architectures and Compilation Techniques. 88. Google ScholarDigital Library
- Gifford, D. K. and Lucassen, J. M. 1986. Integrating functional and imperative programming. In Proceedings of the ACM Conference on LISP and Functional Programming (LFP’86). 28--38. Google ScholarDigital Library
- Girard, J.-Y. 1987. Linear logic. Theor. Comput. Sci. 50, 1. Google ScholarDigital Library
- Goldberg, A. and Robson, D. 1983. Smalltalk-80: The Language and its Implementation. Addison-Wesley Longman Publishing, Boston, MA. Google ScholarDigital Library
- Hindman, B. and Grossman, D. 2006. Atomicity via source-to-source translation. In Proceedings of the Workshop on Memory System Performance and Correctness (MSPC’06). ACM Press, New York, 82--91. Google ScholarDigital Library
- Igarashi, A., Pierce, B. C., and Wadler, P. 2001. Featherweight Java: A minimal core calculus for Java and GJ. In Proceedings of the ACM International Conference on Object Oriented Programming Systems, Languages and Applications (OOPSLA’01). Google ScholarDigital Library
- Leino, K. R. M. 1998. Data groups: Specifying the modification of extended state. In Proceedings of the ACM International Conference on Object Oriented Programming Systems, Languages and Applications (OOPSLA’98). Google ScholarDigital Library
- Leino, K. R. M., Poetzsch-Heffter, A., and Zhou, Y. 2002. Using data groups to specify and check side effects. ACM SIGPLAN Not. 37, 5, 246--257. Google ScholarDigital Library
- McKeeman, W. M. 1965. Peephole optimization. Comm. ACM 8, 443--444. Google ScholarDigital Library
- Microsoft Corporation 2009. Axum programmer’s guide. http://msdn.microsoft.com/en-us/devlabs/dd795202.aspx.Google Scholar
- Moggi, E. 1991. Notions of computation and monads. Inf. Comput. 93, 1, 55--92. Google ScholarDigital Library
- Moore, K. F. and Grossman, D. 2008. High-level small-step operational semantics for transactions. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’08). Google ScholarDigital Library
- Naden, K., Bocchino, R., Aldrich, J., and Bierhoff, K. 2012. A type system for borrowing permissions. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’12). ACM Press, New York, 557--570. Google ScholarDigital Library
- Pierce, B. C. 2002. Types and Programming Languages. MIT Press, Cambridge, MA. Google ScholarDigital Library
- Rumbaugh, J. 1975. A parallel asynchronous computer architecture for data flow programs. Ph.D. thesis, MIT-LCS-TR-150, MIT.Google Scholar
- Sarkar, V. 1989. Partitioning and Scheduling Parallel Programs for Multiprocessors. MIT Press, Cambridge, MA. Google ScholarDigital Library
- Stork, S. 2013. ÆMINIUM- Freeing programmers from the shackles of sequentiality. Ph.D. thesis, School of Computer Science, Carnegie Mellon University.Google Scholar
- Stork, S., Aldrich, J., and Marques, P. 2010. Micro-AEmimium language specification. Tech. rep. CMU-ISR-10-125R2, Carnegie Mellon University.Google Scholar
- Stork, S., Marques, P., and Aldrich, J. 2009. Concurrency by default: Using permissions to express dataflow in stateful programs. In Proceedings of the 24th ACM SIGPLAN Conference Companion on Object Oriented Programming Systems Languages and Applications. 933--940. Google ScholarDigital Library
- Stork, S., Naden, K., and Sunshine, J. 2012. AEminium code repository. http://goo.gl/olbMs.Google Scholar
- Sunshine, J., Naden, K., Stork, S., Aldrich, J., and Tanter, E. 2011. First-class state change in plaid. In Proceedings of the ACM International Conference on Object Oriented Programming Systems, Languages and Applications (OOPSLA’11). ACM Press, New York, 713--732. Google ScholarDigital Library
- Vaziri, M., Tip, F., Dolby, J., and Vitek, J. 2010. A type system for data-centric synchronization. In Proceedings of the ACM International Conference on Object Oriented Programming Systems, Languages and Applications (OOPSLA’10). Google ScholarDigital Library
Index Terms
- Æminium: A Permission-Based Concurrent-by-Default Programming Language Approach
Recommendations
Æminium: a permission based concurrent-by-default programming language approach
PLDI '14The aim of ÆMINIUM is to study the implications of having a concurrent-by-default programming language. This includes language design, runtime system, performance and software engineering considerations.
We conduct our study through the design of the ...
Æminium: a permission based concurrent-by-default programming language approach
PLDI '14: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and ImplementationThe aim of ÆMINIUM is to study the implications of having a concurrent-by-default programming language. This includes language design, runtime system, performance and software engineering considerations.
We conduct our study through the design of the ...
Permission accounting in separation logic
Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languagesA lightweight logical approach to race-free sharing of heap storage between concurrent threads is described, based on the notion of permission to access. Transfer of permission between threads, subdivision and combination of permission is discussed. The ...
Comments