A framework for automated distributed implementation of component-based models. (English) Zbl 1256.68016
Summary: Although distributed systems are widely used nowadays, their implementation and deployment are still time-consuming, error-prone, and hardly predictable tasks. In this paper, we propose a method for producing automatically efficient and correct-by-construction distributed implementations from a model of the application software in behavior, interaction, priority (BIP). BIP is a well-founded component-based framework encompassing high-level multi-party interactions for synchronizing components (e.g., rendezvous and broadcast) and dynamic priorities for scheduling between interactions. Our method transforms an arbitrary BIP model into a send/receive BIP model that is directly implementable on distributed execution platforms. The transformation consists in (1) breaking the atomicity of actions in components by replacing synchronous multiparty interactions with asynchronous send/receive interactions; (2) inserting distributed controllers that coordinate the execution of interactions according to a user-defined partition of interactions, and (3) adding a distributed algorithm for handling conflicts between controllers. The obtained send/receive BIP model is proven observationally equivalent to its corresponding initial model. Hence, all functional properties of the initial BIP model are preserved by construction in the implementation. Moreover, the obtained send/receive BIP model can be used to automatically derive distributed executable code. The proposed method is fully implemented. Currently, it is possible to generate C++ implementations for (1) TCP sockets for conventional distributed communication, (2) MPI for multi-processor platforms, and (3) POSIX threads for deployment on multi-core platforms. We present four case studies and report experimental results for different design choices including partition of interactions and choice of algorithm for distributed conflict resolution.
MSC:
| 68M14 | Distributed systems |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
Keywords:
component-based modeling; automated transformation; distributed systems; BIP; correctness-by-construction; committee coordination; conflict resolutionReferences:
| [1] | Ajtai M., Komlós J., Szemerédi E.: Sorting in c log n parallel steps. Combinatorica 3(1), 1–19 (1983) · Zbl 0523.68048 · doi:10.1007/BF02579338 |
| [2] | Arbab F.: Reo: a channel-based coordination model for component composition. Math. Struct. Comp. Sci. 14, 329–366 (2004) · Zbl 1085.68552 · doi:10.1017/S0960129504004153 |
| [3] | Bagrodia, R.: A distributed algorithm to implement n-party rendevouz. In: Foundations of Software Technology and Theoretical Computer Science, Seventh Conference (FSTTCS), pp. 138–152 (1987) · Zbl 0631.68025 |
| [4] | Bagrodia R.: Process synchronization: design and performance evaluation of distributed algorithms. IEEE Trans. Softw. Eng. (TSE) 15(9), 1053–1065 (1989) · doi:10.1109/32.31364 |
| [5] | Basu, A., Bidinger, P., Bozga, M., Sifakis, J.: Distributed semantics and implementation for systems with interaction and priority. In: Formal Techniques for Networked and Distributed Systems (FORTE), pp. 116–133 (2008) |
| [6] | Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in BIP. In: Software Engineering and Formal Methods (SEFM), pp. 3–12 (2006) |
| [7] | Batcher, K.E.: Sorting networks and their applications. In: AFIPS ’68 (Spring): Proceedings of the April 30–May 2, 1968, Spring Joint Computer Conference, pp. 307–314 (1968) |
| [8] | Bliudze, S., Sifakis, J.: A notion of glue expressiveness for component-based systems. In: Concurrency Theory (CONCUR), pp. 508–522 (2008) · Zbl 1160.68458 |
| [9] | Bonakdarpour, B., Bozga, M., Jaber, M., Quilbeuf, J., Sifakis, J.: From high-level component-based models to distributed implementations. Technical Report TR-2010-9, VERIMAG, March (2010) · Zbl 1256.68016 |
| [10] | Bonakdarpour, B., Bozga, M., Quilbeuf, J.: Automated distributed implementation of component-based models with priorities. In: ACM International Conference on Embedded Software (EMSOFT), pp. 59–68 (2011) · Zbl 1256.68016 |
| [11] | Bonakdarpour, B., Devismes, S., Petit, F.: Snap-stabilizing committee coordination. In: IEEE International Parallel and Distributed Processing Symposium (IPDPS), pp. 231–242 (2011) |
| [12] | Bozga, M., Jaber, M., Sifakis, J.: Source-to-source architecture transformation for performance optimization in BIP. In: Symposium on Industrial Embedded Systems (SIES), pp. 152–160 (2009) |
| [13] | Bozga M., Jaber M., Sifakis J.: Source-to-source architecture transformation for performance optimization in BIP. IEEE Trans. Ind. Inform. 5(4), 708–718 (2010) · doi:10.1109/TII.2010.2069102 |
| [14] | Chandy K.M., Misra J.: The drinking philosophers problem. ACM Trans. Program. Lang. Syst. (TOPLAS) 6(4), 632–646 (1984) · doi:10.1145/1780.1804 |
| [15] | Chandy K.M., Misra J.: Parallel Program Design: A Foundation. Addison-Wesley Longman Publishing Co., Inc., Boston (1988) · Zbl 0717.68034 |
| [16] | Cheiner O.M., Shvartsman A.A.: Implementing an eventuallyserializable data service as a distributed system building block. In: Principles Of Distributed Systems (OPODIS), pp. 9–24 (1998) |
| [17] | Dijkstra E.W., Scholten C.S.: Termination detection for diffusing computations. Inf. Process. Lett. 11(1), 1–4 (1980) · Zbl 0439.68039 · doi:10.1016/0020-0190(80)90021-6 |
| [18] | Galil Z., Micali S., Gabow H.N.: An o(ev log v) algorithm for finding a maximal weighted matching in general graphs. SIAM J. Comput. 15(1), 120–130 (1986) · Zbl 0589.68050 · doi:10.1137/0215009 |
| [19] | Gössler G., Sifakis J.: Composition for component-based modeling. Sci. Comput. Program. 55(1–3), 161–183 (2005) · Zbl 1075.68016 · doi:10.1016/j.scico.2004.05.014 |
| [20] | Herlihy, M., Moss, J.E.B.: Transactional memory: architectural support for lock-free data structures. In: ISCA, pp. 289–300 (1993) |
| [21] | ISO/IEC. Information Processing Systems–Open Systems Interconnection: LOTOS, A Formal Description Technique Based on the Temporal Ordering of Observational Behavior (1989) |
| [22] | Joung Y.-J., Smolka S.A.: Strong interaction fairness via randomization. IEEE Trans. Parallel Distrib. Syst. 9(2), 137–149 (1998) · doi:10.1109/71.663873 |
| [23] | Kumar, D.: An implementation of n-party synchronization using tokens. In: ICDCS, pp. 320–327 (1990) |
| [24] | Luby M.: A simple parallel algorithm for the maximal independent set problem. SIAM J. Comput. 15(4), 1036–1053 (1986) · Zbl 0619.68058 · doi:10.1137/0215074 |
| [25] | Lynch N.: Distributed Algorithms. Morgan Kaufmann, San Mateo (1996) · Zbl 0877.68061 |
| [26] | Manne F., Mjelde M., Pilard L., Tixeuil S.: A new self-stabilizing maximal matching algorithm. Theor. Comput. Sci. 410(14), 1336–1345 (2009) · Zbl 1163.68372 · doi:10.1016/j.tcs.2008.12.022 |
| [27] | Milner, R.: A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer, Berlin (1980) · Zbl 0452.68027 |
| [28] | Milner R.: Communication and Concurrency. Prentice Hall, Hertfordshire (1995) · Zbl 0683.68008 |
| [29] | Murata T.: Petri nets: Properties, analysis and applications. Proc. IEEE 77(4), 541–580 (1989) · doi:10.1109/5.24143 |
| [30] | Pérez J.A., Corchuelo R., Toro M.: An order-based algorithm for implementing multiparty synchronization. Concurr. Comput. Pract. Exp. 16(12), 1173–1206 (2004) · doi:10.1002/cpe.903 |
| [31] | Proença, J.: Synchronous Coordination of Distributed Components. PhD thesis, Faculteit der Wiskunde en Natuurwetenschappen (May 2011) |
| [32] | Shavit N., Touitou D.: Software transactional memory. Distrib. Comput. 10(2), 99–116 (1997) · Zbl 1373.68178 · doi:10.1007/s004460050028 |
| [33] | Tauber, J.A., Lynch, N.A., Tsai, M.J.: Compiling IOA without global synchronization. In: Symposium on Network Computing and Applications (NCA), pp. 121–130 (2004) |
| [34] | von Bochmann, G., Gao, Q., Wu, C.: On the distributed implementation of lotos. In: FORTE, pp. 133–146 (1989) |
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
