The Community for Technology Leaders
RSS Icon
Issue No.07 - July (2012 vol.23)
pp: 1240-1254
Alain Girault , INRIA Rhône-Alpes and LIG Laboratory, POP ART team, Grenoble
Avinash Malik , IBM Research Dublin and Trinity College Dublin, Dublin
The paper presents a programming language, DSystemJ, for dynamic distributed Globally Asynchronous Locally Synchronous (GALS) systems, its formal model of computation, formal syntax and semantics, its compilation and implementation. The language is aimed at dynamic distributed systems, which use socket based communication protocols for communicating between components. DSystemJ allows the creation and control at runtime of asynchronous processes called clock-domains, their mobility on a distributed execution platform, as well as the runtime reconfiguration of the system's functionality and topology. As DSystemJ is based on a GALS model of computation and has a formal semantics, it offers very safe mechanisms for implementation of distributed systems, as well as potential for their formal verification. The details and principles of its compilation, as well as its required runtime support are described. The runtime support is implemented in the SystemJ GALS language that can be considered as a static subset of DSystemJ.
GALS systems, distributed programming, dynamic reconfiguration, weak mobility, formal model of computation, semantics, CSP, \pi-calculus, SystemJ, DSystemJ.
Alain Girault, Avinash Malik, "Formal Semantics, Compilation and Execution of the GALS Programming Language DSystemJ", IEEE Transactions on Parallel & Distributed Systems, vol.23, no. 7, pp. 1240-1254, July 2012, doi:10.1109/TPDS.2011.258
[1] E. Lee, "The Problem with Threads," Computer, vol. 39, no. 5, pp. 33-42, May 2006.
[2] M.J. Quinn, Parallel Programming in C with MPI and OpenMP. McGraw-Hill, Inc., 2004.
[3] "The JADE Website," http:/, 2010.
[4] J. Burch, E. Clarke, K. McMillan, D. Dill, and L. Hwang, "Symbolic Model Checking: $10^{20}$ States and Beyond," Proc. IEEE Fifth Ann. Symp. Logic in Computer Science (LICS '90), pp. 428-439, June 1990.
[5] C.A.R. Hoare, Communicating Sequential Processes. Prentice Hall, 1985.
[6] J. Galletly, Occam-2, second ed. Univ. College London Press, 1996.
[7] R. Milner, Communication and Concurrency. Prentice-Hall, Inc., 1989.
[8] P. Welch and F. Barnes, "Communicating Mobile Processes: Introducing Occam-pi," Proc. Symp. Occasion of 25 Years of Comm. Sequential Processes (CSP), A. Abdallah, C. Jones, and J. Sanders, eds., pp. 175-210,, Apr. 2005.
[9] C. Fournet and G. Gonthier, "The Reflexive CHAM and the Join-Calculus," Proc. 23rd ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages (POPL '96), pp. 372-385, 1996.
[10] L. Mandel and L. Maranget, "Programming in JoCaml - Extended Version," Technical Report 6261, INRIA, 2008.
[11] W. Clinger, "Foundations of Actor Semantics," PhD dissertation, Massachusetts Inst. of Tech nology, 1981.
[12] "ActorFoundry," http://osl.cs.uiuc.eduaf/, 2010.
[13] M. Odersky, P. Altherr, V. Crement, I. Dragos, G. Dubochet, B. Emir, S. McDirmid, S. Micheloud, N. Mihaylov, M. Schinz, E. Stenman, L. Spoon, and M. Zenger, "An Overview of the Scala Programming Language," Technical Report IC/2004/64, EPFL Lausanne, Switzerland, 2004.
[14] R. Virding, C. Wikstrom, and M. Williams, Concurrent Programming in Erlang, second ed. Prentice Hall PTR, 1996.
[15] A. Malik, Z. Salcic, P.S. Roop, and A. Girault, "SystemJ: A GALS Language for System Level Design," Elsevier J. Computer Languages, Systems and Structures, vol. 36, no. 4, pp. 317-344, Dec. 2010.
[16] G. Berry, "The Semantics of Pure Esterel," , 1993.
[17] L. Henry, Reference Manual for the ADA Programming Language. Springer-Verlag, 1983.
[18] A. Malik, Z. Salcic, and P.S. Roop, "SystemJ Compilation Using the Tandem Virtual Machine Approach," ACM Trans. Design Automation of Electronic Systems, vol. 14, no. 3, pp. 1-37, 2009.
[19] A. Malik, "Principia Lingua SystemJ," PhD dissertation, Univ. of Auckland, 2010.
[20] D. Potop-Butucaru, S.A. Edwards, and G. Berry, Compiling Esterel. Springer Verlag, May 2007.
[21] A. Malik, Z. Salcic, A. Girault, A. Walker, and S.C. Lee, "A Customizable Multiprocessor for Globally Asynchronous Locally Synchronous Execution," Proc. Seventh Int'l Workshop Java Technologies for Real-Time and Embedded Systems (JTRES '09), pp. 120-129, 2009.
[22] S.F. Siegel and G.S. Avrunin, "Verification of MPI-Based Software for Scientific Computation," Proc. 11th Int'l SPIN Workshop Model Checking Software, S. Graf and L. Mounier, eds., pp. 286-303, 2004.
[23] A. Vo, S. Vakkalanka, M. DeLisi, G. Gopalakrishnan, R.M. Kirby, and R. Thakur, "Formal Verification of Practical MPI Programs," Proc. 14th ACM SIGPLAN Symp. Principles and Practice of Parallel Programming (PPoPP '09), pp. 261-270, 2009.
[24] G. Li, M. Delisi, G. Gopalakrishnan, and R.M. Kirby, "Formal Specification of the MPI-2.0 Standard in TLA+," Proc. 13th ACM SIGPLAN Symp. Principles and Practice of Parallel Programming (PPoPP '08), pp. 283-284, 2008.
[25] L. Mandel and M. Pouzet, "ReactiveML: A Reactive Extension to ML," Proc. Seventh ACM SIGPLAN Int'l Conf. Principles and Practice of Declarative Programming (PPDP), pp. 82-93, 2005.
[26] R. Milner, J. Parrow, and D. Walker, "A Calculus of Mobile Processes, I," Information and Computation, vol. 100, no. 1, pp. 1-40, 1992.
[27] C. Varela and G. Agha, "Programming Dynamically Reconfigurable Open Systems with SALSA," ACM SIGPLAN Notices, vol. 36, no. 12, pp. 20-34, Dec. 2001.
[28] J.H. Reppy, "CML: A Higher Concurrent Language," Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI '91), pp. 293-305, 113470 , 1991.
[29] S.P. Jones, A. Gordon, and S. Finne, "Concurrent Haskell," Proc. Ann. Symp. Principles of Programming Languages (POPL '96), pp. 295-308, 1996.
[30] "The DSystemJ Website," http:/, 2010.
[31] "The Foundation for Intelligent Physical Agents," http:/www., 2010.
[32] K. Havelund and T. Pressburger, "Model Checking Java Programs Using Java PathFinder," Int'l J. Software Tools for Technology Transfer, vol. 2, no. 4, pp. 366-381, 2000.
23 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool