Fedor Ryabinin, PhD Student, IMDEA Software Institute
Cloud services improve their availability by replicating data across sites in different geographical regions. A variety of state-machine replication protocols have been proposed for this setting that reduce the latency under workloads with low contention. However, when contention increases, these protocols may deliver lower performance than well-known Paxos algorithm. In this talk I will present SwiftPaxos – a protocol that lowers the best-case latency in comparison to Paxos without hurting the worst-case one. SwiftPaxos executes a command in a single round trip if there is no contention, and in 1.5 round trips otherwise. Differently from previous protocols, SwiftPaxos permits a replica to vote twice: first for its own proposal, and then to follow the leader. This mechanism avoids restarting the voting process when a disagreement occurs among replicas, saving computation time and message delays. This is joint work with Alexey Gotsman (IMDEA Software Institute) and Pierre Sutra (Télécom SudParis).
Alejandro Aguirre, PhD Researcher, IMDEA Software Institute
Sensitivity properties describe how changes to the input of a program affect the output, typically by upper bounding the distance between the outputs of two runs by a monotone function of the distance between the corresponding inputs. When programs are probabilistic, the distance between outputs is a distance between distributions. The Kantorovich lifting provides a general way of defining a distance between distributions by lifting the distance of the underlying sample space; by choosing an appropriate distance on the base space, one can recover other usual probabilistic distances, such as the Total Variation distance. We develop a relational pre-expectation calculus to upper bound the Kantorovich distance between two executions of a probabilistic program. We illustrate our methods by proving algorithmic stability of a machine learning algorithm, convergence of a reinforcement learning algorithm, and fast mixing for card shuffling algorithms. We also consider some extensions: proving lower bounds on the Total Variation distance and convergence to the uniform distribution. Finally, we describe an asynchronous extension of our calculus to reason about pairs of program executions with different control flow.
Kyveli Doveri, PhD Student, IMDEA Software Institute
We present a novel algorithmic framework to decide whether inclusion holds between ω-regular languages of infinite words over a finite alphabet. Our approach relies on a least fixpoint characterization of languages based on ultimately periodic infinite words of type uvω, with u finite prefix and v finite period of the word. Our inclusion checking algorithm, called BAInc, is designed as a complete abstract interpretation that performs a least fixpoint computation on a suitable abstraction of sets of finite words. This abstraction is canonically defined through a pair of well-quasiorder relations on finite prefixes and periods of words. We implemented BAInc in Java as a tool called BAIT. We experimentally evaluated BAIT on an extensive suite of benchmarks and performed a comparison with state-of-the-art language inclusion checking tools. The experimental results show that BAIT advances the state-of-the-art of language inclusion tools.