Ballet was developed during my first postdoc to tackle the challenges faced by cross-functional DevOps teams in Edge Computing and Cyber-Physical Systems. Ballet is a fast, decentralized tool that automates choreographies for cross-DevOps reconfigurations. Each node handles its own coordination, planning, and execution, making reconfiguration seamless. Ballet's planner uses constraint programming to infer a local reconfiguration plan. However, such a plan often has consequences on depending services. Then, using a gossip protocole alongside a consensus algorithm, these consequences are formalized as constraints and propagated through the network. The execution phase of Ballet decentralizes Concerto, ensuring efficient and reliable reconfigurations across distributed systems.
SparkTE stands as a significant milestone in my Ph.D. contribution, providing a certified distributed solution for model transformation engines. Developed as a scalable distributed implementation of the CoqTL specification, SparkTE offers a versatile platform for formal reasoning and certification of model transformations. Unlike traditional approaches that prioritize certification at the expense of performance, SparkTE introduces an additional feature: a customizable engine. This aspect allows users to explore various design choices, striking the perfect balance between certification requirements and execution efficiency. With SparkTE, researchers and practitioners gain a flexible and efficient tool for navigating the complexities of model transformations with confidence.
PySke, an academic project initiated during my master's degree, is an algorithmic skeleton library for Python designed to simplify programming for shared or distributed memory parallel architectures. My contribution involved creating PySke's skeletal parallel programming patterns, particularly focusing on skeletons for lists and trees. Additionally, I contributed in the design of a lazy mechanism in PySke's execution, facilitating performance enhancement through equivalence rewriting of composition to optimize the composition of skeletons.
SyDPaCC is a collection of libraries for the Coq proof assistant enabling the transformation of high-complexity functional programs into more efficient versions, which can be parallelized and extracted into OCaml code with calls to the BSML library. During my master's degree, I contributed to SyDPaCC by formalizing map and reduce skeletons on binary trees and partially proving their correctness, enhancing the library's functionality for parallel computing.