Annette Bieniusa
Senior researcher at TU Kaiserslautern
Annette is a lecturer and senior researcher at the Technische Universität Kaiserslautern. Her research interests include semantics of concurrent and distributed programming, with a focus on replication, synchronization, and how they are reflected on a programming language level. Annette was involved in several national and international research projects, most recently in the EU-Projects “SyncFree: Large-scale Computation without Synchronization” and “Lightkone: Lightweight computation for networks at the edge“. She is also leading the development of AntidoteDB, a transactional CRDT-key value store.
Past Activities
Code Mesh V
16.00 - 19.30
Introduction to TLA+
Concurrent and distributed programs are notoriously difficult to get right. Even tiny variations of algorithms like Peterson’s lock for mutual exclusion lead to significantly different behaviours and errors that are complex to locate.
TLA+ is a high-level language for modelling such programs and specifying their behaviour in a rigorous way. In this tutorial, you will learn how to write concurrent and distributed algorithms in PlusCal, a pseudo-code like interface for TLA+, and how to specify correctness conditions using temporal logic. We will further apply the model-checker TLC and discuss typical pitfalls when working with TLA+.
EXPERTISE
Level required to take the course
COURSE DURATION
2h 30 minutes
PREREQUISITES
Please install the TLA Toolbox on your machine by following the instructions on this page.
Code Mesh LDN 2018
13.30 - 17.00
Just the right kind of Consistency!
13:30 - 17:00
You need a data store that allows for high throughput and availability, but you are worried about the consistency of your data under concurrent updates when replicating across data centers? Current designs for data storage forces application developers to decide early in the design cycle, and once and for all, what type of consistency the database should provide.
At one extreme, data stores with strong consistency (such as Spanner and CockroachDB) require frequent global coordination; restricting concurrency in this way greatly simplifies application development, but it reduces availability and increases latency.
At the opposite extreme, there are systems like Cassandra that provide eventual consistency only: they never sacrifice availability, but application developers must write code to deal with all sorts of concurrency anomalies in order to prevent violation of application invariants. But the system just needs to be consistent enough for the application to be correct!
In the training day, we will review different approaches and tools for choosing just the right kind of consistency for your app.
OBJECTIVES
You will learn how conflict-free replicated datatypes (CRDTs), transactions, and causal consistency interact to keep your data safe. Further, you will see how to analyse your application and its invariants to obtain a provable correct model. This tutorial is hands-on with many interactive elements to explore the features and limits of the Just-Right Consistency approach.
AUDIENCE
Application developers and system developers.
Code BEAM Lite Munich 2018
14.45 - 15.25
AntidoteDB: a planet scale, highly available, transactional database
Cloud-scale applications must be highly available and offer low latency responses while serving an ever-growing number of users concurrently.
To achieve these goals, these apps rely on distributed cloud data stores that provide availability even under network partition.
It takes significant effort and expertise from programmers to understand the intricate semantics and develop correct applications on top of such highly available databases.
In my talk, I will show how AntidoteDB supports a principled approach to build highly-available, yet correct applications by combining conflict-free replicated data types (CRDTs), highly-available transactions and stronger synchronisation mechanisms.
OBJECTIVES
You will learn how conflict-free replicated datatypes (CRDTs), transactions, and causal consistency interact to keep application data safe. Further, you will see how to identify patterns in your application that have specific synchronisation requirements und learn how to employ them with AntidoteDB.
AUDIENCE
App developers that rely on datastores