Joint workshop Whisper/University of Sydney, 17th june 2019
Room 24-25/405, Lip6
The workshop is supported in part by the FASIC program by Campus France.
The goal of the workshop is to discuss on going research done as part of the CSG joint team on concurrent systems.
Talks
Baptiste Lepers, Université de Sydney
The Battle of the Schedulers: FreeBSD ULE vs. Linux CFS
This talk analyzes the impact on application performance of the design and implementation choices made in two widely used open-source schedulers: ULE, the default FreeBSD scheduler, and CFS, the default Linux scheduler. We compare ULE and CFS in otherwise identical circumstances. We have ported ULE to Linux, and use it to schedule all threads that are normally scheduled by CFS. We compare the performance of a large suite of applications on the modified kernel running ULE and on the standard Linux kernel running CFS. The observed performance differences are solely the result of scheduling decisions, and do not reflect differences in other sub-systems between FreeBSD and Linux.
There is no overall winner. On many workloads the two schedulers perform similarly, but for some workloads there are significant and even surprising differences. ULE may cause starvation, even when executing a single application with identical threads, but this starvation may actually lead to better application performance for some workloads. The more complex load balancing mechanism of CFS reacts more quickly to workload changes, but ULE achieves better load balance in the long run.
Xavier Rival, (Inria/ENS)
Abstract interpretation based static analysis
Static analysis aims at computing a conservative approximation of program semantic properties in a sound manner. As an example, it may be applied to the verification of absence of runtime errors or to the verification of the preservation of global (structural or other) invariants. Since these properties are all undecidable in general, conservative approaches maintain automation at the cost of imprecision, and may fail to compute the strongest possible properties.
In this talk, we will introduce the abstract interpretation framework in a high level and intuitive manner, and we will show two applications to
program verification. The first application focuses on safety critical embedded systems. The Astrée static analyzer computes precise invariants for a wide range of safety-critical software written in C, so as to prove the absence of runtime errors. The second application is aimed at the verification of memory safety and of the preservation of global structural invariants. The MemCAD static analysis tool provides a platform for data structures abstraction, and can be applied to structures such as arrays, lists, trees and others. We will discuss the applications of this tool to the verification of OS components in previous projects, and in the ongoing VeriAMOS ANR project.
Vincent Gramoli, Université de Sydney
Polygraph: Accountable Byzantine Agreement
In this talk, I will introduce Polygraph, the first accountable Byzantine consensus algorithm for partially synchronous systems.
If among $n$ users $t<\frac{n}{3}$ are malicious then it ensures consensus, otherwise it eventually detects malicious users that cause disagreement. Polygraph is appealing for blockchain applications as it allows them, if $t<\frac{n}{3}$, to totally order blocks in a chain, hence avoiding forks and double spending and, otherwise, to punish malicious users when a fork occurs. We first show that stronger forms of the problem including a fixed time detection are impossible to solve before proving our solution. We also show that Polygraph has a bounded justification size so that each of its asynchronous rounds exchanges only $O(n^2)$ messages. Finally, we use the Red Belly Blockchain application to evaluate Polygraph on a geodistributed system of 80 machines and show that accountability reduces the performance of the non-accountable baseline by about a third, still committing thousands of transactions per second.
Gauthier Voron, Université de Sydney
Towards scalable private blockchains
Blockchains are now a popular building block for complex distributed systems. One one side, public blockchains (e.g. Bitcoin, Ethereum) use consen sus algorithms that rely on a debatable network synchrony assumptions. On the other side, private blockchains (e.g. Hyperledger, Corda) use Byzantine Fault Tolerant consensus algorithms. These algorithms are valid in a partially synchronous network but are not ecient with more than a dozen of nodes. This talk describes how to execute eciently a BFT consensus on hundreds of nodes.
