Events

Upcoming events

Software for Fast Storage Hardware

Willy Zwaenepoel University of Sydney
20 Jan 2022, 10:00 am - 11:00 am
Virtual talk
SWS Distinguished Lecture Series
Storage technologies are entering the market with performance vastly superior to conventional storage devices. This technology shift requires a complete rethinking of the software storage stack.

In this talk I will give two examples of our work with Optane-based solid-state (block) devices that illustrate the need for and the benefit of a wholesale redesign.

First, I will describe the Kvell key-value (KV) store. The key observation underlying Kvell is that conventional KV software on fast devices is bottlenecked by the CPU rather than by the device. ...
Storage technologies are entering the market with performance vastly superior to conventional storage devices. This technology shift requires a complete rethinking of the software storage stack.

In this talk I will give two examples of our work with Optane-based solid-state (block) devices that illustrate the need for and the benefit of a wholesale redesign.

First, I will describe the Kvell key-value (KV) store. The key observation underlying Kvell is that conventional KV software on fast devices is bottlenecked by the CPU rather than by the device. Kvell therefore focuses on minimizing CPU intervention.

Second, I will describe the Kvell+ OLTP/OLAP system built on top of Kvell. The key underlying observation here is that these storage devices have become so fast that the conventional implementation of snapshot isolation – maintaining multiple versions – quickly leads to the device filling up. Kvell therefore focuses processes new versions as they are created.

This talk describes joint work with Oana Balmau (McGill University), Karan Gupta (Nutanix) and Baptiste Lepers (University of Sydney).

---

Please contact the MPI-SWS Office Team for the ZOOM link information. .
Read more

Recent events

Human Factors in Machine-Assisted Decision-Making

Nina Grgić-Hlača Max Planck Institute for Software Systems
18 Jan 2022, 3:00 pm - 4:00 pm
Saarbrücken building E1 4, room 029
SWS Student Defense Talks - Thesis Proposal
Machine learning (ML) based algorithms assist human decision-making in a variety of scenarios, ranging from medical diagnostics to bail decision-making. The potential societal impact of using machine decision aids in real-world settings sparked concerns about their accuracy and fairness, and inspired a flurry of research on algorithmic fairness, accountability and transparency. However, in many settings, algorithms do not make decisions, but only assist human decision-makers. In this thesis, we go beyond studying the fairness and accuracy of decision aids, ...
Machine learning (ML) based algorithms assist human decision-making in a variety of scenarios, ranging from medical diagnostics to bail decision-making. The potential societal impact of using machine decision aids in real-world settings sparked concerns about their accuracy and fairness, and inspired a flurry of research on algorithmic fairness, accountability and transparency. However, in many settings, algorithms do not make decisions, but only assist human decision-makers. In this thesis, we go beyond studying the fairness and accuracy of decision aids, and study machine-assisted human decision-making as a whole. Specifically, we study how people perceive and utilize machine decision aids.

Please contact the MPI-SWS Office Team for the ZOOM link information.
Read more

Program Logic for Weak Memory Concurrency

Marko Doko Max Planck Institute for Software Systems
07 Dec 2021, 2:00 pm - 3:00 pm
Kaiserslautern building Uni Kaiserlautern, room 48
SWS Student Defense Talks - Thesis Defense
In order to improve performance or conserve energy, modern hardware implementations have adopted weak memory models; that is, models of concurrency that allow more outcomes than the classic sequentially consistent (SC) model of execution. Modern programming languages similarly provide their own language-level memory models, which strive to allow all the behaviors allowed by the various hardware-level memory models, as well as those that can occur as a result of desired compiler optimizations.

As these weak memory models are often rather intricate, ...
In order to improve performance or conserve energy, modern hardware implementations have adopted weak memory models; that is, models of concurrency that allow more outcomes than the classic sequentially consistent (SC) model of execution. Modern programming languages similarly provide their own language-level memory models, which strive to allow all the behaviors allowed by the various hardware-level memory models, as well as those that can occur as a result of desired compiler optimizations.

As these weak memory models are often rather intricate, it can be difficult for programmers to keep track of all the possible behaviors of their programs. It is therefore very useful to have an abstraction layer over the model that can be used to ensure program correctness without reasoning about the underlying memory model. Program logics are a way of constructing such an abstraction—one can use their syntactic rules to reason about programs, without needing to understand the messy details of the memory model for which the logic has been proven sound.

Unfortunately, most of the work on formal verification in general, and program logics in particular, has so far assumed the SC model of execution. This means that new logics for weak memory have to be developed.

This thesis presents two such logics—fenced separation logic (FSL) and weak separation logic (Weasel)—which are sound for reasoning under two different weak memory models.

FSL considers the C/C++ concurrency memory model, supporting several of its advanced features. The soundness of FSL depends crucially on a specific strengthening of the model which eliminates a certain class of undesired behaviors (so-called out-of-thin-air behaviors) that were inadvertently allowed by the original C/C++ model.

Weasel works under weaker assumptions than FSL, considering a model which takes a more fine-grained approach to the out-of-thin-air problem. Weasel's focus is on exploring the programming constructs directly related to out-of-thin-air behaviors, and is therefore significantly less feature-rich than FSL.

Using FSL and Weasel, the thesis explores the key challenges in reasoning under weak memory models, and what effect different solutions to the out-of-thin-air problem have on such reasoning. It explains which reasoning principles are preserved when moving from a stronger to a weaker model, and develops novel proof techniques to establish soundness of logics under weaker models.
Read more

Semantic Congruence Closure Algorithms

Deepak Kapur University of New Mexico; Guest Researcher RG1
01 Dec 2021, 12:15 pm - 1:15 pm
Virtual talk
Joint Lecture Series
Congruence closure of ground equations is a fundamental operation used in numerous applications in computer science. Going back to the early 1960's, this operation was considered critical in recognizing common subexpressions for optimizing compilers especially for high performance computing. In the 80's, it was used to combine decision procedures for various quantifier-free theories in building verification systems. More recently, it serves as a glue in fast decision procedures based on the satisfiability modulo theory framework. In 1997, ...
Congruence closure of ground equations is a fundamental operation used in numerous applications in computer science. Going back to the early 1960's, this operation was considered critical in recognizing common subexpressions for optimizing compilers especially for high performance computing. In the 80's, it was used to combine decision procedures for various quantifier-free theories in building verification systems. More recently, it serves as a glue in fast decision procedures based on the satisfiability modulo theory framework. In 1997, an approach for generating congruence closure of uninterpreted symbols was proposed by generating a canonical rewrite system on constants by abstracting nonconstant subterms in ground equations. This framework is not only time and space efficient, but generates canonical forms with respect to the congruence closure relation. Algorithms based on this have been integrated well into SMT solvers. This talk will discuss how semantic properties of function symbols, including commutativity, idempotency, nilpotency and identity, as well as associative-commutative can also be considered without having to need any sophisticated machinery, such as associative-commutative unification, associated compatible termination orderings and associative-commutative completion, typically needed for generating canonical rewrite systems of ground equations with asssocative-commutative function symbols. The use of semantic congruence closure for generating uniform interpolants if they exist will be shown; interpolants have been found useful for automatically generating loop invariants of programs.
Read more

Archive