CS Talks - Filip Niksic (2pm), Marko Doko (2:30pm), MPI-SWS, Germany

Event time: 
Tuesday, January 16, 2018 - 2:00pm to 4:00pm
Event description: 

CS Talk #1

Speaker: Filip Niksic (2:00 p.m.)

Title: Why is Random Testing Effective for Partition Tolerance Bugs?

Host: Ruzica Piskac

Abstract:

Random testing has proven to be an extremely effective way to catch subtle bugs in distributed systems in the presence of network partition faults. This is surprising, as the space of potentially faulty executions is enormous, and the bugs depend on a subtle interplay between sequences of operations and faults.

We provide a theoretical justification of the effectiveness of random testing in this context. First, we show a general construction, using the probabilistic method from combinatorics, that shows that whenever a random test covers a fixed coverage goal with sufficiently high probability, there is a small set of random tests which achieves full coverage with high probability. In particular, we show that our construction can give test sets exponentially smaller than systematic enumeration. Second, based on an empirical study of many bugs found by random testing in production distributed systems, we introduce notions of test coverage relating to network partition faults which are effective in finding bugs. Finally, we show using combinatorial arguments that for these notions of test coverage we introduce, we can find a lower bound on the probability that a random test covers a given goal. Our general construction then explains why random testing tools achieve good coverage—and hence, find bugs—quickly.

While we formulate our results in terms of network partition faults, our construction provides a step towards rigorous analysis of random testing algorithms. We demonstrate that several other random testing approaches in the literature can be explained using our main result.

Bio:

Filip Niksic is a doctoral student at the Max Planck Institute for Software Systems (MPI-SWS) in Kaiserslautern, Germany. His research interests broadly lie in the analysis, verification, and testing of concurrent systems.

CS Talk # 2

Speaker: Marko Doko (2:30 p.m.)

Title: A Separation Logic for Promising Semantics

Host: Ruzica Piskac

Abstract:

We present the first expressive program logic for reasoning about concurrent programs under a weak memory model addressing the out-of-thin-air problem. Our logic includes the standard features from existing logics, such as RSL and GPS, that were previously known to be sound only under stronger memory models: (1) separation, (2) per-location invariants, and (3) ownership transfer via release-acquire synchronisation—as well as novel features for reasoning about (4) the absence of out-of-thin-air behaviours and (5) coherence. The logic is proved sound over the recent “promising” memory model of Kang et al., using a substantially different argument to soundness proofs of logics for simpler memory models.

This is a joint work with Kasper Svendsen, Jean Pichon-Pharabod, Ori Lahav, and Viktor Vafeiadis.

Bio:

Marko Doko is a PhD student at MPI-SWS in Kaiserslautern, Germany. He is working with Viktor Vafeiadis in the area of programming languages and verification. His current research focus is on weak memory models, and program logics for reasoning about weak memory concurrency.