The workshop is an opportunity for doctoral students and young researchers working in the area of distributed systems to present their work to our highly motivated and interested audience. You can use it to test your wild new ideas, discuss work in progress, or present your accomplishments (e.g., submitted or accepted conference papers, designed systems, etc.).
We also provide space for posters in the coffee rooms.
14:20 - 14:30 Opening
14:30 - 14:45
Andrey Tabakov, Saint-Petersburg State University
Optimization of Relaxed Concurrent Priority Queues
Relaxed concurrent data structures are non-linearizable and do not provide strong operation semantics (such as FIFO/LIFO for linear lists, delete max (min) element for priority queues, etc.). We use the approach based on design of concurrent data structure as multiple simple data structures distributed among the threads. For operation execution (insert, delete), a thread randomly chooses a subset of these simple structures and make actions on them. We propose optimized relaxed concurrent priority queues based on this approach. We designed algorithms for optimization of priority queues selection for insert/delete operations and algorithm for balancing of elements in this distributed data structure.
14:45 - 15:00
Evgenii Moiseenko, Saint-Petersburg State University and JetBrains Research
Compilation correctness from event structure based weak memory model
The problem of giving a formal semantics for a weak memory model of a high-level programming language is known to be challenging. Recently, Chakraborty & Vafeiadis proposed a new solution to this problem. Their model called WeakestMO defines the semantics of a concurrent program as an event structure. The event structure is a graph, that encodes all possible executions of a program.
For a weak memory model of a programming language to be useful, several results about this model should be established. One of them is the presence of an effective compilation scheme from high-level language to the low-level assembly languages of modern hardware architectures. Chakraborty & Vafeiadis have provided only pen and paper proofs of compilation correctness for a weaker version of their model. Our work is dedicated to the mechanization of WeakestMO model, together with compilation correctness arguments, using the Coq proof assistant. We have proven the correctness of compilation to x86, ARMv8 and POWER hardware memory models, by using the IMM (intermediate memory model), a recently proposed model that abstracts over details of the hardware models.
Joint work with Anton Podkopaev and Viktor Vafeiadis
15:00 - 15:15
Egor Namakonov, Saint-Petersburg State University.
Compilation of OCaml Memory Model to IMM
The mainstream memory models such as C++ and Java MM have flaws regarding programs with data races: the former doesn't give semantics for racy programs and in the latter data races affect program execution globally. The OCaml Memory Model [Dolan-al:PLDI18] has Local DRF property which solves these problems. For the model, there are compilation correctness results to x86-TSO and ARMv8 memory models but not for POWER. We solve the problem of compilation to POWER (as well as x86 and ARM) by proving the correctness of compilation to IMM [Podkopaev-al:POPL19] - an intermediate model which already has compilation correctness proofs for various architectures. This approach is also more scalable in terms of adding new architectures.
The compilation correctness proof is formalized in Coq and is available at Github
15:15 - 15:30
Roland Schmid, ETHZ
A Permit-Based Optimistic Byzantine Ledger
PermitBFT solves the byzantine consensus problem for n nodes tolerating up to f < n/3 byzantine nodes in the partially synchronous networking model; it is the first BFT protocol to achieve an optimistic latency of just 2 message delays despite tolerating byzantine failures throughout the "fast track". The design of PermitBFT relies on two fundamental concepts. First, in PermitBFT the participating nodes do not wait for a distinguished leader to act and subsequently confirm its actions, but send permits to the next designated block creator proactively. Second, PermitBFT achieves a separation of the decision powers that are usually concentrated on a single leader node. A block creator controls which transactions to include in a new block, but not where to append the block in the block graph.
Joint work with Roger Wattenhofer
Technical report: here
15:30 - 15:45
Alexander Visheratin, ITMO University and Siemens Labs
Key words: numerical time series, big data, database, indexing, cloud computing, clusters
What is the best storage for sensor data? Database or files? What if there are decades of data from millions of sensors and it's growing? What if a user needs to search by values range or visualize any interval of data with real-time feedback? A new cloud database is being developed by the joint team of RND experts from Siemens CT (Russia) and ITMO University.
15:45 - 15:55
Yury Kuznetsov, Siemens Labs
Siemens Academic Research
We give a short overview of the research agenda of two recently created research labs supported by Siemens CT (Russia) at ITMO University and Polytechnical University.
15:55 - 16:00 Discussion and closing