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.
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
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.
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
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.
We consider data automata in the form of finite automata equipped with variables (counters or registers) ranging over infinite data domains. A trace of such a data automaton is an alternating sequence of alphabet symbols and values taken by the counters during an execution of the automaton. We address the problem of checking the inclusion between the sets of traces (data languages) recognized by such automata. Since the problem is undecidable in general, we give a semi-algorithm based on abstraction refinement, which is proved to be sound and complete modulo termination. Due to the undecidability of the trace inclusion problem, our procedure is not guaranteed to terminate. We have implemented our technique in a prototype tool and show promising results on several non-trivial examples.
Unsatisfiability proofs in the DRAT format became the de
facto standard to increase the reliability of contemporary SAT solvers.
We consider the problem of generating proofs for the XOR reasoning
component in SAT solvers and propose two methods: direct translation
transforms every XOR constraint addition inference into a DRAT proof,
whereas T-translation avoids the exponential blow-up in direct transla-
tions by using fresh variables. T-translation produces DRAT proofs from
Gaussian elimination records that are polynomial in the size of the input
CNF formula. Experiments show that a combination of both approaches
with a simple prediction method outperforms the BDD-based method.
Security vulnerabilities plague modern systems because writing secure systems code is hard. Promising approaches can retrofit security automatically via runtime checks that implement the desired security policy; these checks guard critical operations, like memory accesses. Alas, the induced slowdown usually exceeds by a wide margin what system users are willing to tolerate in production, so these tools are hardly ever used. As a result, the insecurity of real-world systems persists. We present an approach in which developers/operators can specify what level of overhead they find acceptable for a given workload (e.g., 5%); our proposed tool ASAP then automatically instruments the program to maximize its security while staying within the specified “overhead budget.” Two insights make this approach effective: most overhead in existing tools is due to only a few “hot” checks, whereas the checks most useful to security are typically “cold”and cheap. We evaluate ASAP on programs from the Phoronix and SPEC benchmark suites. It can precisely select the best points in the security-performance spectrum. Moreover, we analyzed existing bugs and security vulnerabilities in RIPE, OpenSSL, and the Python interpreter, and found that the protection level offered by the ASAP approach is sufficient to protect against all of them. Joint work with Jonas Wagner, Volodymyr Kuznetsov and George Candea (EPFL), presented at IEEE S&P (Oakland) 2015.
Difference constraints have been used for termination analysis in the literature, where they denote relational inequalities of the form x ≤ y + c, and describe that the value of x in the current state is at most the value of y in the previous state plus some integer constant c. We believe that difference constraints are also a good choice for complexity and resource bound analysis because the complexity of imperative programs typically arises from counter increments and resets, which can be modeled naturally by difference constraints. In this article we propose a bound analysis based on difference constraints. We make the following contributions:
(1) Our analysis handles bound analysis problems of high practical relevance which current approaches cannot handle: We extend the range of bound analysis to a class of challenging but natural loop iteration patterns which typically appear in parsing and string-matching routines.
(2) We advocate the idea of using bound analysis to infer invariants: Our soundness proven algorithm obtains invariants through bound analysis, the inferred invariants are in turn used for obtaining bounds. Our bound analysis therefore does not rely on external techniques for invariant generation.
(3) We demonstrate that difference constraints are a suitable abstract program model for automatic complexity and resource bound analysis: We provide efficient abstraction techniques for obtaining difference constraint programs from imperative code.
(4) We report on a thorough experimental comparison of state-of-the-art bound analysis tools.
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