Parity games are two-player infinite-duration games on numerically labeled

graphs, playing a crucial role in various fields of theoretical computer

science. Finding efficient algorithms to solve these games in practice is widely

acknowledged as a core problem in formal verification, as it leads, indeed, to

efficient solutions of the model-checking and satisfiability problems for

expressive temporal logics, e.g., the modal µCalculus. This problem has also an

intriguing status from a complexity theoretic viewpoint, since it belongs to the

class UPTime ∩ CoUPTime, and still open is the question whether it can be solved

in polynomial time. The solution of a parity game can be reduced to the problem

of identifying sets of positions of the game, called dominions, in each of which

a player can force a win by remaining in the set forever. In this talk, we

describe a novel technique to compute dominions, based on the idea of promoting

positions to higher priorities during the search for winning regions. The

proposed approaches have nice computational properties, exhibiting the best

space complexity among the currently known solutions. Experimental results on

both random games and benchmark families show that the technique is also very

effective in practice.

The talk is based on joint works with Massimo Benerecetti and Daniele Dell’Erba

of the Università degli Studi di Napoli Federico II.

We consider the following problem: given a dxd matrix A and two polytopes P and Q, is there a natural number n such that A^n P intersects Q. We show that the problem can be decided in PSPACE for dimension at most three. As in previous works, decidability in the case of higher dimensions is left open, as the problem is known to be hard for long-standing number-theoretic open problems.

The talk is self-contained and assumes no background from the audience. As such, the talk will include short introductions to various mathematical tools, such as representation of algebraic numbers, the theory of real-closed fields, and quantifier elimination.

Abstract:

Scheduling tasks on clusters in large-scale datacenters is challenging:

thousands of tasks must be cleverly and quickly placed to achieve good

application-level performance and high resource utilization. Centralized

datacenter schedulers can make high-quality placement decisions, but

today these high-quality placements come at the cost of high latency at

scale, which degrades response time for interactive tasks and reduces

resource utilization.

In this talk I present Firmament, a centralized scheduler that scales to

over ten thousand machines, even though it performs a computationally

expensive min-cost max-flow (MCMF) optimization that continuously

reschedules all tasks. To achieve this, Firmament automatically chooses

between different MCMF algorithms, solves the optimization problem

incrementally when possible, and applies problem-specific optimizations.

Experiments with a Google workload trace from a 12,500-machine cluster

show that Firmament places tasks in hundreds of milliseconds, and that

Firmament improves placement latency by 20x over Quincy, a prior

centralized scheduler using the same MCMF optimization. Moreover, even

though Firmament is centralized, it matches the placement latency of

distributed schedulers for workloads of short tasks. Finally, Firmament

exceeds the placement quality of four widely-used centralized and

distributed schedulers on a real-world cluster, improving batch task

response time by 6x.

Reference:

I. Gog, M. Schwarzkopf, A. Gleave, R. N. M. Watson, S. Hand. “Firmament:

Fast, Centralized Cluster Scheduling at Scale”. In Proceedings of the

12th USENIX Symposium on Operating Systems Design and Implementation

(OSDI), Savannah, GA, USA, November 2016, p. 99–115.

**[Software Testing] Hitting families of schedules**

We consider the following basic task in the testing of concurrent systems.

The input to the task is a partial order of events, which models actions performed on or by the system and specifies ordering constraints between them. The task is to determine if some scheduling of these events can result in a bug. The number of schedules to be explored can, in general, be exponential.

Empirically, many bugs in concurrent programs have been observed to have small bug depth; that is, these bugs are exposed by every schedule that orders some d specific events in a particular way, irrespective of how the other events are ordered, and d is small compared to the total number of events. To find all bugs of depth $d$, one needs to only test a d-hitting family of schedules: we call a set of schedules a $d$-hitting family if for each set of d events, and for each allowed ordering of these events, there is some schedule in the family that executes these

events in this ordering. The size of a d-hitting family may be much smaller than the number of all possible schedules, and a natural question is whether one can find $d$-hitting families of schedules that have small size.

In general, finding the size of optimal d-hitting families is hard, even for d=2. We show, however, that when the partial order is a tree, one can explicitly construct d-hitting families of schedules of small size. When the tree is balanced, our constructions are polylogarithmic in the number of events.

Correctness Witnesses: Exchanging Verification Results between Verifiers

Dirk Beyer

Paper: http://dx.doi.org/10.1145/2950290.2950351

Proc. SIGSOFT FSE 2016.

Standard verification tools provide a counterexample to witness a specification violation,

and, since a few years, such a witness can be validated by an independent validator

using an exchangeable witness format. This way, information about the violation can be shared across verification tools and the user can use standard tools to visualize and explore witnesses.

This technique is not yet established for the correctness case, where a program fulfills a specification. Even for simple programs, it is often difficult for users to comprehend why a given program is correct, and there is no way to independently check the verification result.

We close this gap by complementing our earlier work on violation witnesses with correctness witnesses. While we use an extension of the established common exchange format for violation witnesses to represent correctness witnesses, the techniques for producing and validating correctness witnesses are different. The overall goal to make proofs available to engineers is probably as old as programming itself, and proof-carrying code was proposed two decades ago —

our goal is to make it practical: We consider witnesses as first-class exchangeable objects, stored independently from the source code and checked independently from the verifier that produced them, respecting the important principle of separation of concerns.

At any time, the invariants from the correctness witness can be used to reconstruct a correctness proof to establish trust. We extended two state-of-the-art verifiers, CPAchecker and Ultimate Automizer, to produce and validate witnesses, and report that the approach is promising

on a large set of verification tasks.

Partial but Precise Loop Summarization and Its Applications

We show a symbolic-execution-based algorithm computing the precise effect of a program cycle on

program variables. For a program variable, the algorithm produces an expression representing

the variable value after the number of cycle iterations specified by parameters of the

expression. The algorithm is partial in the sense that it can fail to find such an expression

for some program variables (for example, it fails in cases when the variable value depends on

the order of paths in the cycle taken during iterations).

We present two applications of this loop summarization procedure. The first is a construction

of a nontrivial necessary condition on program input to reach a given program location. The

second application is a loop bound detection algorithm, which produces tighter loop bounds than

other approaches.

Software-defined networking (SDN) programs must simultaneously

describe static forwarding behavior and dynamic updates in response to

events. Event-driven updates are critical to get right, but

difficult to implement correctly due to the high degree of concurrency

in networks. Existing SDN platforms offer weak guarantees that can

break application invariants, leading to problems such as dropped

packets, degraded performance, and security violations. We

introduce event-driven consistent updates that are

guaranteed to preserve well-defined behaviors when transitioning

between configurations in response to events. We propose network

event structures (NESs) to model constraints on updates, such as

which events can be enabled simultaneously and causal dependencies

between events. We define an extension of the NetKAT language with

mutable state, give semantics to stateful programs using NESs, and

discuss strategies for implementing NESs in SDNs.

Finally, we evaluate our approach empirically,

demonstrating that it gives well-defined consistency guarantees while

avoiding expensive synchronization and packet buffering.

This is joint work with Jedidiah McClurg, Hossein Hojjat, and Nate Foster.

Abstract:

We present an approach to the classification of error messages in the context of static checking in the style of ESC/Java. The idea is to compute a semantics-based signature for each error message and then group together error messages with the same signature. The approach aims at exploiting modern verification techniques based on, e.g., Craig interpolation in order to generate small but significant signatures. We have implemented the approach and applied it to three benchmark sets (from Apache Ant, Apache Cassandra, and our own tool). Our experiments indicate an interesting practical potential. More than half of the considered error messages (for procedures with more than just one error message) can be grouped together with another error message.

Bio:

Martin Schäf is a Computer Scientist at SRI International. Before joining SRI, he worked at the United Nations University in Macau. He received his PhD from University of Freiburg in 2011, and his MS degree in computer science from Saarland University in 2006. His research interests include static analysis, software verification, fault localization, and GUI testing.

We study dynamic games with finite horizon. These games evolve in time and the players are able to observe and react to information during the course of the game. We assume the players have imperfect information and there can be stochastic events. The problem of finding optimal strategies is determined in many subclasses of finite dynamic games and for many game-theoretic solution concepts – including maxmin strategies or a Stackelberg equilibrium, where one player publicly commits to a strategy, to which the second player plays a best response. During the talk I will describe some of the algorithmic challenges when computing maxmin and Stackelberg strategies and our recent domain-independent algorithms that overcome these challenges.

We consider a continuous analogue of Babai et al.’s and Cai et al.’s problem of solving multiplicative matrix equations. Given k+1 square matrices A_1, …, A_k, C, all of the same dimension, whose entries are real algebraic, we examine the problem of deciding whether there exist non-negative reals t_1, …, t_k such that exp(A_1 t_1)…exp(A_kt_k) = C.

We show that this problem is undecidable in general, but decidable under the assumption that the matrices A_1,…,A_k commute. Our results have applications to reachability problems for linear hybrid automata. Our decidability proof relies on a number of theorems from algebraic and transcendental number theory, most notably those of Baker, Kronecker, Lindemann, and Masser, as well as some useful geometric and linear-algebraic results, including the Minkowski-Weyl theorem and a new (to the best of our knowledge) result about the uniqueness of strictly upper triangular matrix logarithms of upper unitriangular matrices. On the other hand, our undecidability result is shown by reduction from Hilbert’s Tenth Problem.