Design and implementation of distributed algorithms often involve many subtleties due to their complex structure, nondeterminism, and low atomicity as well as occurrence of unanticipated physical events such as faults. Thus, constructing correct distributed systems has always been a challenge and often subject to serious errors. We propose a method for generating distributed implementations from high-level component-based models that only employ simple synchronization primitives. The method is a sequence of three transformations preserving observational equivalence: (1) A transformation from a global state to a partial state model, (2) a transformation which replaces multi-party strong synchronization primitives in atomic components by point-to-point send/receive primitives based on asynchronous message passing, and (3) a final transformation to concrete distributed implementation based on platform and architecture. These transformations may use additional mechanisms ensuring mutual exclusion between conflicting interactions. We propose different distributed implementations from fully centralized to fully decentralized ones. We study the properties of different transformations, in particular, performance criteria such as degree of parallelism and overhead for coordination. In our case studies, we observe that different types of distributed and parallel algorithms may significantly behave differently in terms of performance under different types of transformations.Bio:
Borzoo Bonakdarpour is currently a post-doctoral researcher at the Verimag Laboratory in Grenoble, France. His main focus is on the BIP project led by Joseph Sifakis. The aim of the project is to develop theory, methods, and tools for building real-time and distributed systems consisting of heterogeneous components. His other research interests include compositional verification of embedded systems, program synthesis and, in particular, program revision. He is the main developer of the tool SYCRAFT which is capable of synthesizing fault-tolerant distributed programs of the size 1080 reachable states and beyond. Borzoo Bonakdarpour obtained his Ph.D. from the Department of Computer Science and Engineering at Michigan State University in 2008 where he joined as a Master's student in 2002. His Ph.D. dissertation, "Automated Revision of Distributed and Real-Time Programs", studies a wide range of revision problems in closed an open systems. He completed his Bachelor of Science in computer engineering at The University of Esfahan, Iran, in 1998. His B. Sc. project on queuing theoretic analysis and implementation of voice over Ethernet won the President of Iran Khawrazmi Research Prize.