Concurrency is a ubiquitous phenomenon in modern software ranging from distributed systems communicating over the Internet to communicating processes running on multi-core processors and multi-processors. Therefore modern programming languages offer ways to program concurrency effectively. Still, writing correct concurrent programs is notoriously difficult because of the complexity of possible interactions between concurrent processes and because concurrency-related errors are often subtle and hard to reproduce, especially for safety-critical applications. This thesis develops and formally investigates different static analysis methods for various concurrency-related problems in concurrent object-oriented programming languages to guarantee the absence of common concurrency-related errors, hence contribute to the quality of concurrent programs.
Aspects covered by our analyses involve lock-based concurrency, transaction-based concurrency, resource consumption and inheritance. In the lock-based setting, using explicit locks in a non-lexical scope to protect critical regions might be the source of aliasing problems or misuse of locks. In the transaction-based model, a similar problem of misuse of non-lexical transactions can happen in the same way as the misuse of explicit locks. Furthermore, for the purpose of checking conflicts and supporting rollback mechanisms, additional storage are required to keep track of changes during transactions’ execution which can lead to resource consumption problems. So it is useful to investigate different analysis methods to achieve safe concurrent programs. In open systems, the combination of inheritance and late-binding problematic, e.g., replacing one base class by another, seemingly satisfying the same interface description, may break the code of the client of the base class. This thesis also investigates an observable interface behavior of open systems for a concurrent object-oriented language with single-class inheritance where code from the environment can be inherited to the component and vice versa.
All analyses developed in this work are formulated as static type and effect systems resp. an open semantics based on a type and effect system. As usual for type and effect systems, they are formalized as derivation systems over the syntax of the languages, and thus compositional. In all cases, we prove the correctness of the analyses. When based on a rigorous formal foundation, the analyses can give robust guarantees concerning the safety of the program. To tackle the complexity of large and distributed applications, we have insisted that all the analysis methods in this thesis should be compositional. In other words, our analyses are scalable, i.e., a composed program should be analyzed in a divide-and-conquer manner relying on the results of the analysis of its sub-parts, so they are useful in practice.
List of papers. Papers 2-4, numbered as chapters 9-11 in this thesis, are removed from the thesis due to publisher restrictions.
Paper 1 / Chapter 8: T. Mai Thuong Tran and M. Steffen. Safe commits for Transactional Featherweight Java. Proceedings of the 8th International Conference on Integrated Formal Methods (iFM 2010), volume 6396 of Lecture Notes in Computer Science, pages 290– 304. An earlier and longer version has appeared as UiO, Dept. of Informatics Technical Report 392, Oct. 2009. doi:10.1007/978-3-642-16265-7_21 The final publication is available at link.springer.com
Paper 2 / Chapter 9: T. Mai Thuong Tran, M. Steffen, and H. Truong. Compositional static analysis for implicit join synchronization in a transactional setting. Proceedings of the 11th International Conference (SEFM 2013), volume 8137 of Lecture Notes in Computer Science, pages 212-228. doi:10.1007/978-3-642-40561-7_15
Paper 3 / Chapter 10: E. B. Johnsen, T. Mai Thuong Tran, O. Owe, and M. Steffen. Safe locking for multithreaded Java with exceptions. Journal of Logic and Algebraic Programming, Volume 81, Issue 3, April 2012, Pages 257–283, doi:10.1016/j.jlap.2011.11.002
Paper 4 / Chapter 11: E. Ábrahám, T. Mai Thuong Tran, and M. Steffen. Observable interface behavior and inheritance. Nov. 2012. Accepted for publication in the Special Issue on Behavioral Types in the Journal of Mathematical Structures in Computer Science (MSCS).
Paper 5 / Chapter 12: T. Mai Thuong Tran and M. Steffen. Design issues in concurrent object-oriented languages and observability. In Proceedings of the Third International Conference on Knowledge and Systems Engineering (KSE 2011), Hanoi 14th-17th Oct, 2011, pages 135–142. IEEE Computer Society CPS, June 2011. doi:10.1109/KSE.2011.28 Copyright 2011 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other users, including reprinting/ republishing this material for advertising or promotional purposes, creating new collective works for resale or redistribution to servers or lists, or reuse of any copyrighted components of this work in other works.