×

zbMATH — the first resource for mathematics

Automatic distributed code generation from formal models of asynchronous processes interacting by multiway rendezvous. (English) Zbl 1362.68038
Summary: Formal process languages inheriting the concurrency and communication features of process algebras are convenient formalisms to model distributed applications, especially when they are equipped with formal verification tools (e.g., model checkers) to help hunting for bugs early in the development process. However, even starting from a fully verified formal model, bugs are likely to be introduced while translating (generally by hand) the concurrent model – which relies on high-level and expressive communication primitives – into the distributed implementation – which often relies on low-level communication primitives. In this paper, we present DLC, a compiler that enables distributed code to be generated from models written in a formal process language called LNT, which is equipped with a rich verification toolbox named CADP, and where processes interact by value-passing multiway rendezvous. The generated code uses an elaborate protocol to implement rendezvous, and can be either executed in an autonomous way (i.e., without requiring additional code to be defined by the user), or connected to external software through user-modifiable C functions. The protocol itself is modeled in LNT and verified using CADP. We present several experiments assessing the performance of DLC, including the Raft consensus algorithm.
MSC:
68N20 Theory of compilers and interpreters
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Amnell, T.; Fersman, E.; Mokrushin, L.; Pettersson, P.; Yi, W., TIMES: a tool for schedulability analysis and code generation of real-time systems, (Formal Modeling and Analysis of Timed Systems, (2004), Springer), 60-72
[2] Arbab, F., Reo: a channel-based coordination model for component composition, Math. Struct. Comput. Sci., 14, 3, 329-366, (2004) · Zbl 1085.68552
[3] Bagrodia, R., Process synchronization: design and performance evaluation of distributed algorithms, IEEE Trans. Softw. Eng., 15, 9, 1053-1065, (1989)
[4] Behrmann, G.; Larsen, K. G.; Moller, O.; David, A.; Pettersson, P.; Yi, W., Uppaal — present and future, (Proceedings of the 40th IEEE Conference on Decision and Control, vol. 3, (2001), IEEE), 2881-2886
[5] Bensalem, S.; Griesmayer, A.; Legay, A.; Nguyen, T.; Sifakis, J.; Yan, R., D-finder 2: towards efficient correctness of incremental design, (Proceedings of the 3rd NASA International Symposium on Formal Methods, NFM’2011, Pasadena, CA, USA, (2011)), 453-458
[6] Bergamini, D.; Descoubes, N.; Joubert, C.; Mateescu, R., Bisimulator: a modular tool for on-the-fly equivalence checking, (Halbwachs, N.; Zuck, L., Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’2005, Edinburgh, Scotland, UK, Lecture Notes in Computer Science, vol. 3440, (Apr. 2005), Springer), 581-585 · Zbl 1087.68583
[7] Berry, G., SCADE: synchronous design and validation of embedded control software, (Next Generation Design and Verification Methodologies for Distributed Embedded Control Systems, (2007), Springer), 19-33 · Zbl 1189.93012
[8] Bochmann, G.; Gao, Q.; Wu, C., On the distributed implementation of LOTOS, (Proceedings of the 2nd International Conference on Formal Description Techniques, FORTE’89, (1989)), 133-146
[9] Bonakdarpour, B.; Bozga, M.; Quilbeuf, J., Model-based implementation of distributed systems with priorities, Des. Autom. Embed. Syst., 17, 2, 251-276, (2013)
[10] Bouajjani, A.; Fernandez, J.-C.; Graf, S.; Rodríguez, C.; Sifakis, J., Safety for branching time semantics, (Proceedings of 18th ICALP, (1991), Springer) · Zbl 0769.68089
[11] Carbone, M.; Montesi, F., Deadlock-freedom-by-design: multiparty asynchronous global programming, (Giacobazzi, R.; Cousot, R., Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’13, Rome, Italy, (2013), ACM), 263-274 · Zbl 1301.68097
[12] D. Champelovier, X. Clerc, H. Garavel, Y. Guerte, C. McKinty, V. Powazny, F. Lang, W. Serwe, G. Smeding, Reference manual of the LNT to LOTOS translator (version 6.2), INRIA/VASY and INRIA/CONVECS, 2015, 130 pages.
[13] Chandy, K. M.; Misra, J., Parallel program design: A foundation, (1988), Addison-Wesley · Zbl 0717.68034
[14] Coste, N.; Garavel, H.; Hermanns, H.; Lang, F.; Mateescu, R.; Serwe, W., Ten years of performance evaluation for concurrent systems using CADP, (Margaria, T.; Steffen, B., Proceedings of the 4th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, Part II, ISoLA 2010 (Amirandes, Heraclion, Crete), Lecture Notes in Computer Science, vol. 6416, (2010), Springer), 128-142
[15] Dijkstra, E. W., Solution of a problem in concurrent programming control, Commun. ACM, 8, 9, 569-570, (1965)
[16] Dijkstra, E. W., Guarded commands, non-determinacy and formal derivation of programs, Commun. ACM, 18, 8, 453-457, (1975) · Zbl 0308.68017
[17] Dokter, K.; Jongmans, S. T.Q.; Arbab, F.; Bliudze, S., Relating BIP and reo, (Knight, S.; Lanese, I.; Lluch-Lafuente, A.; Vieira, H. T., Proceedings of the 8th Interaction and Concurrency Experience, ICE’2015, Grenoble, France, EPTCS, vol. 189, (2015)), 3-20
[18] Evrard, H., Génération automatique d’implémentation distribuée à partir de modèles formels de processus concurrents asynchrones, (2015), Université Grenoble Alpes, Thesis
[19] Evrard, H., DLC: compiling a concurrent system formal specification to a distributed implementation, (Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’2016, Lecture Notes in Computer Science, (2016), Springer-Verlag)
[20] Evrard, H.; Lang, F., Formal verification of distributed branching multiway synchronization protocols, (Beyer, D.; Boreale, M., Proceedings of the IFIP Joint International Conference on Formal Techniques for Distributed Systems, FORTE/FMOODS’2013, Florence, Italy, Lecture Notes in Computer Science, vol. 7892, (2013), IFIP, Springer), 146-160
[21] Evrard, H.; Lang, F., Automatic distributed code generation from formal models of asynchronous concurrent processes, (Proceedings of the 23rd Euromicro International Conference on Parallel, Distributed and Network-based Processing, PDP’2015, Turku, Finland, (2015), IEEE)
[22] Garavel, H., Reflections on the future of concurrency theory in general and process calculi in particular, (Palamidessi, C.; Valencia, F. D., Proceedings of the LIX Colloquium on Emerging Trends in Concurrency Theory, Ecole Polytechnique de Paris, France, November 13-15, 2006, Electronic Notes in Theoretical Computer Science, vol. 209, (2008), Elsevier Science Publishers), 149-164, also available as INRIA Research Report RR-6368 · Zbl 1279.68258
[23] Garavel, H.; Lang, F., SVL: a scripting language for compositional verification, (Kim, M.; Chin, B.; Kang, S.; Lee, D., Proceedings of the 21st IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems, FORTE’2001, Cheju Island, Korea, (Aug. 2001), IFIP, Kluwer Academic Publishers), 377-392, full version available as INRIA Research Report RR-4223
[24] Garavel, H.; Lang, F.; Mateescu, R., Compiler construction using LOTOS NT, (Horspool, N., Proceedings of the 11th International Conference on Compiler Construction, CC’2002, Grenoble, France, Lecture Notes in Computer Science, vol. 2304, (2002), Springer), 9-13 · Zbl 1051.68658
[25] Garavel, H.; Lang, F.; Mateescu, R., Compositional verification of asynchronous concurrent systems using CADP, Acta Inform., 52, 4, 337-392, (Apr. 2015)
[26] Garavel, H.; Lang, F.; Mateescu, R.; Serwe, W., CADP 2011: a toolbox for the construction and analysis of distributed processes, Int. J. Softw. Tools Technol. Transf., 15, 2, 89-107, (2013)
[27] Garavel, H.; Sighireanu, M., A graphical parallel composition operator for process algebras, (Wu, J.; Gao, Q.; Chanson, S. T., Proceedings of the Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification, FORTE/PSTV’99, Beijing, China, (1999), IFIP, Kluwer Academic Publishers), 185-202 · Zbl 0952.68097
[28] Garavel, H.; Viho, C.; Zendri, M., System design of a CC-numa multiprocessor architecture using formal specification, model-checking, co-simulation, and test generation, Int. J. Softw. Tools Technol. Transf., 3, 3, 314-331, (2001), also available as INRIA Research Report RR-4041 · Zbl 0991.68731
[29] Havender, J., Avoiding deadlock in multitasking systems, IBM Syst. J., 7, 2, 74-84, (1968)
[30] Holzmann, G. J., The SPIN model checker: primer and reference manual, vol. 1003, (2004), Addison-Wesley Reading
[31] ISO/IEC, LOTOS — a formal description technique based on the temporal ordering of observational behaviour, International Standard 8807, International Organization for Standardization — Information Processing Systems — Open Systems Interconnection, Geneva, 1989.
[32] ISO/IEC, Enhancements to LOTOS (E-LOTOS), International Standard 15437:2001, International Organization for Standardization — Information Technology, Geneva, 2001.
[33] Jard, C.; Jéron, T., Tgv: theory, principles and algorithms — a tool for the automatic synthesis of conformance test cases for non-deterministic reactive systems, Int. J. Softw. Tools Technol. Transf., 7, 4, 297-315, (Aug. 2005)
[34] Jongmans, S. T.Q.; Santini, F.; Arbab, F., Partially-distributed coordination with reo, (Proceedings of the 22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP’2014, Torino, Italy, (2014)), 697-706
[35] Katz, G.; Peled, D., Code mutation in verification and automatic code correction, (Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’2010, (2010), Springer), 435-450
[36] Kumar, D., An implementation of n-party synchronization using tokens, (Proceedings of the 10th International Conference on Distributed Computing Systems, ICDCS’1990, Paris, France, (1990)), 320-327
[37] Lamport, L., Paxos made simple, SIGACT News, 32, 4, 18-25, (2001)
[38] Lang, F., EXP.OPEN 2.0: a flexible tool integrating partial order, compositional, and on-the-fly verification methods, (van de Pol, J.; Romijn, J.; Smith, G., Proceedings of the 5th International Conference on Integrated Formal Methods, IFM’2005, Eindhoven, The Netherlands, Lecture Notes in Computer Science, vol. 3771, (2005), Springer), 70-88, full version available as INRIA Research Report RR-5673
[39] Lantreibecq, E.; Serwe, W., Model checking and co-simulation of a dynamic task dispatcher circuit using CADP, (Salaün, G.; Schätz, B., Proceedings of the 16th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2011, Trento, Italy, Lecture Notes in Computer Science, vol. 6959, (2011), Springer), 180-195
[40] Lockefeer, L.; Williams, D. M.; Fokkink, W. J., Formal specification and verification of TCP extended with the window scale option, Sci. Comput. Program., 118, 3-23, (2016)
[41] Löffler, S., From specification to implementation: a PROMELA to C compiler, (1996), Project Report Ecole Nationale Supérieure des Télécommunications
[42] Mañas, J. A.; de Miguel, T.; Salvachúa, J.; Azcorra, A., Tool support to implement LOTOS formal specifications, Comput. Netw. ISDN Syst., 25, 7, 815-839, (1993)
[43] Mateescu, R.; Garavel, H., Xtl: a meta-language and tool for temporal logic model-checking, (Margaria, T., Proceedings of the International Workshop on Software Tools for Technology Transfer, STTT’98, Aalborg, Denmark, (Jul. 1998), BRICS), 33-42
[44] Mateescu, R.; Sighireanu, M., Efficient on-the-fly model-checking for regular alternation-free mu-calculus, Sci. Comput. Program., 46, 3, 255-281, (Mar. 2003)
[45] Mateescu, R.; Thivolle, D., A model checking language for concurrent value-passing systems, (Cuellar, J.; Maibaum, T.; Sere, K., Proceedings of the 15th International Symposium on Formal Methods, FM’08, Turku, Finland, Lecture Notes in Computer Science, vol. 5014, (2008), Springer), 148-164
[46] Montesi, F.; Yoshida, N., Compositional choreographies, (D’Argenio, P. R.; Melgratti, H. C., Proceedings of the 24th International Conference on Concurrency Theory, CONCUR’13, Buenos Aires, Argentina, Lecture Notes in Computer Science, vol. 8052, (2013), Springer), 425-439 · Zbl 1390.68483
[47] Nestmann, U.; Pierce, B. C., Decoding choice encodings, (Montanari, U.; Sassone, V., Proceedings of the 7th International Conference on Concurrency Theory, CONCUR’96, Pisa, Italy, Lecture Notes in Computer Science, vol. 1119, (1996), Springer), 179-194
[48] Ng, N.; Yoshida, N., Pabble: parameterised scribble for parallel programming, (22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP’2014, Torino, Italy, (2014), IEEE Computer Society), 707-714
[49] Oliveira, M. V.M.; de Medeiros Júnior, I. S.; Woodcock, J., A verified protocol to implement multi-way synchronisation and interleaving in CSP, (Hierons, R. M.; Merayo, M. G.; Bravetti, M., Proceedings of the 11th International Conference on Software Engineering and Formal Methods, SEFM’2013, Madrid, Spain, Lecture Notes in Computer Science, vol. 8137, (2013), Springer), 46-60
[50] Ongaro, D.; Ousterhout, J., Safety proof and formal specification for raft, (2013)
[51] Ongaro, D.; Ousterhout, J., In search of an understandable consensus algorithm, (Proceedings of the USENIX Annual Technical Conference, USENIX ATC’2014, (2014), USENIX Association Philadelphia, PA), 305-319
[52] Park, D., Concurrency and automata on infinite sequences, (Deussen, P., Theoretical Computer Science, Lecture Notes in Computer Science, vol. 104, (1981), Springer), 167-183
[53] Parrow, J.; Sjödin, P., Designing a multiway synchronization protocol, Comput. Commun., 19, 14, 1151-1160, (1996)
[54] Pérez, J. A.; Corchuelo, R.; Toro, M., An order-based algorithm for implementing multiparty synchronization, Concurrency, 16, 12, 1173-1206, (2004)
[55] Peters, K.; Nestmann, U.; Goltz, U., On distributability in process calculi, (Felleisen, M.; Gardner, P., Proceedings of the 22nd European Symposium on Programming, ESOP’2013, Rome, Italy, Lecture Notes in Computer Science, vol. 7792, (2013), Springer), 310-329 · Zbl 1381.68215
[56] Proença, J.; Clarke, D.; de Vink, E.; Arbab, F., Dreams: a framework for distributed synchronous coordination, (Proceedings of the 27th International Symposium on Applied Computing, SAC’2012, Trento, Italy, (2012), ACM)
[57] Quilbeuf, J., Distributed implementations of component-based systems with prioritized multiparty interactions, (2013), Université de Grenoble, Ph.D. thesis
[58] Schneider, F. B., Implementing fault-tolerant services using the state machine approach: a tutorial, ACM Comput. Surv., 22, 4, 299-319, (1990)
[59] Sharma, A., A refinement calculus for PROMELA, (Proceedings of the 18th International Conference on Engineering of Complex Computer Systems, ICECCS’2013, (2013), IEEE), 75-84
[60] Sighireanu, M., Contribution à la définition et à l’implémentation du langage “extended LOTOS”, (1999), Université Joseph Fourier Grenoble, Thèse de Doctorat
[61] Sisto, R.; Ciminiera, L.; Valenzano, A., A protocol for multirendezvous of LOTOS processes, IEEE Trans. Comput., 40, 4, 437-447, (1991)
[62] Sjödin, P., From LOTOS specifications to distributed implementations, (1991), Department of Computer Science, University of Uppsala Sweden, Ph.D. thesis
[63] Taubner, D., On the implementation of Petri nets, (Rozenberg, G., Proceedings of the 8th European Workshop on Applications and Theory of Petri Nets, Zaragoza, Spain, Lecture Notes in Computer Science, vol. 340, (1987), Springer), 418-434
[64] Winkowski, J., A distributed implementation of Petri nets, (1983), Polish Academy of Science, Institute of Computer Science Warsaw, Tech. Rep. 518 · Zbl 0525.68036
[65] Yasumoto, K.; Higashino, T.; Taniguchi, K., A compiler to implement LOTOS specifications in distributed environments, Comput. Netw., 36, 2, 291-310, (2001)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.