Safe and Verifiable Design of Concurrent Java Programs

Abstract

The design of concurrent programs has a reputation for being difficult, and thus potentially dangerous in safety-critical real-time and embedded systems. The recent appearance of Java, while cleaning up many insecure aspects of OO programming endemic in C++ , suffers from a deceptively simple threads model that is an insecure variant of ideas that are over 25 years old. Consequently, we cannot directly exploit a range of new CASE tools " based on modern developments in parallel computing theory " that can verify and check the design of concurrent systems for a variety of dangers such as deadlock and livelock that otherwise plague us during testing and maintenance and, more seriously, cause catastrophic failure in service. The approach proposed in this paper uses recently developed Java class libraries based on Hoare's Communicating Sequential Processes (CSP); the use of CSP greatly simplifies the design of concurrent systems and, in many cases, a parallel approach often significantly simplifies systems originally approached sequentially. New CSP CASE tools permit designs to be verified against formal specifications and checked for deadlock and livelock. We introduce CSP and its implementation in Java and develop a small concurrent application. The formal CSP description of the application is provided, as well as that of an equivalent sequential version. FDR is used to verify the correctness of both implementations, their equivalence, and their freedom from deadlock and livelock.

Key Words:

• Concurrency
• multithreading
• Java
• CSP
• formal methods

Additional information

Notes on contributors

P.H. Welch

Peter Welch completed an undergraduate degree in mathematics and a Ph.D. in computer science at Warwick University; his doctoral research was on semantic models for the lamb da-calculus. His main area of research an d teaching is parallel computing. He has contributed to theoretical developments (e.g., CSP-based design rules for process networks with proven safety properties), tools supporting those rules, parallel language compilers, very lightweight CSP kernels (with sub-microsecond process management), and CSP class libraries for Java. He is currently working on design rules for eliminating race-hazards from shared-memory multiprocessing systems with dynamic memory allocation, higher level synchronization primitives, SMP multithreading kernels, and the exploitation of these ideas in Java. He is Professor of Parallel Computing at the University of Kent at Canterbury, England, and is the current chair of the World occam and/o r Transputer User Group (WoTUG). Professor Welch has over 50 refereed technical publications and is frequently an invited speaker.

G.H. Hilderink

Gerald Hilderink is currently a Ph.D. student in computer engineering at the Control Laboratory of the University of Twente, The Netherlands. His main research interest is the development of a reliable foundation using formal methods for real-time and embedded system design. He is interested in proposing a new parallel model for real-time and embedded systems programming in Java. He has developed the CSP channel class concept for Java and has implemented the CTJ channel class library.

A.W.P. Bakkers

André Bakkers is a professor at the Dutch Open University in Information Technology, emphasizing real time and parallel systems. He also works at the University of Twente Control Laboratory. In 1977 he joined Twente University as a senior lecturer with the control systems and computer engineering group, of the electrical engineering faculty. Together with the University of Kent he acquired two COMET T projects: "Occam and Transputer Engineering I and II". These projects have set an international standard for the education and training in the area of parallel systems; their results are used at universities around the world and have been incorporated into Java channel class libraries. His present research covers the realization of real-time control systems using heterogeneous parallel processing. He has guided three Ph.D. students in this area. He has also organized and edited the proceedings of several WoTUG conferences.

G.S. Stiles

G.S. Stiles graduated in philosophy from the University of Washington in 1966 and received the M.Sc. and Ph.D. degrees in electrical engineering from Stanford University in 1972 and 1975. His doctoral and post-doctoral work (at Los Alamos) was in computational aspects of space physics III; and engineering. Since moving to Utah State University, where he is % i currently a professor of electrical ering, he has concentrated on applications and implementations of parallel computing, particularly in the areas of real-time and near real-time high-performance data acquisition and analysis systems and stochastic optimization algorithms. Professor Stiles was the founding chair of the North American Transputer Users Group, was an associate editor of Transputer Communications, and is presently an editor of the Concurrent Systems Engineering Series of 10S Press. He has over 30 refereed journal and conference proceeding to his credit, and has presented four workshops and tutorials on parallel computing at international conferences.