Abstract
Transactions are a high-level alternative for low-level concurrency-control mechanisms such as locks, semaphores, monitors. A recent proposal for integrating transactional features into programming languages is Transactional Featherweight Java (TFJ), extending Featherweight Java by adding transactions. With support for nested and multi-threaded transactions, its transactional model is rather expressive. In particular, the constructs governing transactions —to start and to commit a transaction— can be used freely with a non-lexical scope. On the downside, this flexibility also allows for an incorrect use of these constructs, e.g., trying to perform a commit outside any transaction. To catch those kinds of errors, we introduce a static type and effect system for the safe use of transactions for TFJ. We prove the soundness of our type system by subject reduction.
The work has been partly supported by the EU-project FP7-231620 HATS (Highly Adaptable and Trustworthy Software using Formal Methods).
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
Abadi, M., Birell, A., Harris, T., Isard, M.: Semantics of transactional memory and automatic mutual exclusion. In: Proceedings of POPL 2008. ACM, New York (2008)
Bigliardi, G., Laneve, C.: A type system for JVM threads. In: Proceedings of 3rd ACM SIGPLAN Workshop on Types in Compilation (TIC 2000), p. 2003 (2000)
Blundell, C., Lewis, E.C., Martin, M.K.: Subtleties of transactional memory atomicity semantics. IEEE Computer Architecture Letters 5(2) (2006)
Carlstrom, B.D., McDonald, A., Chafi, H., Chung, J., Minh, C.C., Kozyrakis, C., Oluktun, K.: The ATOMOΣ transactional programming language. In: ACM Conference on Programming Language Design and Implementation, Ottawa, Ontario, Canada. ACM, New York (2006)
Davare, A.: Concurrent BLAST, Internal Report, EECS Berkely. Mentors Rupak Majumdar and Ranjit Jhala, Mentors (2003)
Flanagan, C., Freund, S.: Atomizer: A dynamic atomicity checker for multithreaded programs. In: Proceedings of POPL 2004, pp. 256–267. ACM, New York (2004)
Flanagan, C., Quadeer, S.: A type and effect system for atomicity. In: ACM Conference on Programming Language Design and Implementation, San Diego, California. ACM, New York (2003)
Harris, T., Fraser, K.: Language support for lightweight transactions. In: Eighteenth OOPSLA 2003. SIGPLAN Notices. ACM, New York (2003)
Harris, T., Peyton Jones, S.M.S., Herlihy, M.: Composable memory transactions. In: PPoPP 2005: 10th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, pp. 48–60 (June 2005)
Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. International Journal on Software Tools for Technology Transfer 2(4), 366–381 (2000)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 235–239. Springer, Heidelberg (2003)
Igarashi, A., Kobayashi, N.: Resource usage analysis. ACM Transactions on Programming Languages and Systems 27(2), 264–313 (2005)
Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Java: A minimal core calculus for Java and GJ. In: OOPSLA 1999. SIGPLAN Notices, pp. 132–146. ACM, New York (1999)
Isard, M., Birell, A.: Automatic mutual exclusion. In: Proceedings of the 11th Workshop on Hot Topics in Operating Systems (2007)
Jagannathan, S., Vitek, J., Welc, A., Hosking, A.: A transactional object calculus. Science of Computer Programming 57(2), 164–186 (2005)
Johnsen, E.B., Owe, O., Yu, I.C.: Creol: A type-safe object-oriented model for distributed concurrent systems. Theoretical Computer Science 365(1-2), 23–66 (2006)
Tran, T.M.T., Owe, O., Steffen, M.: Safe typing for transactional vs. lock-based concurrency in multi-threaded Java. In: Proceedings of the Second International Conference on Knowledge and Systems Engineering, KSE 2010 (accepted for publication 2010)
Nielson, F., Nielson, H.-R., Hankin, C.L.: Principles of Program Analysis. Springer, Heidelberg (1999)
Ranganath, V.P., Hatcliff, J.: Slicing concurrent Java programs using Indus and Kaveri. International Journal of Software Tools and Technology Transfer 9(5), 489–504 (2007)
Steffen, M., Tran, T.M.T.: Safe commits for Transactional Featherweight Java. Technical Report 392, University of Oslo, Dept. of Computer Science (October 2009)
Welc, A., Jagannathan, S., Hosking, A.: Transactional monitors for concurrent objects. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 518–541. Springer, Heidelberg (2004)
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
Thuong Tran, T.M., Steffen, M. (2010). Safe Commits for Transactional Featherweight Java. In: Méry, D., Merz, S. (eds) Integrated Formal Methods. IFM 2010. Lecture Notes in Computer Science, vol 6396. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16265-7_21
Download citation
DOI: https://doi.org/10.1007/978-3-642-16265-7_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16264-0
Online ISBN: 978-3-642-16265-7
eBook Packages: Computer ScienceComputer Science (R0)