Events 2018

Algorithms and the Brain

Emanuele Natale
MPI-INF - D1
Joint Lecture Series
01 Aug 2018, 12:15 pm - 1:15 pm
Saarbrücken building E1 5, room 002
Around the mid of the 20th century, pioneering theoreticians of brain science and computer science such as von Neumann, Turing, McCulloch, Pitts and Barlow, were beginning to leverage their interests in the other field to gain a better understanding of their own. These two fields have since then rapidly grown their prestige as sciences, as they became more sophisticated and their body of knowledge expanded. However, in doing so, they have also grown further apart. In this talk I will outline some recent efforts from both research communities to recognize the potential for what could be achieved in a unified research effort to answer the question: "What are the algorithms which run our brain?"

Practical Program Analysis

Maria Christakis
Max Planck Institute for Software Systems
Joint Lecture Series
04 Jul 2018, 12:15 pm - 1:15 pm
Saarbrücken building E1 5, room 002
Sound static analysis over-approximates the set of all possible executions in a given program in order to prove the absence of errors in the program. Due to this over-approximation, sound static analysis may generate spurious warnings about executions that are not wrong or even possible in the program. To become more practical, many static analyzers give up soundness by design. This means that they do not check certain properties or that they check them under certain unsound assumptions, such as the absence of arithmetic overflow. At the other end of the soundness spectrum, we have automatic test-case generation, which typically under-approximates the set of possible program executions. The goal of test-case generation is not to prove the absence of errors in the program but, rather, their existence. In this talk, I will present an overview of my research on combining these program analysis techniques to improve their overall automation, performance, and accuracy on real programs.

The Internet: A Complex System at its Limits

Anja Feldmann
MPI-INF - INET
Joint Lecture Series
06 Jun 2018, 12:15 pm - 1:15 pm
Saarbrücken building E1 5, room 002
tbd

Capturing and Learning Digital Humans

Gerard Pons-Moll
MPI-INF - D2
Joint Lecture Series
02 May 2018, 12:15 pm - 1:15 pm
Saarbrücken building E1 5, room 002
tbd

Power to the People. Verified.

Holger Hermanns
Fachrichtung Informatik - Saarbrücken
Joint Lecture Series
11 Apr 2018, 12:15 pm - 1:15 pm
Saarbrücken building E1 5, room 002
Twenty years ago we were able to repair cars at home. Nowadays customer services repair coffee machines by installing software updates. Soon you will no longer be able to repair your bike.

Embedded software innovations boost our society; they help us tremendously in our daily life. But we do not understand what the software embedded therein actually does, regardless of how well educated or smart we are. Proprietary embedded software has become an opaque layer between functionality and user. That layer is thick enough to possibly induce malicious or unintended behaviour, as it happened massively in our diesel cars. From the outside, there is no understanding of how decisions are made inside and across these software-driven black boxes. The outcomes are often not designed to be accessible, verified or evaluated by humans, limiting our ability to identify if, when, where, and why the software produced harm -- and worse still -- redress this harm. Proprietary embedded software locks us out of the products we own.

The presentation of Holger Hermanns will sketch the main cornerstones of a research agenda which targets the foundations of open and hence customisable embedded software. A minor customisation might well have strong unexpected impact, for instance on the longevity of an embedded battery, or the safety of the battery charging process. Means to detect, quantify and prevent such implications are needed. Those are delivered by quantitative verification technology for system-level correctness, safety, dependability and performability. Hermanns will link foundational achievements to concrete results in the area of power management for electric mobility and for satellite operation. Electric power is intricate to handle by software, is safety-critical, but vital for mobile devices and their longevity. Since ever more tools, gadgets, and vehicles run on batteries and use power harvesting, electric power management is itself a pivot of the future.

Lovasz meets Weisfeiler-Leman

Prof. Martin Grohe
RWTH Aachen University
SWS Colloquium
04 Apr 2018, 10:30 am - 11:30 am
Kaiserslautern building G26, room 111
I will speak about an unexpected correspondence between a beautiful theory, due to Lovasz, about homomorphisms and graph limits and a popular heuristic for the graph isomorphism problem known as the Weisfeiler-Leman algorithm. I will also relate this to graph kernels in machine learning. Indeed, the context of this work is to desgin and understand similarity measures between graphs and discrete structures.

Failures-In-Time (FIT) Analysis for Fault-Tolerant Distributed Real-Time Systems

Arpan Gujarati
Max Planck Institute for Software Systems
SWS Student Defense Talks - Thesis Proposal
28 Mar 2018, 4:00 pm
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
Distributed real-time (DiRT) systems are widely deployed in contemporary cyber-physical systems (CPS). Many of these systems are safety-critical, since their failure or malfunction can result in death or serious injuries to the people and/or severe damage to the environment involved, e.g., human spaceflight vehicles, surgical robots, air traffic and nuclear reactor control systems, drive-by-wire and fly-by-wire systems, railway signaling systems, etc.

Safety-certification standards mandate that the failure rate of safety-critical systems in the presence of any unpreventable and intolerable errors due to environmentally-induced transient faults (such as due to electromagnetic, thermal, and radiation sources) must be under a certain threshold.

In this regard, prior work on the reliability analysis of DiRTs in the presence of environmentally-induced transient faults does not target all possible error scenarios (such as Byzantine errors). This is mainly because the likelihood of a complex error scenario is extremely low and/or because the workloads for safety-critical systems have traditionally been simple, with sufficient slack to tolerate fault-induced failures and with mechanical backups to tolerate complete software failures.

However, a majority of CPS devices are expected to be fully autonomous in future, thus requiring stronger reliability guarantees with fail-operational semantics. In addition, since the workloads used for safety-critical systems are becoming more and more complex (e.g., deep learning neural networks are being used in self-driving cars) and since there is a push towards the use of cheaper community hardware, the likelihood of complex Byzantine errors is going to increase. Therefore, it is imperative that we revisit the existing techniques for analyzing and building safety-critical DiRTs.

To address this issue, we propose analyses to derive a safe upper-bound on the failure rates of safety-critical DiRTs in the presence of Byzantine errors due to environmentally-induced transient faults. We focus on DiRTs based on Controller Area Network that are commonly used in today's cyber-physical systems, and on Ethernet-based DiRTs that are expected to be at the core of next-generation cyber-physical systems.

High-Throughput and Predictable VM Scheduling for High-Density Workloads

Manohar Vanga
Max Planck Institute for Software Systems
SWS Student Defense Talks - Thesis Proposal
26 Mar 2018, 3:00 pm
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
In the increasingly competitive public-cloud marketplace, improving the efficiency of data centers is a major concern. One way to improve efficiency is to consolidate as many virtual machines (VMs) onto as few physical cores as possible, provided that customers' performance expectations are not violated. However, as a prerequisite for supporting increased VM densities, the hypervisor's VM scheduler must allocate processor time efficiently and in a timely fashion. Unfortunately, we show that contemporary VM schedulers leave substantial room for improvements in both regards when facing challenging high-VM-density workloads that frequently trigger the VM scheduler.

We identify the root causes of this inability to support high-density VM scenarios to be (i) high runtime overheads and (ii) unpredictable scheduling heuristics. To better support high VM densities, we propose Tableau, a VM scheduler that guarantees a minimum processor share and a maximum bound on scheduling delay for every VM in the system. Tableau achieves this by combining a low-overhead, core-local, table-driven dispatcher within the hypervisor with a fast on-demand table-generation procedure (triggered asynchronously upon VM creation and teardown) that employs scheduling techniques typically used in hard real-time systems.

In an evaluation comparing Tableau against three current Xen schedulers on a 16-core Intel Xeon machine, Tableau is shown to improve both tail latency (e.g., a 17x reduction in maximum ping latency compared to Credit, Xen's default scheduler) and throughput (e.g., 1.6x peak web server throughput compared to Xen's real-time RTDS scheduler when serving 1 KiB files with a 100 ms SLA). While Tableau solves one piece of the unpredictability puzzle, namely the VM scheduler, there are other sources of unpredictability that arise in a shared, high-density setting. We therefore propose extensions of Tableau to deal with two other major sources of unpredictability: LLC interference caused by other VMs co-located on the same CPU socket, and delays that arise due to I/O scheduling.

Data Science for Human Well-being

Tim Althoff
Stanford University
SWS Colloquium
26 Mar 2018, 10:30 am - 11:30 am
Saarbrücken building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
The popularity of wearable and mobile devices, including smartphones and smartwatches, has generated an explosion of detailed behavioral data. These massive digital traces provide us with an unparalleled opportunity to realize new types of scientific approaches that provide novel insights about our lives, health, and happiness. However, gaining valuable insights from these data requires new computational approaches that turn observational, scientifically "weak" data into strong scientific results and can computationally test domain theories at scale. In this talk, I will describe novel computational methods that leverage digital activity traces at the scale of billions of actions taken by millions of people. These methods combine insights from data mining, social network analysis, and natural language processing to generate actionable insights about our physical and mental well-being. Specifically, I will describe how massive digital activity traces reveal unknown health inequality around the world, and how personalized predictive models can target personalized interventions to combat this inequality. I will demonstrate that modelling how fast we are using search engines enables new types of insights into sleep and cognitive performance. Further, I will describe how natural language processing methods can help improve counseling services for millions of people in crisis. I will conclude the talk by sketching interesting future directions for computational approaches that leverage digital activity traces to better understand and improve human well-being.

CANCELLED: Human-Centric Tools for Software Maintenance

Austin Henley
University of Memphis
SWS Colloquium
22 Mar 2018, 1:30 pm - 2:30 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
All software failures are fundamentally the fault of humans--either the design was ill-formed or the implementation contained a bug. By designing more human-centric development tools, developers can produce higher quality code in less time with lower cognitive load. In this talk, I will present tools for supporting two common activities in software maintenance: code navigation and code reviewing. Since navigating code is known to be time consuming and problematic, I designed Patchworks, a novel code editor interface that enables efficient juxtaposition and rapid scanning of code. Two empirical studies found that developers using Patchworks navigated faster and made fewer navigation mistakes than with traditional code editors. Once developers have made changes to the code, other developers must review and discuss the changes to ensure the code is of sufficient quality. To aid developers in this tedious task of reviewing code, I designed CFar, an automated code reviewer that provides feedback using program analysis. A laboratory study and field deployment involving 98 developers at Microsoft found that using CFar increased communication, productivity, and review quality.

Characterizing the Space of Adversarial Examples in Machine Learning

Nicolas Papernot
Pennsylvania State University
SWS Colloquium
22 Mar 2018, 10:30 am - 12:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
There is growing recognition that machine learning (ML) exposes new security and privacy vulnerabilities in software systems, yet the technical community's understanding of the nature and extent of these vulnerabilities remains limited but expanding. In this talk, I explore the threat model space of ML algorithms, and systematically explore the vulnerabilities resulting from the poor generalization of ML models when they are presented with inputs manipulated by adversaries. This characterization of the threat space prompts an investigation of defenses that exploit the lack of reliable confidence estimates for predictions made. In particular, we introduce a promising new approach to defensive measures tailored to the structure of deep learning. Through this research, we expose connections between the resilience of ML to adversaries, model interpretability, and training data privacy.

Catch-22: Isolation and Efficiency in Datacenters

Mihir Nanavati
UBC
SWS Colloquium
19 Mar 2018, 10:30 am - 11:30 am
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
The datacenters behind popular cloud services are extremely resource-dense. A typical deployment has thousands of cores, terabytes of memory, gigabits of bandwidth, and petabytes of storage available per-rack. Datacenter economics require that providers share these resources across multiple customers for efficient utilization and as a means of providing price-competitive offerings. Shared infrastructure, however, risks cross-client interference and can result in degraded performance or data leaks, leading to outages and breaches. My work explores this tension with systems that provide security and performance isolation on shared hardware, while enabling efficient utilization and preserving the underlying performance of the devices.

This talk describes two such systems dealing with different resources: the first, Plastic, transparently mitigates poor scalability on multi-core systems caused by insufficient cache line isolation, which results in unnecessary memory contention and wasted compute cycles. Another one, Decibel, provides isolation in shared non-volatile storage and allows clients to remotely access high-speed devices at latencies comparable to local devices while guaranteeing throughput, even in the face of competing workloads.

Static Program Analysis for a Software-Driven Society

Dr. Caterina Urban
ETH Zurich
SWS Colloquium
15 Mar 2018, 10:30 am - 12:00 pm
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
As we rely more and more on computer software for automating processes and making decisions, the range of software that is considered critical goes well beyond the avionics and nuclear power industries: nowadays software plays an increasingly important role in convicting criminals, trading on the financial markets, autonomously driving cars, and performing medical diagnoses, to name a few applications. It is now paramount to ensure the reliability and security of such software, and expectations about software fairness and transparency are rapidly rising. To meet these needs, we need new mathematical models of software behavior that capture the aspects relevant for a particular dependability property, and new algorithmic approaches to effectively navigate this mathematical space and decide whether the software behaves as desired. This talk gives an overview of the steps I have taken towards addressing these challenges. Starting from a series of works on deciding software termination, I show that the insights from this domain are transferable to other formal methods and properties. These results pave the way for a unified framework for deciding increasingly advanced software dependability properties. I discuss the first results that I obtained in this more general direction, which in particular bring new conceptual clarity to the synergies with deciding security properties of software. Finally, I conclude with an outlook to the future and discuss the potential impact of this research on our personal, civic, and economic life.

Language Support for Distributed Systems in Scala

Heather Miller
Northeastern University and EPFL
SWS Colloquium
12 Mar 2018, 10:30 am - 12:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
Recent years have seen a rise in distributed systems for interactive, large-scale data processing. Cutting-edge systems focus on reducing latency and increasing expressiveness in order to provide an interactive and rich experience to more and varied users coming from emerging fields such as data science. Meanwhile, the languages and runtimes underlying such systems face numerous challenges in the context of the severely demanding needs of these new distributed systems; popular languages and runtimes like Scala and the JVM (a) limit the customizability of fundamental operations like serialization, and (b) expose low-level distribution-related errors to application developers and end users when trying to distribute core language features, such as functions. This talk presents three systems that (a) give more control over these primitives to distributed systems builders thereby enabling important optimizations, and (b) increase the reliability of distributing functions and objects. Theoretical, experimental, and empirical results are used in the validation of our work.

Self-aware Computing: Combining Learning and Control to Manage Complex, Dynamic Systems

Dr. Hank Hoffmann
University of Chicago
SWS Colloquium
08 Mar 2018, 10:30 am - 12:00 pm
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
Modern computing systems must meet multiple---often conflicting---goals; e.g., high-performance and low energy consumption. The current state-of-practice involves ad hoc, heuristic solutions to such system management problems that offer no formally verifiable behavior and must be rewritten or redesigned wholesale as new computing platforms and constraints evolve. In this talk, I will discuss my research on building self-aware computing systems that address computing system goals and constraints in a fundamental way, starting with rigorous mathematical models and ending with real software and hardware implementations that have formally analyzable behavior and can be re-purposed to address new problems as they emerge.

These self-aware systems are distinguished by awareness of user goals and operating environment; they continuously monitor themselves and adapt their behavior and foundational models to ensure the goals are met despite the challenges of complexity (diverse hardware resources to be managed) and dynamics (unpredictable changes in input workload or resource availability). In this talk, I will describe how to build self-aware systems through a combination of machine learning and control theoretic techniques. I will then show how this combination enables new capabilities, like increasing system robustness, reducing application energy, and meeting latency requirements even with no prior knowledge of the application.

Incorporating Positional and Contextual Information into a Neural IR Model

Andrew Yates
MPI-INF - D5
Joint Lecture Series
07 Mar 2018, 12:15 pm - 1:15 pm
Saarbrücken building E1 5, room 002
Ad-hoc information retrieval models consider query-document interactions to produce a document relevance score for a given query and document. Traditionally, such interactions have been modeled using handcrafted statistics that generally count term occurrences within a document and across a collection. Recently, neural models have demonstrated that they provide the instruments necessary to consider query-document interactions directly, without the need for engineering such statistics.

In this talk, I will describe how positional term information can be represented and incorporated into a neural IR model. The resulting model, called PACRR, performs significantly better on standard TREC benchmarks than previous neural approaches. This improvement can be attributed to the fact that PACRR can learn to match both ordered and unordered sequences of query terms in addition to the single term matches considered by prior work. Using PACRR's approach to modeling query-document interactions as a foundation, I will describe how several well-known IR problems can be addressed by incorporating contextual information into the model; the resulting Co-PACRR model significantly outperforms the original PACRR model. Finally, I will provide a brief look inside the model to illustrate the interpretability of the learned weights and to investigate how match signals are combined by the model to produce a query-document relevance score.

Observing and Controlling Distributed Systems with Cross-Cutting Tools

Jonathan Mace
Brown University
SWS Colloquium
05 Mar 2018, 10:30 am - 12:00 pm
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
Distributed systems represent some of the most interesting and successful computing applications in use today, from modern web applications and social networks, to data analytics and large-scale machine learning.  However, it is notoriously difficult to understand, troubleshoot, and enforce distributed systems behaviors, because unlike standalone programs, they lack a central point of visibility and control.  This impacts important tasks like resource management, performance, security, accounting, and more.  In this talk I will outline techniques and abstractions for re-establishing cross-component visibility and control.  I will demonstrate with two cross-cutting tools that I have developed in my research: Retro, which measures resource usage and co-ordinates scheduler parameters to achieve end-to-end performance goals; and Pivot Tracing, which dynamically monitors and correlates metrics across component boundaries.  Together, these tools illustrate some of the common challenges and potential solutions when developing and deploying tools for distributed systems.

Storage mechanisms and finite-state abstractions for software verification

Georg Zetzsche
Université Paris-Diderot
SWS Colloquium
01 Mar 2018, 10:30 am - 11:30 am
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
A popular approach to automatic program verification is to come up with an abstraction that reflects pertinent properties of the program. This abstraction is drawn from a class of formal models that is amenable to analysis. In the plethora of existing formal models, the aspects of programs that can be represented faithfully are typically determined by the infinite dimension of its state space, its storage mechanism. A central theme of my recent research is to obtain general insights into how the structure of the storage mechanism affects the analysis of a formal model. In the first part of my talk, I will survey results on an overarching framework of storage mechanisms developed in my doctoral work. It encompasses a range of infinite-state models and permits meaningful characterizations of when a particular method of analysis is applicable. Another current focus of my work concerns finite-state abstractions of infinite-state models. On one hand, these can be over- or under-approximations that are more efficient to analyze than infinite-state systems. On the other hand, they can serve as easy-to-check correctness certificates that are produced instead of yes-or-no answers to a verification task. Thus, the second part of my talk will be concerned with results on computing downward closures and related finite-state abstractions.

Fighting Large-scale Internet Abuse

Kevin Borgolte
University of California, Santa Barbara
SWS Colloquium
26 Feb 2018, 10:30 am - 12:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
The widespread access to the Internet and the ubiquity of web-based services make it easy to communicate and interact globally. Unfortunately, the software implementing the functionality of these services is often vulnerable to attacks. In turn, an attacker can exploit them to compromise and abuse the services for nefarious purposes. In my research, I aim to better understand, detect, and prevent these attacks.

In this talk, we first look at detecting website defacements, which can inflict significant harm on a website's owner or operator through the loss of sales, the loss in reputation, or because of legal ramifications. Then, we dive into how to automatically identify malware distribution campaigns, which has become a major challenge in today's Internet. Next, we look at how to mitigate the dangers of domain takeover attacks, which give attackers the same capabilities to spread misinformation or malware as vulnerabilities do, but without the actual need for a vulnerability in the affected service. Last, I will conclude by sketching interesting future directions on how to better understand, detect, and prevent Internet abuse.

High Performance Data Center TCP Packet Processing

Antoine Kaufmann
University of Washington
SWS Colloquium
19 Feb 2018, 10:30 am - 11:30 am
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
TCP is widely used for client-server communication in modern data centers. But TCP packet handling is notoriously CPU intensive, accounting for an increasing fraction of data center processing time. Techniques such as TCP segment offload, kernel bypass, and RDMA are of limited benefit for the typical small, frequent RPCs. These techniques can also compromise protocol agility, resource isolation, overall system reliability, and complicate multi-tenancy.

I propose a unique refactoring of TCP functionality that splits processing between a streamlined fast path for common operations, and an out-of-band slow path. Protocol processing executes in the kernel on dedicated cores that enforce correctness and resource isolation. Applications asynchronously communicate with the kernel through event queues, improving parallelism and cache utilization. I show that my approach can increase RPC throughput by up to 4.1x compared to Linux. The fast-path can be offloaded to a programmable NIC to further improve performance and minimize CPU time for network processing. With hardware offload, data packets are delivered directly from application to application, while the NIC and kernel cooperate to enforce correctness and resource isolation. I show that hardware offload can increase per-core packet throughput by 10.7x compared to the Linux kernel TCP implementation.

Towards Latency Guarantees in Datacenters

Keon Jang
Google
SWS Colloquium
15 Feb 2018, 10:30 am - 12:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
A large portion of computation is now carried out in datacenter. A single datacenter hosts several 100s or 1000s of applications which share common compute and network resources in a datacenter. Isolating each application's performance, i.e., ensuring that its performance is predictable regardless of the behavior of other applications is essential to developing and deploying data center applications, since otherwise developers need to account for co-located applications, which increases development and deployment complexity. Despite its importance current approaches to performance isolation are incomplete, and focus mostly on isolating computational resources. In this talk I present two schemes for isolation network performance. The first, Silo, takes a resource allocation based approach and implements mechanisms for guaranteeing an application's network latency and throughput. The second, Express Pass, takes a congestion control based approach and fairly partitions network resources across applications.  Both approaches require no hardware (ASIC) changes, and can be deployed in today's datacenter. This shows that full application performance isolation is achievable today.

Liquid Haskell: Usable Language-Based Program Verification

Niki Vazou
University of Maryland
SWS Colloquium
12 Feb 2018, 10:30 am - 12:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
Formal verification has been gaining the attention and resources of both the academic and the industrial world since it prevents critical software bugs that cost money, energy, time, and even lives. Yet, software development and formal verification are decoupled, requiring verification experts to prove properties of a template - instead of the actual - implementation ported into verification specific languages. My goal is to bridge formal verification and software development for the programming language Haskell. Haskell is a unique programming language in that it is a general purpose, functional language used for industrial development, but simultaneously it stands at the leading edge of research and teaching welcoming new, experimental, yet useful features.

In this talk I am presenting Liquid Haskell, a refinement type checker in which formal specifications are expressed as a combination of Haskell's types and expressions and are automatically checked against real Haskell code. This natural integration of specifications in the language, combined with automatic checking, established Liquid Haskell as a usable verifier, enthusiastically accepted by both industrial and academic Haskell users. Recently, I turned Liquid Haskell into a theorem prover, in which arbitrary theorems about Haskell functions would be proved within the language. As a consequence, Liquid Haskell can be used in Haskell courses to teach the principles of mechanized theorem proving.   

Turning a general purpose language into a theorem prover opens up new research questions - e.g., can theorems be used for runtime optimizations of existing real-world applications? - that I plan to explore in the future.

Scalable positioning of commodity mobile devices using audio signals

Viktor Erdélyi
Max Planck Institute for Software Systems
SWS Student Defense Talks - Thesis Proposal
09 Feb 2018, 4:00 pm - 4:45 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
This thesis explores the problem of computing a position map for co-located mobile devices without local infrastructure. The capability to obtain a position map can, for instance, aid spontaneous and private communication among users based on their relative position (e.g., in a given section of a room, at the same table, or in a given seat) at events like meetings, talks, or conferences. It can also facilitate interaction between speaker and audience in a lecture hall, and enable the distribution of materials and the collection of feedback based on users' location. In this thesis, we first present Sonoloc, a mobile app and system that, by relying on acoustic signals, allows a set of co-located commodity smart devices to determine their relative positions without local infrastructure. Sonoloc can position any number of devices within acoustic range with a constant number of chirps emitted by a self-organized subset of devices. Our experimental evaluation shows that the system can locate up to hundreds of devices with an accuracy of tens of centimeters using no more than 15 acoustic signals emitted by dynamically selected devices, in realistic rooms and despite substantial background noise. Then, we also discuss two planned extensions to Sonoloc: (1) one that enables users to determine the correct orientation of the position map while also allowing per-user choices, and (2) one that enables the creation of a combined relative position map in meetings that span multiple locations over videoconference.

Caribou -- Intelligent Distributed Storage for the Datacenter

Zsolt Istvan
ETH Zurich
SWS Colloquium
08 Feb 2018, 10:30 am - 12:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
In the era of Big Data, datacenter and cloud architectures decouple compute and storage resources from each other for better scalability. While this design choice enables elastic scale-out, it also causes unnecessary data movements. One solution is to push parts of the computation down to storage where data can be filtered more efficiently. Systems that do this are already in use and rely either on regular server machines as storage nodes or on network attached storage devices. Even though the former provide complex computation and rich functionality since there are plenty of conventional cores available to run the offloaded computation, this solution is quite inefficient because of the over-provisioning of computing capacity and the bandwidth mismatches between storage, CPU, and network.  Networked storage devices, on the other hand, are better balanced in terms of bandwidth but at the price of offering very limited options for offloading data processing.

With Caribou, we explore an alternative design that offers rich offloading functionality while matching the available line-rate processing performance of either storage or network. It also does this in a much more efficient package (size, energy consumption) than regular servers. Our FPGA-based prototype system has been designed such that the internal data management logic can saturate the network for most operation mixes, without being over-provisioned. As a result, it can extract and process data from storage at multi-GB/s rate before sending it to the computing nodes, while at the same time offering features such as replication for fault-tolerance.

Caribou has been released as open source. Its modular design and extensible processing pipeline make it a convenient platform for exploring domain-specific processing inside storage nodes.

Relational Cost Analysis

Ezgi Çiçek
Max Planck Institute for Software Systems
SWS Student Defense Talks - Thesis Defense
22 Jan 2018, 4:00 pm - 5:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
Programming languages research has made great progress towards statically estimating the execution cost of a program. However, when one is interested in how the execution costs of two programs compare to each other (i.e., relational cost analysis), the use of unary techniques does not work well in many cases. In order to support a relational cost analysis, we must ultimately support reasoning about not only the executions of a single program, but also the executions of two programs, taking into account their similarities. This dissertation makes several contributions to the understanding and development of such a relational cost analysis. It shows how: 1) Refinement types and effect systems can express functional and relational quantitative properties of pairs of programs, including the difference in execution costs; 2) Relational cost analysis can be adapted to reason about dynamic stability, a measure of the update times of incremental programs as their inputs change; and 3) A sound and complete bidirectional type system can be developed (and implemented) for relational cost analysis.