Dagstuhl Publishing
http://www.dagstuhl.de
RSS feed announcing the latest publications published by Schloss Dagstuhlen-en2010-06-082010-06-08http://www.dagstuhl.de/rss.phpDagstuhl Reports, Volume 7, Issue 1, January 2017, Complete Issue
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7314
Dagstuhl Reports, Volume 7, Issue 1, January 2017, Complete IssueThu, 22 Jun 2017 12:40:12 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7314Dagstuhl Reports, Table of Contents, Volume 7, Issue 1, 2017
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7313
Table of Contents, FrontmatterThu, 22 Jun 2017 12:40:02 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7313Front Matter, Table of Contents, Preface, Committee
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7302
Front Matter, Table of Contents, Preface, CommitteeWed, 21 Jun 2017 15:36:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7302The Heptane Static Worst-Case Execution Time Estimation Tool
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7303
Estimation of worst-case execution times (WCETs) is required to validate the temporal behavior of hard real time systems. Heptane is an open-source software program that estimates upper bounds of execution times on MIPS and ARM v7 architectures, offered to the WCET estimation community to experiment new WCET estimation techniques. The software architecture of Heptane was designed to be as modular and extensible as possible to facilitate the integration of new approaches. This paper is devoted to a description of Heptane, and includes information on the analyses it implements, how to use it and extend it.Wed, 21 Jun 2017 15:36:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7303STR2RTS: Refactored StreamIT Benchmarks into Statically Analyzable Parallel Benchmarks for WCET Estimation & Real-Time Scheduling
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7304
We all had quite a time to find non-proprietary architecture-independent exploitable parallel benchmarks for Worst-Case Execution Time (WCET) estimation and real-time scheduling. However, there is no consensus on a parallel benchmark suite, when compared to the single-core era and the Mälardalen benchmark suite. This document bridges part of this gap, by presenting a collection of benchmarks with the following good properties: (i) easily analyzable by static WCET estimation tools (written in structured C language, in particular neither goto nor dynamic memory allocation, containing flow information such as loop bounds); (ii) independent from any particular run-time system (MPI, OpenMP) or real-time operating system. Each benchmark is composed of the C source code of its tasks, and an XML description describing the structure of the application (tasks and amount of data exchanged between them when applicable). Each benchmark can be integrated in a full end-to-end empirical method validation protocol on multi-core architecture. This proposed collection of benchmarks is derived from the well known StreamIT [Thies et al., Comp. Constr., 2002] benchmark suite and will be integrated in the TACleBench suite [Falk et al., WCET, 2016] in a near future. All these benchmarks are available at https://gitlab.inria.fr/brouxel/STR2RTS.Wed, 21 Jun 2017 15:36:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7304Best Practice for Caching of Single-Path Code
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7305
Single-path code has some unique properties that make it interesting to explore different caching and prefetching alternatives for the stream of instructions. In this paper, we explore different cache organizations and how they perform with single-path code.Wed, 21 Jun 2017 15:36:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7305Tightening the Bounds on Cache-Related Preemption Delay in Fixed Preemption Point Scheduling
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7306
Limited Preemptive Fixed Preemption Point scheduling (LP-FPP) has the ability to decrease and control the preemption-related overheads in the real-time task systems, compared to other limited or fully preemptive scheduling approaches. However, existing methods for computing the preemption overheads in LP-FPP systems rely on over-approximation of the evicting cache blocks (ECB) calculations, potentially leading to pessimistic schedulability analysis. In this paper, we propose a novel method for preemption cost calculation that exploits the benefits of the LP-FPP task model both at the scheduling and cache analysis level. The method identifies certain infeasible preemption combinations, based on analysis on the scheduling level, and combines it with cache analysis information into a constraint problem from which less pessimistic upper bounds on cache-related preemption delays (CRPD) can be derived. The evaluation results indicate that our proposed method has the potential to significantly reduce the upper bound on CRPD, by up to 50% in our experiments, compared to the existing over-approximating calculations of the eviction scenarios.Wed, 21 Jun 2017 15:36:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7306Early WCET Prediction Using Machine Learning
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7307
For delivering a precise Worst Case Execution Time (WCET), the WCET static analysers need the executable program and the target architecture. However, a prediction (even coarse) of the future WCET would be helpful at design stages where only the source code is available. We investigate the possibility of creating predictors of the WCET based on the C source code using machine-learning (work in progress). If successful, our proposal would offer to the designer precious information on the WCET of a piece of code at the early stages of the development process.Wed, 21 Jun 2017 15:36:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7307On the Representativity of Execution Time Measurements: Studying Dependence and Multi-Mode Tasks
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7308
The Measurement-Based Probabilistic Timing Analysis (MBPTA) infers probabilistic Worst-Case Execution Time (pWCET) estimates from measurements of tasks execution times; the Extreme Value Theory (EVT) is the statistical tool that MBPTA applies for inferring worst-cases from observations/measurements of the actual task behavior. MBPTA and EVT capability of estimating safe/pessimistic pWCET rely on the quality of the measurements; in particular, execution time measurements have to be representative of the actual system execution conditions and have to cover multiple possible execution conditions. In this work, we investigate statistical dependences between execution time measurements and tasks with multiple runtime operational modes. In the first case, we outline the effects of dependences on the EVT applicability as well as on the quality of the pWCET estimates. In the second case, we propose the best approaches to account for the different task execution modes and guaranteeing safe pWCET estimates that cover them all. The solutions proposed are validated with test cases.Wed, 21 Jun 2017 15:36:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7308The W-SEPT Project: Towards Semantic-Aware WCET Estimation
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7309
Critical embedded systems are generally composed of repetitive tasks that must meet hard timing constraints, such as termination deadlines. Providing an upper bound of the worst-case execution time (WCET) of such tasks at design time is necessary to guarantee the correctness of the system. In static WCET analysis, a main source of over-approximation comes from the complexity of the modern hardware platforms: their timing behavior tends to become more unpredictable because of features like caches, pipeline, branch prediction, etc. Another source of over-approximation comes from the software itself: WCET analysis may consider potential worst-cases executions that are actually infeasible, because of the semantics of the program or because they correspond to unrealistic inputs. The W-SEPT project, for "WCET, Semantics, Precision and Traceability", has been carried out to study and exploit the influence of program semantics on the WCET estimation. This paper presents the results of this project : a semantic-aware WCET estimation workflow for high-level designed systems.Wed, 21 Jun 2017 15:36:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7309Worst-Case Execution Time Analysis of Predicated Architectures
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7310
The time-predictable design of computer architectures for the use in (hard) real-time systems is becoming more and more important, due to the increasing complexity of modern computer architectures. The design of predictable processor pipelines recently received considerable attention. The goal here is to find a trade-off between predictability and computing power.Branches and jumps are particularly problematic for high-performance processors. For one, branches are executed late in the pipeline. This either leads to high branch penalties (flushing) or complex software/hardware techniques (branch predictors). Another side-effect of branches is that they make it difficult to exploit instruction-level parallelism due to control dependencies.Predicated computer architectures allow to attach a predicate to the instructions in a program. An instruction is then only executed when the predicate evaluates to true and otherwise behaves like a simple nop instruction. Predicates can thus be used to convert control dependencies into data dependencies, which helps to address both of the aforementioned problems.A downside of predicated instructions is the precise worst-case execution time (WCET) analysis of programs making use of them. Predicated memory accesses, for instance, may or may not have an impact on the processor's cache and thus need to be considered by the cache analysis. Predication potentially has an impact on all analysis phases of a WCET analysis tool. We thus explore a preprocessing step that explicitly unfolds the control-flow graph, which allows us to apply standard analyses that are themselves not aware of predication.Wed, 21 Jun 2017 15:36:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7310Towards Multicore WCET Analysis
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7311
AbsInt is the leading provider of commercial tools for static code-level timing analysis. Its aiT Worst-Case Execution Time Analyzer computes tight bounds for the WCET of tasks in embedded real-time systems. However, the results only incorporate the core-local latencies, i.e. interference delays due to other cores in a multicore system are ignored. This paper presents some of the work we have done towards multicore WCET analysis. We look into both static and measurement-based timing analysis for COTS multicore systems.Wed, 21 Jun 2017 15:36:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7311The P-SOCRATES Timing Analysis Methodology for Parallel Real-Time Applications Deployed on Many-Core Platforms
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7312
This paper presents the timing analysis methodology developed in the European project P-SOCRATES (Parallel Software Framework for Time-Critical Many-core Systems). This timing analysis methodology is defined for parallel applications that must satisfy both performance and real-time requirements and are executed on modern many-core processor architectures. We discuss the motivation and objectives of the project, the timing analysis flow that we proposed, the tool that has been developed to automatize it, and finally we report on some of the preliminary results that we have obtained when applying this methodology to the three application use-cases of the project.Wed, 21 Jun 2017 15:36:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7312LIPIcs, Volume 77, SoCG'17, Complete Volume
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7301
LIPIcs, Volume 77, SoCG'17, Complete VolumeWed, 21 Jun 2017 15:11:24 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7301LIPIcs, Volume 74, ECOOP'17, Complete Volume
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7299
LIPIcs, Volume 74, ECOOP'17, Complete VolumeMon, 19 Jun 2017 15:53:12 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7299 Front Matter - ECOOP 2017 Artifacts, Table of Contents, Preface, Artifact Evaluation Committee
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7281
Front Matter - ECOOP 2017 Artifacts, Table of Contents, Preface, Artifact Evaluation CommitteeWed, 14 Jun 2017 12:47:12 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7281IceDust 2: Derived Bidirectional Relations and Calculation Strategy Composition (Artifact)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7282
This artifact is based on IceDust2, a data modeling language with derived values. The provided package is designed to support the claims of the companion paper: in particular, it allows users to compile and run IceDust2 specifications. Instructions for building the IceDust2 compiler from source in Spoofax are also provided.Wed, 14 Jun 2017 12:47:12 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7282A Capability-Based Module System for Authority Control (Artifact)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7283
This artifact is intended to demonstrate the module system of the Wyvern programming language and consists of a Linux virtual machine with a snapshot of the Wyvern programming language's codebase. The Wyvern codebase contains a test suite that corresponds to the code examples in the paper accompanying the artifact. In addition, the artifact contains a document describing how to compile and run Wyvern programs.Wed, 14 Jun 2017 12:47:12 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7283A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming (Artifact)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7284
This artifact contains a version of the Scribble tool that, given a protocol specification with multiple participants, can generate Scala APIs for implementing each participant in a type-safe, protocol-abiding way. Crucially, the API generation leverages a decomposition of the multiparty protocol into type-safe peer-to-peer interactions between pairs of participants; and this, in turn, allows to implement the API internals on top of the existing lchannels library for type-safe binary session programming. As a result, several technically challenging aspects in the implementation of multiparty sessions are solved "for free", at the underlying binary level. This includes distributed multiparty session delegation: this artifact implements it for the first time. Wed, 14 Jun 2017 12:47:12 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7284Concurrent Data Structures Linked in Time (Artifact)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7285
This artifact provides the full mechanization in FCSL of thedevelopments in the companion paper, "Concurrent Data StructuresLinked in Time". In the latter, we propose a new method, based on aseparation-style logic, for reasoning about concurrent objects withsuch linearization points. We embrace the dynamic nature oflinearization points, and encode it as part of the data structure'sauxiliary state, so that it can be dynamically modified inplace by auxiliary code, as needed when some appropriate run-timeevent occurs. We illustrate the method by verifying (mechanically inFCSL) an intricate optimal snapshot algorithm due to Jayanti, as wellas some clients.FCSL is the first completely formalized framework for mechanizedverification of full functional correctness of fine-grained concurrentprograms. It is implemented as an embedded domain-specific language(DSL) in the dependently-typed language of the Coq proof assistant,and is powerful enough to reason about programming features such ashigher-order functions and local thread spawning. By incorporating auniform concurrency model, based on state-transition systems andpartial commutative monoids, FCSL makes it possible to build proofsabout concurrent libraries in a thread-local, compositional way, thusfacilitating scalability and reuse: libraries are verified just once,and their specifications are used ubiquitously in client-sidereasoning.Wed, 14 Jun 2017 12:47:12 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7285Towards Strong Normalization for Dependent Object Types (DOT) (Artifact)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7286
This artifact provides the fully mechanized proof of strong normalization for D_{<:} , a variant of (Dependent Object Types) DOT (Rompf & Amin, 2016) that excludes recursive functions and recursive types. The intersection type and recursive self type are further integrated, moving towards DOT. The key proof idea follows the method of Girard (Girard, 1972) and Tait (Tait, 1967).Wed, 14 Jun 2017 12:47:12 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7286Contracts in the Wild: A Study of Java Programs (Artifact)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7287
This artefact contains a dataset of open-source programs obtained from the Maven Central Repository and scripts that first extract contracts from these programs and then perform several analyses on the contracts extracted. The extraction and analysis is fully automated and directly produces the tables presented in the accompanying paper. The results show how contracts are used in real-world program, and how their usage changes between versions and within inheritance hierarchies.Wed, 14 Jun 2017 12:47:12 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7287Parallelizing Julia with a Non-Invasive DSL (Artifact)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7288
This artifact is based on ParallelAccelerator, an embedded domain-specific language (DSL) and compiler for speeding up compute-intensive Julia programs. In particular, Julia code that makes heavy use of aggregate array operations is a good candidate for speeding up with ParallelAccelerator. ParallelAccelerator is a non-invasive DSL that makes as few changes to the host programming model as possible.Wed, 14 Jun 2017 12:47:12 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7288Mixed Messages: Measuring Conformance and Non-Interference in TypeScript (Artifact)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7289
In the paper Mixed Messages: Measuring Conformance and Non-Interference in TypeScript we present our experiences of evaluating gradual typing using our tool TypeScript TPD. The tool, based on the polymorphic blame calculus, monitors JavaScript libraries and TypeScript clients against the corresponding TypeScript definition. Our experiments yield two conclusions. First, TypeScript definitions are prone to error. Second, there are serious technical concerns with the use of the JavaScript proxy mechanism for enforcing contracts. This artifact includes all the libraries we tested, their definition files, and the source code of our tool. From this, all libraries can be wrapped and tested to reproduce the log data that formed our conclusion. All conformance errors and examples of interference are documented, and can be verified against the generated logs. Wed, 14 Jun 2017 12:47:12 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7289Type Abstraction for Relaxed Noninterference (Artifact)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7290
This artifact is a web interpreter for the ObSec language defined in the companion paper. ObSec is a simple object-oriented language that supports type-based declassification. Type-base declassification exploits the familiar notion of type abstraction to support expressive declassification policies in a simple and expressive manner. Wed, 14 Jun 2017 12:47:12 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7290EVF: An Extensible and Expressive Visitor Framework for Programming Language Reuse (Artifact)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7291
This artifact is based on EVF, an extensible and expressive Java visitor framework. EVF aims at reducing the effort involved in creation and reuse of programming languages. EVF an annotation processor that automatically generate boilerplate ASTs and AST for a given an Object Algebra interface. This artifact contains source code of the case study on "Types and Programming Languages", illustrating how effective EVF is in modularizing programming languages. There is also a microbenchmark in the artifact that shows that EVF has reasonable performance with respect to traditional visitors.Wed, 14 Jun 2017 12:47:12 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7291Mailbox Abstractions for Static Analysis of Actor Programs (Artifact)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7292
This artifact is based on Scala-AM, a static analysis framework relying on the Abstracting Abstract Machines approach. This version of the framework is extended to support actor-based programs, written in a variant of Scheme. The sound static analysis is performed in order to verify the absence of errors in actor-based program, and to compute upper bounds on actor's mailboxes. We developed several mailbox abstractions with which the static analysis can be run, and evaluate the precision of the technique with these mailbox abstractions. This artifact contains documentation on how to use analysis and on how to reproduce the results presented in the companion paper.Wed, 14 Jun 2017 12:47:12 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7292Data Exploration through Dot-driven Development (Artifact)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7293
This artifact presents The Gamma, a simple programming environment for data exploration that uses member access as the primary mechanism for constructing queries. The artifact consists of two parts. The user facing web-based component allows users to explore a simple dataset of Olympic medal winners while a back-end service provides the data and evaluates queries executed by the user.The purpose of the artifact is to illustrate the pivot type provider, which provides a simple way for constructing queries in a object-based programming language equipped with member access. The pivot type provider can be use to construct new queries from code or using the user interface, but it also encourages the user to modify existing code. Wed, 14 Jun 2017 12:47:12 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7293Evil Pickles: DoS Attacks Based on Object-Graph Engineering (Artifact)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7294
This artefact demonstrates the effects of the serialisation vulnerabilities described in the companion paper. It is composed of three components: scripts, including source code, for Java, Ruby and C# serialisation-vulnerabilities, two case studies that demonstrate attacks based on the vulnerabilities, and a contracts-based mitigation strategy for serialisation-based attacks on Java applications. The artefact allows users to witness how the serialisation-based vulnerabilities result in behavior that can be used in security attacks. It also supports the repeatability of the case study experiments and the benchmark for the mitigation measures proposed in the paper. Instructions for running the tasks are provided along with a description of the artefact setup.Wed, 14 Jun 2017 12:47:12 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7294Interprocedural Specialization of Higher-Order Dynamic Languages Without Static Analysis (Artifact)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7295
This artifact is based on LC, a research oriented JIT compiler for Scheme. The compiler is extended to allow interprocedural, type based, code specialization using the technique and its implementation presented in the paper. Because the technique is directly implemented in LC, the package contains the build of the compiler used for our experiments. To support repeatability, the artifact allows the user to easily extract the data presented in the paper such as the number of executed type checks or the generated code size. The user can repeat the experiments using a set of standard benchmarks as well as its own programs. Instructions for building the compiler from scratch are also provided.Wed, 14 Jun 2017 12:47:12 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7295Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris (Artifact)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7296
This artifact provides the soundness proofs for the encodings in Iris the RSL and GPS logics, as well as the verification for all standard examples known to be verifiable in those logics. All of these proofs are formalized in Coq, which is the main content of this artifact. The formalization is provided in a virtual machine for the convenience of testing, but can also be built from source.Wed, 14 Jun 2017 12:47:12 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7296Proactive Synthesis of Recursive Tree-to-String Functions from Examples (Artifact)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7297
This artifact, named Prosy, is an interactive command-line tool for synthesizing recursive tree-to-string functions (e.g. pretty-printers) from examples. Specifically, Prosy takes as input a Scala file containing a hierarchy of abstract and case classes, and synthesizes the printing function after interacting with the user. Prosy first pro-actively generates a finite set of trees such that their string representations uniquely determine the function to synthesize. While asking the output for each example, Prosy prunes away questions when it can infer their answers from previous answers. In the companion paper, we prove that this pruning allows Prosy not to require that the user provides answers to the entire set of questions, which is of size O(n^3) where n is the size of the input file, but only to a reasonably small subset of size O(n). Furthermore, Prosy guides the interaction by providing suggestions whenever it can.Wed, 14 Jun 2017 12:47:12 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7297Challenges to Achieving High Availability at Scale (Invited Talk)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7250
Facebook is a social network that connects more than 1.8 billion people. To serve these many users requires infrastructure which is composed of thousands of interdependent systems that span geographically distributed data centers. But what is the guiding principle for building and operating these systems?For Facebook’s infrastructure teams the answer is: Systems must always be available and never lose data. This talk will explore this quest. We will focus on three aspects.Availability and consistency. What form of consistency do Facebook’s systems guarantee? Strong consistency makes understanding easy but has latency penalties, weak consistency is fast but difficult to reason for developers and users. We describe our usage of eventual consistency and delve into how Facebook constructs its caching and replicated storage systems to minimize the duration for achieving consistency. We share empirical data that measures the effectiveness of our design.Availability and correctness. With network partitions, relaxed forms of consistency, and software bugs, how do we guarantee a consistent state? We present two systems to find and repair structural errors in Facebook’s social graph, one batch and one real-time.Availability and scale. Sharding is one of the standard answers to operate at scale. But how can we develop one system that can shard storage as well as compute? We will introduce a new Sharding-as-a-Service component. We will show and evaluate how its design and service policies control for latency, failure tolerance and operationally efficiency.Tue, 13 Jun 2017 16:00:31 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7250IceDust 2: Derived Bidirectional Relations and Calculation Strategy Composition
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7251
Derived values are values calculated from base values. They can be expressed with views in relational databases, or with expressions in incremental or reactive programming. However, relational views do not provide multiplicity bounds, and incremental and reactive programming require significant boilerplate code in order to encode bidirectional derived values. Moreover, the composition of various strategies for calculating derived values is either disallowed, or not checked for producing derived values which will be consistent with the derived values they depend upon.In this paper we present IceDust2, an extension of the declarative data modeling language IceDust with derived bidirectional relations with multiplicity bounds and support for statically checked composition of calculation strategies. Derived bidirectional relations, multiplicity bounds, and calculation strategies all influence runtime behavior of changes to data, leading to hundreds of possible behavior definitions. IceDust2 uses a product-line based code generator to avoid explicitly defining all possible combinations, making it easier to reason about correctness. The type system allows only sound composition of strategies and guarantees multiplicity bounds. Finally, our case studies validate the usability of IceDust2 in applications.Tue, 13 Jun 2017 16:00:31 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7251Speeding Up Maximal Causality Reduction with Static Dependency Analysis
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7252
Stateless Model Checking (SMC) offers a powerful approach to verifying multithreaded programs but suffers from the state-space explosion problem caused by the huge thread interleaving space. The pioneering reduction technique Partial Order Reduction (POR) mitigates this problem by pruning equivalent interleavings from the state space. However, limited by the happens-before relation, POR still explores redundant executions. The recent advance, Maximal Causality Reduction (MCR), shows a promising performance improvement over the existing reduction techniques, but it has to construct complicated constraints to ensure the feasibility of the derived execution due to the lack of dependency information. In this work, we present a new technique, which extends MCR with static analysis to reduce the size of the constraints, thus speeding up the exploration of the state space. We also address the redundancy problem caused by the use of static analysis. We capture the dependency between a read and a later event e in the trace from the system dependency graph and identify those reads that e is not control dependent on. Our approach then ignores the constraints over such reads to reduce the complexity of the constraints. The experimental results show that compared to MCR, the number of the constraints and the solving time by our approach are averagely reduced by 31.6% and 27.8%, respectively.Tue, 13 Jun 2017 16:00:31 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7252Mixing Metaphors: Actors as Channels and Channels as Actors
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7253
Channel- and actor-based programming languages are both used inpractice, but the two are often confused. Languages such as Goprovide anonymous processes which communicate using buffers or rendezvous points---known as channels---while languages such as Erlang provide addressable processes---known as actors---each with a single incoming message queue.The lack of a common representation makes it difficult to reason abouttranslations that exist in the folklore. We define a calculuslambda-ch for typed asynchronous channels, and a calculus lambda-act fortyped actors. We define translations from lambda-act into lambda-ch andlambda-ch into lambda-act and prove that both are type- andsemantics-preserving.We show that our approach accounts for synchronisation and selectivereceive in actor systems and discuss future extensions to support guardedchoice and behavioural types.Tue, 13 Jun 2017 16:00:31 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7253Mailbox Abstractions for Static Analysis of Actor Programs
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7254
Properties such as the absence of errors or bounds on mailbox sizes are hard to deduce statically for actor-based programs.This is because actor-based programs exhibit several sources of unboundedness, in addition to the non-determinism that is inherent to the concurrent execution of actors.We developed a static technique based on abstract interpretation to soundly reason in a finite amount of time about the possible executions of an actor-based program.We use our technique to statically verify the absence of errors in actor-based programs, and to compute upper bounds on the actors' mailboxes.Sound abstraction of these mailboxes is crucial to the precision of any such technique.We provide several mailbox abstractions and categorize them according to the extent to which they preserve message ordering and multiplicity of messages in a mailbox.We formally prove the soundness of each mailbox abstraction, and empirically evaluate their precision and performance trade-offs on a corpus of benchmark programs.The results show that our technique can statically verify the absence of errors for more benchmark programs than the state-of-the-art analysis.Tue, 13 Jun 2017 16:00:31 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7254Concurrent Data Structures Linked in Time
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7255
Arguments about correctness of a concurrent data structure aretypically carried out by using the notion of linearizability andspecifying the linearization points of the data structure'sprocedures. Such arguments are often cumbersome as the linearizationpoints' position in time can be dynamic (depend on the interference,run-time values and events from the past, or even future), non-local(appear in procedures other than the one considered), and whoseposition in the execution trace may only be determined after theconsidered procedure has already terminated.In this paper we propose a new method, based on a separation-stylelogic, for reasoning about concurrent objects with such linearizationpoints. We embrace the dynamic nature of linearization points, andencode it as part of the data structure's auxiliary state, so that itcan be dynamically modified in place by auxiliary code, as needed whensome appropriate run-time event occurs. We name the idealinking-in-time, because it reduces temporal reasoning to spatialreasoning. For example, modifying a temporal position of alinearization point can be modeled similarly to a pointer update inseparation logic. Furthermore, the auxiliary state provides aconvenient way to concisely express the properties essential forreasoning about clients of such concurrent objects. We illustrate themethod by verifying (mechanically in Coq) an intricate optimalsnapshot algorithm due to Jayanti, as well as some clients.Tue, 13 Jun 2017 16:00:31 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7255A Generic Approach to Flow-Sensitive Polymorphic Effects
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7256
Effect systems are lightweight extensions to type systems that can verify a wide range of important properties with modest developer burden. But our general understanding of effect systems is limited primarily to systems where the order of effects is irrelevant.Understanding such systems in terms of a lattice of effects grounds understanding of the essential issues, and provides guidance when designing new effect systems.By contrast, sequential effect systems --- where the order of effects is important --- lack a clear algebraic characterization.We derive an algebraic characterization from the shape of prior concrete sequential effect systems.We present an abstract polymorphic effect system with singleton effects parameterized by an effect quantale --- an algebraic structure with well-defined properties that can model a range of existing order-sensitive effect systems. We define effect quantales, derive useful properties, and show how they cleanly model a variety of known sequential effect systems.We show that effect quantales provide a free, general notion of iterating a sequential effect, and that for systems we consider the derived iteration agrees with the manually designed iteration operators in prior work.Identifying and applying the right algebraic structure led us to subtle insights into the design of order-sensitive effect systems, which provides guidance on non-obvious points of designing order-sensitive effect systems.Effect quantales have clear relationships to the recent category theoretic work on order-sensitive effect systems, but are explained without recourse to category theory. In addition, our derived iteration construct should generalize to these semantic structures, addressing limitations of that work.Tue, 13 Jun 2017 16:00:31 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7256Proactive Synthesis of Recursive Tree-to-String Functions from Examples
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7257
Synthesis from examples enables non-expert users to generate programs by specifying examples of their behavior. A domain-specific form of such synthesis has been recently deployed in a widely used spreadsheet software product. In this paper we contribute to foundations of such techniques and present a complete algorithm for synthesis of a class of recursive functions defined by structural recursion over a given algebraic data type definition. The functions we consider map an algebraic data type to a string; they are useful for, e.g., pretty printing and serialization of programs and data. We formalize our problem as learning deterministic sequentialtop-down tree-to-string transducers with a single state (1STS).The first problem we consider is learning a tree-to-stringtransducer from any set of input/output examples provided by the user. We show that, given a set of input/output examples, checking whether there exists a 1STS consistent with these examples is NP-complete in general. In contrast, the problem can be solved in polynomial time under a (practically useful) closure condition that eachsubtree of a tree in the input/output example set is alsopart of the input/output examples.Because coming up with relevant input/output examples may bedifficult for the user while creating hard constraint problemsfor the synthesizer, we also study a more automatedactive learning scenario in which the algorithm chooses theinputs for which the user provides the outputs. Ouralgorithm asks a worst-case linear number of queries as afunction of the size of the algebraic data type definitionto determine a unique transducer.To construct our algorithms we present two new results onformal languages.First, we define a class of word equations, calledsequential word equations, for which we prove thatsatisfiability can be solved in deterministic polynomialtime. This is in contrast to the general word equations forwhich the best known complexity upper bound is in linear space.Second, we close a long-standing open problem about theasymptotic size of test sets for context-free languages. Atest set of a language of words L is a subset T of Lsuch that any two word homomorphisms equivalent on T arealso equivalent on L. We prove that it is possible tobuild test sets of cubic size for context-free languages,matching for the first time the lower bound found 20 yearsago.Tue, 13 Jun 2017 16:00:31 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7257An Empirical Study on Deoptimization in the Graal Compiler
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7258
Managed language platforms such as the Java Virtual Machine or the Common Language Runtime rely on a dynamic compiler to achieve high performance. Besides making optimization decisions based on the actual program execution and the underlying hardware platform, a dynamic compiler is also in an ideal position to perform speculative optimizations. However, these tend to increase the compilation costs, because unsuccessful speculations trigger deoptimization and recompilation of the affected parts of the program, wasting previous work. Even though speculative optimizations are widely used, the costs of these optimizations in terms of extra compilation work has not been previously studied. In this paper, we analyze the behavior of the Graal dynamic compiler integrated in Oracle's HotSpot Virtual Machine. We focus on situations which cause program execution to switch from machine code to the interpreter, and compare application performance using three different deoptimization strategies which influence the amount of extra compilation work done by Graal. Using an adaptive deoptimization strategy, we managed to improve the average start-up performance of benchmarks from the DaCapo, ScalaBench, and Octane benchmark suites, mostly by avoiding wasted compilation work. On a single-core system, we observed an average speed-up of 6.4% for the DaCapo and ScalaBench workloads, and a speed-up of 5.1% for the Octane workloads; the improvement decreases with an increasing number of available CPU cores. We also find that the choice of a deoptimization strategy has negligible impact on steady-state performance. This indicates that the cost of speculation matters mainly during start-up, where it can disturb the delicate balance between executing the program and the compiler, but is quickly amortized in steady state.Tue, 13 Jun 2017 16:00:31 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7258Contracts in the Wild: A Study of Java Programs
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7259
The use of formal contracts has long been advocated as an approach to develop programs that are provably correct. However, the reality is that adoption of contracts has been slow in practice. Despite this, the adoption of lightweight contracts — typically utilising runtime checking — has progressed. In the case of Java, built-in features of the language (e.g. assertions and exceptions) can be used for this. Furthermore, a number of libraries which facilitate contract checking have arisen.In this paper, we catalogue 25 techniques and tools for lightweight contract checking in Java, and present the results of an empirical study looking at a dataset extracted from the 200 most popular projects found on Maven Central, constituting roughly 351,034 KLOC. We examine (1) the extent to which contracts are used and (2) what kind of contracts are used. We then investigate how contracts are used to safeguard code, and study problems in the context of two types of substitutability that can be guarded by contracts: (3) unsafe evolution of APIs that may break client programs and (4) violations of Liskovs Substitution Principle (LSP) when methods are overridden. We find that: (1) a wide range of techniques and constructs are used to represent contracts, and often the same program uses different techniques at the same time; (2) overall, contracts are used less than expected, with significant differences between programs; (3) projects that use contracts continue to do so, and expand the use of contracts as they grow and evolve; and, (4) there are cases where the use of contracts points to unsafe subtyping (violations of Liskov's Substitution Principle) and unsafe evolution.Tue, 13 Jun 2017 16:00:31 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7259Evil Pickles: DoS Attacks Based on Object-Graph Engineering
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7260
In recent years, multiple vulnerabilities exploiting the serialisation APIs of various programming languages, including Java, have been discovered. These vulnerabilities can be used to devise in- jection attacks, exploiting the presence of dynamic programming language features like reflection or dynamic proxies. In this paper, we investigate a new type of serialisation-related vulnerabilit- ies for Java that exploit the topology of object graphs constructed from classes of the standard library in a way that deserialisation leads to resource exhaustion, facilitating denial of service attacks. We analyse three such vulnerabilities that can be exploited to exhaust stack memory, heap memory and CPU time. We discuss the language and library design features that enable these vulnerabilities, and investigate whether these vulnerabilities can be ported to C#, Java- Script and Ruby. We present two case studies that demonstrate how the vulnerabilities can be used in attacks on two widely used servers, Jenkins deployed on Tomcat and JBoss. Finally, we propose a mitigation strategy based on contract injection.Tue, 13 Jun 2017 16:00:31 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7260Data Exploration through Dot-driven Development
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7261
Data literacy is becoming increasingly important in the modern world. While spreadsheets make simple data analytics accessible to a large number of people, creating transparent scripts that can be checked, modified, reproduced and formally analyzed requires expert programming skills. In this paper, we describe the design of a data exploration language that makes the task more accessible by embedding advanced programming concepts into a simple core language.The core language uses type providers, but we employ them in a novel way -- rather than providing types with members for accessing data, we provide types with members that allow the user to also compose rich and correct queries using just member access ('dot'). This way, we recreate functionality that usually requires complex type systems (row polymorphism, type state and dependent typing) in an extremely simple object-based language.We formalize our approach using an object-based calculus and prove that programs constructed using the provided types represent valid data transformations. We discuss a case study developed using the language, together with additional editor tooling that bridges some of the gaps between programming and spreadsheets. We believe that this work provides a pathway towards democratizing data science - our use of type providers significantly reduce the complexity of languages that one needs to understand in order to write scripts for exploring data.Tue, 13 Jun 2017 16:00:31 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7261A Co-contextual Type Checker for Featherweight Java
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7262
This paper addresses compositional and incremental type checking for object-oriented programming languages. Recent work achieved incremental type checking for structurally typed functional languages through co-contextual typing rules, a constraint-based formulation that removes any context dependency for expression typings. However, that work does not cover key features of object-oriented languages: Subtype polymorphism, nominal typing, and implementation inheritance. Type checkers encode these features in the form of class tables, an additional form of typing context inhibiting incrementalization.In the present work, we demonstrate that an appropriate co-contextual notion to class tables exists, paving the way to efficient incremental type checkers for object-oriented languages. This yields a novel formulation of Igarashi et al.'s Featherweight Java (FJ) type system, where we replace class tables by the dual concept of class table requirements and class table operations by dual operations on class table requirements. We prove the equivalence of FJ's type system and our co-contextual formulation. Based on our formulation, we implemented an incremental FJ type checker and compared its performance against javac on a number of realistic example programs.Tue, 13 Jun 2017 16:00:31 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7262A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7263
Multiparty Session Types (MPST) is a typing discipline formessage-passing distributed processes that can ensure properties suchas absence of communication errors and deadlocks, and protocolconformance. Can MPST provide a theoretical foundation for concurrent and distributed programming in "mainstream" languages? We addressthis problem by (1) developing the first encoding of afull-fledged multiparty session pi-calculus into linearpi-calculus, and (2) using the encoding as the foundation of apractical toolchain for safe multiparty programming in Scala.Our encoding is type-preserving and operationally sound and complete.Crucially, it keeps the distributed choreographic nature ofMPST, illuminating that the safety properties of multiparty sessionscan be precisely represented with a decomposition into binarylinear channels. Previous works have only studied the relationbetween (limited) multiparty and binary sessions via centralisedorchestration means. We exploit these results to implement anautomated generation of Scala APIs for multiparty sessions,abstracting existing libraries for binary communication channels.This allows multiparty systems to be safely implemented over binarymessage transports, as commonly found in practice. Our implementationis the first to support distributed multiparty delegation: ourencoding yields it for free, via existing mechanisms for binarydelegation.Tue, 13 Jun 2017 16:00:31 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7263Mixed Messages: Measuring Conformance and Non-Interference in TypeScript
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7264
TypeScript participates in the recent trend among programminglanguages to support gradual typing. The DefinitelyTyped Repositoryfor TypeScript supplies type definitions for over 2000 popularJavaScript libraries. However, there is no guarantee thatimplementations conform to their corresponding declarations.We present a practical evaluation of gradual typing for TypeScript.We have developed a tool for use with TypeScript, based on thepolymorphic blame calculus, for monitoring JavaScript libraries andTypeScript clients against the TypeScript definition. We apply ourtool, TypeScript TPD, to those libraries in the DefinitelyTypedRepository which had adequate test code to use. Of the 122 librarieswe checked, 62 had cases where either the library or its testsfailed to conform to the declaration.Gradual typing should satisfy non-interference. Monitoring a programshould never change its behaviour, except to raise a type errorshould a value not conform to its declared type. However, ourexperience also suggests serious technical concerns with the use ofthe JavaScript proxy mechanism for enforcing contracts. Of the 122libraries we checked, 22 had cases where the library or its testsviolated non-interference.Tue, 13 Jun 2017 16:00:31 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7264muPuppet: A Declarative Subset of the Puppet Configuration Language
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7265
Puppet is a popular declarative framework for specifying and managing complex system configurations. The Puppet framework includes a domain-specific language with several advanced features inspired by object-oriented programming, including user-defined resource types, ‘classes’ with a form of inheritance, and dependency management. Like most real-world languages, the language has evolved in an ad hoc fashion, resulting in a design with numerous features, some of which are complex, hard to understand, and difficult to use correctly.We present an operational semantics for muPuppet, a representative subset of the Puppet language that covers the distinctive features of Puppet, while excluding features that are either deprecated or work-in-progress. Formalising the semantics sheds light on difficult parts of the language, identifies opportunities for future improvements, and provides a foundation for future analysis or debugging techniques, such as static typechecking or provenance tracking. Our semantics leads straightforwardly to a reference implementation in Haskell. We also discuss some of Puppet’s idiosyncrasies, particularly its handling of classes and scope, and present an initial corpus of test cases supported by our formal semantics.Tue, 13 Jun 2017 16:00:31 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7265Promising Compilation to ARMv8 POP
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7266
We prove the correctness of compilation of relaxed memory accesses and release-acquire fences from the "promising" semantics of [Kang et al. POPL'17] to the ARMv8 POP machine of [Flur et al. POPL'16]. The proof is highly non-trivial because both the ARMv8 POP and the promising semantics provide some extremely weak consistency guarantees for normal memory accesses; however, they do so in rather different ways. Our proof of compilation correctness to ARMv8 POP strengthens the results of the Kang et al., who only proved the correctness of compilation to x86-TSO and Power, which are much simpler in comparison to ARMv8 POP. Tue, 13 Jun 2017 16:00:31 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7266Relaxed Linear References for Lock-free Data Structures
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7267
Linear references are guaranteed to be free from aliases. This is a strong property that simplifies reasoning about programs and enables powerful optimisations, but it is also a property that is too strong for many applications. Notably, lock-free algorithms, which implement protocols that ensure safe, non-blocking concurrent access to data structures, are generally not typable with linear references because they rely on aliasing to achieve lock-freedom.This paper presents LOLCAT, a type system with a relaxed notion of linearity that allows an unbounded number of aliases to an object as long as at most one alias at a time owns the right to access the contents of the object. This ownership can be transferred between aliases, but can never be duplicated. types are powerful enough to type several lock-free data structures and give a compile-time guarantee of absence of data-races when accessing owned data. In particular, LOLCAT is able to assign types to the CAS (compare and swap) primitive that precisely describe how ownership is transferred across aliases, possibly across different threads.The paper introduces LOLCAT through a sound core procedural calculus, and shows how LOLCAT can be applied to three fundamental lock-free data structures. It also discusses a prototype implementation which integrates LOLCAT with an object-oriented programming language.Tue, 13 Jun 2017 16:00:31 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7267Type Abstraction for Relaxed Noninterference
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7268
Information-flow security typing statically prevents confidential information to leak to public channels. The fundamental information flow property, known as noninterference, states that a public observer cannot learn anything from private data. As attractive as it is from a theoretical viewpoint, noninterference is impractical: real systems need to intentionally declassify some information, selectively. Among the different information flow approaches to declassification, a particularly expressive approach was proposed by Li and Zdancewic, enforcing a notion of relaxed noninterference by allowing programmers to specify declassification policies that capture the intended manner in which public information can be computed from private data. This paper shows how we can exploit the familiar notion of type abstraction to support expressive declassification policies in a simpler, yet more expressive manner. In particular, the type-based approach to declassification---which we develop in an object-oriented setting---addresses several issues and challenges with respect to prior work, including a simple notion of label ordering based on subtyping, support for recursive declassification policies, and a local, modular reasoning principle for relaxed noninterference. This work paves the way for integrating declassification policies in practical security-typed languages.Tue, 13 Jun 2017 16:00:31 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7268Parallelizing Julia with a Non-Invasive DSL
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7269
Computational scientists often prototype software using productivitylanguages that offer high-level programming abstractions. When higherperformance is needed, they are obliged to rewrite their code in alower-level efficiency language. Different solutions have beenproposed to address this trade-off between productivity andefficiency. One promising approach is to create embeddeddomain-specific languages that sacrifice generality for productivityand performance, but practical experience with DSLs points to someroad blocks preventing widespread adoption. This paper proposes anon-invasive domain-specific language that makes as few visiblechanges to the host programming model as possible. We present ParallelAccelerator,a library and compiler for high-level, high-performance scientificcomputing in Julia. ParallelAccelerator's programming model is aligned with existingJulia programming idioms. Our compiler exposes the implicitparallelism in high-level array-style programs and compiles them tofast, parallel native code. Programs can also run in "library-only"mode, letting users benefit from the full Julia environment andlibraries. Our results show encouraging performance improvements with very few changes to source code required. In particular, few to no additional type annotations are necessary.Tue, 13 Jun 2017 16:00:31 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7269A Capability-Based Module System for Authority Control
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7270
The principle of least authority states that each component of the system should be given authority to access only the information and resources that it needs for its operation. This principle is fundamental to the secure design of software systems, as it helps to limit an application's attack surface and to isolate vulnerabilities and faults. Unfortunately, current programming languages do not provide adequate help in controlling the authority of application modules, an issue that is particularly acute in the case of untrusted third-party extensions.In this paper, we present a language design that facilitates controlling the authority granted to each application module. The key technical novelty of our approach is that modules are first-class, statically typed capabilities. First-class modules are essentially objects, and so we formalize our module system by translation into an object calculus and prove that the core calculus is type-safe and authority-safe. Unlike prior formalizations, our work defines authority non-transitively, allowing engineers to reason about software designs that use wrappers to provide an attenuated version of a more powerful capability.Our approach allows developers to determine a module's authority by examining the capabilities passed as module arguments when the module is created, or delegated to the module later during execution. The type system facilitates this by identifying which objects provide capabilities to sensitive resources, and by enabling security architects to examine the capabilities passed into and out of a module based only on the module's interface, without needing to examine the module's implementation code. An implementation of the module system and illustrative examples in the Wyvern programming language suggest that our approach can be a practical way to control module authority.Tue, 13 Jun 2017 16:00:31 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7270Interprocedural Specialization of Higher-Order Dynamic Languages Without Static Analysis
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7271
Function duplication is widely used by JIT compilers to efficiently implement dynamic languages. When the source language supports higher order functions, the called function's identity is not generally known when compiling a call site, thus limiting the use of function duplication. This paper presents a JIT compilation technique enabling function duplication in the presence of higher order functions. Unlike existing techniques, our approach uses dynamic dispatch at call sites instead of relying on a conservative analysis to discover function identity. We have implemented the technique in a JIT compiler for Scheme.Experiments show that it is efficient at removing type checks, allowing the removal of almost all the run time type checks for several benchmarks.This allows the compiler to generate code up to 50% faster. We show that the technique can be used to duplicate functions using other run time information opening up new applications such as register allocation based duplication and aggressive inlining.Tue, 13 Jun 2017 16:00:31 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7271What'’s the Optimal Performance of Precise Dynamic Race Detection? –A Redundancy Perspective
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7272
In a precise data race detector, a race is detected only if the execution exhibits a real race. In such tools, every memory access from each thread is typically checked by a happens-before algorithm. What’s the optimal runtime performance of such tools? In this paper, we identify that a significant percentage of memory access checks in real-world program executions are often redundant: removing these checks affects neither the precision nor the capability of race detection. We show that if all such redundant checks were eliminated with no cost, the optimal performance of a state-of-the-art dynamic race detector, FastTrack, could be improved by 90%, reducing its runtime overhead from 68X to 7X on a collection of CPU intensive benchmarks. We further develop a purely dynamic technique, ReX, that efficiently filters out redundant checks and apply it to FastTrack. With ReX, the runtime performance of FastTrack is improved by 31% on average.Tue, 13 Jun 2017 16:00:31 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7272Compiling Tree Transforms to Operate on Packed Representations
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7273
When written idiomatically in most programming languages, programsthat traverse and construct trees operate over pointer-based datastructures, using one heap object per-leaf and per-node. Thisrepresentation is efficient for random access and shape-changingmodifications, but for traversals, such as compiler passes, thatprocess most or all of a tree in bulk, it can be inefficient. In thiswork we instead compile tree traversals to operate onpointer-free pre-order serializations of trees. On modernarchitectures such programs often run significantly faster thantheir pointer-based counterparts, and additionally are directly suitedto storage and transmission without requiring marshaling.We present a prototype compiler, Gibbon, that compiles asmall first-order, purely functional language sufficient for treetraversals. The compiler transforms this language into intermediaterepresentation with explicit pointers into input and output buffersfor packed data. The key compiler technologies include an effectsystem for capturing traversal behavior, combined with an algorithm toinsert destination cursors. We evaluate our compiler on treetransformations over a real-world dataset of source-code syntax trees.For traversals touching the whole tree, such as maps and folds, packeddata allows speedups of over 2x compared to a highly-optimizedpointer-based baseline.Tue, 13 Jun 2017 16:00:31 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7273EVF: An Extensible and Expressive Visitor Framework for Programming Language Reuse
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7274
Object Algebras are a design pattern that enables extensibility, modularity, and reuse in mainstream object-oriented languages such as Java. The theoretical foundations of Object Algebras are rooted on Church encodings of datatypes, which are in turn closely related to folds in functional programming. Unfortunately, it is well-known that certain programs are difficult to write, and may incur performance penalties when using Church-encodings/folds.This paper presents EVF: an extensible and expressive Java Visitor framework. The visitors supported by EVF generalize Object Algebras and enable writing programs using a generally recursive style rather than folds. The use of such generally recursive style enables users to more naturally write programs, which would otherwise require contrived workarounds using a fold-like structure. EVF visitors retain the type-safe extensibility of Object Algebras. The key advance in EVF is a novel technique to support extensible external visitors. Extensible external visitors are able to control traversals with direct access to the data structure being traversed, allowing dependent operations to be defined modularly without the need of advanced type system features. To make EVF practical, the framework employs annotations to automatically generate large amounts of boilerplate code related to visitors and traversals. To illustrate the applicability of EVF we conduct a case study, which refactors a large number of non-modular interpreters from the “Types and Programming Languages” (TAPL) book. Using EVF we are able to create a modular software product line (SPL) of the TAPL interpreters, enabling sharing of large portions of code and features. The TAPL software product line contains several modular operations, which would be non-trivial to define with standard Object Algebras.Tue, 13 Jun 2017 16:00:31 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7274Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7275
The field of concurrent separation logics (CSLs) has recentlyundergone two exciting developments: (1) the Iris framework forencoding and unifying advanced higher-order CSLs and formalizing them in Coq, and (2) the adaptation of CSLs to account for weak memory models, notably C11's release-acquire (RA) consistency.Unfortunately, these developments are seemingly incompatible, sinceIris only applies to languages with an operational interleavingsemantics, while C11 is defined by a declarative (axiomatic)semantics. In this paper, we show that, on the contrary, it is notonly feasible but useful to marry these developments together. Ourfirst step is to provide a novel operational characterization ofRA+NA, the fragment of C11 containing RA accesses and "non-atomic"(normal data) accesses. Instantiating Iris with this semantics, wethen derive higher-order variants of two prominent RA+NA logics, GPSand RSL. Finally, we deploy these derived logics in order to performthe first mechanical verifications (in Coq) of several interestingcase studies of RA+NA programming. In a nutshell, we provide thefirst foundationally verified framework for proving programs correctunder C11's weak-memory semantics.Tue, 13 Jun 2017 16:00:31 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7275Towards Strong Normalization for Dependent Object Types (DOT)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7276
The Dependent Object Types (DOT) family of calculi has been proposed as a new theoretic foundation for Scala and similar languages, unifying functional programming, object oriented programming and ML-style module systems. Following the recent type soundness proof forDOT, the present paper aims to establish stronger meta-theoretic properties. The main result is a fully mechanized proof of strong normalization for D_<:, a variant of DOT that excludes recursive functions and recursive types. We further discuss techniques and challenges for adding recursive types while maintaining strong normalization, and demonstrate that certain variants of recursive self types can be integrated successfully.Tue, 13 Jun 2017 16:00:31 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7276Modelling Homogeneous Generative Meta-Programming
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7277
Homogeneous generative meta-programming (HGMP) enables the generation of program fragments at compile-time or run-time. We present a foundational calculus which can model both compile-time and run-time evaluated HGMP, allowing us to model, for the first time, languages such as Template Haskell. The calculus is designed such that it can be gradually enhanced with the features needed to model many of theadvanced features of real languages. We demonstrate this by showing how a simple, staged type system as found in Template Haskell can be added to the calculus.Tue, 13 Jun 2017 16:00:31 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7277Front Matter, Table of Contents, Foreword, Conference Organization, External Reviewers, Authors
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7278
Front Matter, Table of Contents, Foreword, Conference Organization, External Reviewers, AuthorsTue, 13 Jun 2017 16:00:31 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7278Composing Software in an Age of Dissonance (Invited Talk)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7279
The power of languages is rooted in composition. An infinite number of sentences can be composed from a finite set of generative rules. The more uniformly the rules apply, the more valid compositions there are. Hence simpler rules give rise to richer discourse - a case of ‘less is more’. We must however be careful as to which distinctions we preserve and which we eliminate. If we abstract too much we risk creating an undifferentiated soup with no landmarks to orient us.A uniform space of objects with simple rules governing their interaction is an obvious example of these ideas, but objects also serve as a cautionary tale. Achieving simplicity is not easy; it requires taste, judgement, experience and dedication. Ingenuity is essential as well, but left unchecked, it often leads to uncontrollable complexity. The path of least resistance follows the tautological principle that ‘more is more’, and who can argue with a tautology? Dissonance dominates.I will endeavour to illustrate these rather abstract principles by means of examples from my own work and that of others, in programming languages, software and other domains. We may speak of many things - mixins, modules and memory, graphics and generics, patterns and parsers, architecture and automobiles, objects or other things entirely.Tue, 13 Jun 2017 16:00:31 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7279Retargeting Gradual Typing (Invited Talk)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7280
Gradual typing is often motivated by efforts to add types to massive untyped code bases. A major challenge here is the fact that these code bases were not written with types in mind, yet the goal is to add types to them without requiring any significant changes in their implementation. Thus, critical to this application is the notion that gradual typing is being added onto a preexisting system.But gradual typing also has applications in education, prototyping, and scripting. It allows programmers to ignore types while they are learning programmatic reasoning, while they are experimenting with new designs, or while they are interacting with external systems. At the same time, gradual typing allows these programmers to utilize APIs with types that provide navigable documentation, that concisely describe interfaces, and that enable IDEs to provide assistance. In these applications, programmers are working with types even when they are not writing types. By targeting just these applications, we can lift a major burden from gradual typing. Rather than being added to something that already exists, here gradual typing can be integrated into the software-development process, into the core language design, and into the run-time environment, with each component designed to support gradual typing from conception.This retargeting provides significant flexibility, enabling designers to tradeoff various capabilities of gradual typing. For example, a designer might choose to require some minor annotation burden in untyped programs for, say, a hundred-fold improvement in run-time performance. For the past half decade I have been exploring gradual typing behind the scenes in both academia and industry, and I will be presenting my experiences with these design tradeoffs so far.Tue, 13 Jun 2017 16:00:31 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7280Theory and Applications of Behavioural Types (Dagstuhl Seminar 17051)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7249
This report documents the programme and the outcomes of Dagstuhl Seminar 17051 "Theory and Applications of Behavioural Types". Behavioural types describe the dynamic aspects of programs, in contrast to data types, which describe the fixed structure of data. Perhaps the most well-known form of behavioural types is session types, which are type-theoretic specifications of communication protocols. More generally, behavioural types include typestate systems, which specify state-dependent availability of operations; choreographies, which specify collective communication behaviour; and behavioural contracts.In recent years, research activity in behavioural types has increased dramatically, in both theoretical and practical directions. Theoretical work has explored new relationships between established behavioural type systems and areas such as linear logic, automata theory, process calculus testing theory, dependent type theory, and model-checking. On the practical side, there are several implementations of programming languages, programming language extensions, software development tools, and runtime monitoring systems, which are becoming mature enough to apply to real-world case studies.The seminar brought together researchers from the established, largely European, research community in behavioural types, and other participants from outside Europe and from related research topics such as effect systems and actor-based languages. The questions that we intended to explore included:- How can we understand the relationships between the foundations of session types in terms of linear logic, automata, denotational models, and other type theories?- How can the scope and applicability of behavioural types be increased by incorporating ideas and approaches from gradual typing and dependent type theory?- What is the relationship, in terms of expressivity and tractability, between behavioural types and other verification techniques such as model-checking?- What are the theoretical and practical obstacles to delivering behavioural types to software developers in a range of mainstream programming languages?- What are the advantages and disadvantages of incorporating behavioural types into standard programming languages or designing new languages directly based on the foundations of session types?- How can we evaluate the effectiveness of behavioural types in programming languages and software development?Thu, 08 Jun 2017 16:15:02 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7249From Characters to Understanding Natural Language (C2NLU): Robust End-to-End Deep Learning for NLP (Dagstuhl Seminar 17042)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7248
This report documents the program and the outcomes of Dagstuhl Seminar 17042 "From Characters to Understanding Natural Language (C2NLU): Robust End-to-End Deep Learning for NLP". The seminar brought together researchers from different fields, including natural language processing, computational linguistics, deep learning and general machine learning. 31 participants from 22 academic and industrial institutions discussed advantages and challenges of using characters, i.e., "raw text", as input for deep learning models instead of language-specific tokens. Eight talks provided overviews of different topics, approaches and challenges in current natural language processing research. In five working groups, the participants discussed current natural language processing/understanding topics in the context of character-based modeling, namely, morphology, machine translation, representation learning, end-to-end systems and dialogue. In most of the discussions, the need for a more detailed model analysis was pointed out. Especially for character-based input, it is important to analyze what a deep learning model is able to learn about language - about tokens, morphology or syntax in general. For an efficient and effective understanding of language, it might furthermore be beneficial to share representations learned from multiple objectives to enable the models to focus on their specific understanding task instead of needing to learn syntactic regularities of language first. Therefore, benefits and challenges of transfer learning were an important topic of the working groups as well as of the panel discussion and the final plenary discussion.Thu, 08 Jun 2017 16:14:47 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7248Randomization in Parameterized Complexity (Dagstuhl Seminar 17041)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7247
Dagstuhl Seminar 17041 "Randomization in Parameterized Complexity" took place from January 22nd to January 27th 2017 with the objective to bridge the gap between randomization and parameterized complexity theory. This report documents the talks held during the seminar as well as the open questions arised in the discussion sessions.Thu, 08 Jun 2017 16:14:12 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7247Network Function Virtualization in Software Defined Infrastructures (Dagstuhl Seminar 17032)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7246
The softwarization of networks by introducing concepts such as Software-Defined Networking (SDN) or Network Functions Virtualization (NFV) currently massively changes network management by enabling more flexible communication networks. The main goal of this seminar was to gather researchers from academia, industry, and standardization bodies to discuss a joint perspective on research questions in the field of NFV. This report contains talk summaries, reports on the discussion groups, as well as the personal statements and main challenges contributed by the seminar participants.Thu, 08 Jun 2017 16:13:08 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7246Planning and Robotics (Dagstuhl Seminar 17031)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7245
This report documents the program and the outcomes of Dagstuhl Seminar 17031 on "Planning and Robotics". The seminar was concerned with the synergy between the research areas of Automated Planning & Scheduling and Robotics. The motivation for this seminar was to bring together researchers from the two communities and people from the Industry in order to foster a broader interest in the integration of planning and deliberation approaches to sensory-motor functions in robotics. The first part of the seminar was dedicated to eight sessions composed on several topics in which attendees had the opportunity to present position statements. Then, the second part was composed by six panel sessions where attendees had the opportunity to further discuss the position statements and issues raised in previous sessions. The main outcomes were a greater common understanding of planning and robotics issues and challenges, and a greater appreciation of crossover between different perspectives, i.e., spanning from low level control to high-level cognitive approaches for autonomous robots. Different application domains were also discussed in which the deployment of planning and robotics methodologies and technologies constitute an added value.Thu, 08 Jun 2017 16:10:31 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7245Front Matter, Table of Contents, Foreword, Conference Organization, External Reviewers, Sponsors
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7177
Front Matter, Table of Contents, Foreword, Conference Organization, External Reviewers, SponsorsThu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7177Coloring Curves That Cross a Fixed Curve
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7178
We prove that for every integer t greater than or equal to 1, the class of intersection graphs of curves in the plane each of which crosses a fixed curve in at least one and at most t points is chi-bounded. This is essentially the strongest chi-boundedness result one can get for this kind of graph classes. As a corollary, we prove that for any fixed integers k > 1 and t > 0, every k-quasi-planar topological graph on n vertices with any two edges crossing at most t times has O(n log n) edges.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7178Local Equivalence and Intrinsic Metrics between Reeb Graphs
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7179
As graphical summaries for topological spaces and maps, Reeb graphs are common objects in the computer graphics or topological data analysis literature. Defining good metrics between these objects has become an important question for applications, where it matters to quantify the extent by which two given Reeb graphs differ. Recent contributions emphasize this aspect, proposing novel distances such as functional distortion or interleaving that are provably more discriminative than the so-called bottleneck distance, being true metrics whereas the latter is only a pseudo-metric. Their main drawback compared to the bottleneck distance is to be comparatively hard (if at all possible) to evaluate. Here we take the opposite view on the problem and show that the bottleneck distance is in fact good enough locally, in the sense that it is able to discriminate a Reeb graph from any other Reeb graph in a small enough neighborhood, as efficiently as the other metrics do. This suggests considering the intrinsic metrics induced by these distances, which turn out to be all globally equivalent. This novel viewpoint on the study of Reeb graphs has a potential impact on applications, where one may not only be interested in discriminating between data but also in interpolating between them.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7179Fine-Grained Complexity of Coloring Unit Disks and Balls
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7180
On planar graphs, many classic algorithmic problems enjoy a certain "square root phenomenon" and can be solved significantly faster than what is known to be possible on general graphs: for example, Independent Set, 3-Coloring, Hamiltonian Cycle, Dominating Set can be solved in time 2^O(sqrt{n}) on an n-vertex planar graph, while no 2^o(n) algorithms exist for general graphs, assuming the Exponential Time Hypothesis (ETH). The square root in the exponent seems to be best possible for planar graphs: assuming the ETH, the running time for these problems cannot be improved to 2^o(sqrt{n}). In some cases, a similar speedup can be obtained for 2-dimensional geometric problems, for example, there are 2^O(sqrt{n}log n) time algorithms for Independent Set on unit disk graphs or for TSP on 2-dimensional point sets.In this paper, we explore whether such a speedup is possible for geometric coloring problems. On the one hand, geometric objects can behave similarly to planar graphs: 3-Coloring can be solved in time 2^O(sqrt{n}) on the intersection graph of n unit disks in the plane and, assuming the ETH, there is no such algorithm with running time 2^o(sqrt{n}). On the other hand, if the number L of colors is part of the input, then no such speedup is possible: Coloring the intersection graph of n unit disks with L colors cannot be solved in time 2^o(n), assuming the ETH. More precisely, we exhibit a smooth increase of complexity as the number L of colors increases: If we restrict the number of colors to L=Theta(n^alpha) for some 0<=alpha<=1, then the problem of coloring the intersection graph of n unit disks with L colors* can be solved in time exp(O(n^{{1+alpha}/2}log n))=exp( O(sqrt{nL}log n)), and* cannot be solved in time exp(o(n^{{1+alpha}/2}))=exp(o(sqrt{nL})), unless the ETH fails.More generally, we consider the problem of coloring d-dimensional unit balls in the Euclidean space and obtain analogous results showing that the problem * can be solved in time exp(O(n^{{d-1+alpha}/d}log n))=exp(O(n^{1-1/d}L^{1/d}log n)), and* cannot be solved in time exp(n^{{d-1+alpha}/d-epsilon})= exp (O(n^{1-1/d-epsilon}L^{1/d})) for any epsilon>0, unless the ETH fails.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7180Constrained Triangulations, Volumes of Polytopes, and Unit Equations
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7181
Given a polytope P in R^d and a subset U of its vertices, is there a triangulation of P using d-simplices that all contain U? We answer this question by proving an equivalent and easy-to-check combinatorial criterion for the facets of P. Our proof relates triangulations of P to triangulations of its "shadow", a projection to a lower-dimensional space determined by U. In particular, we obtain a formula relating the volume of P with the volume of its shadow. This leads to an exact formula for the volume of a polytope arising in the theory of unit equations.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7181A Spectral Gap Precludes Low-Dimensional Embeddings
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7182
We prove that if an n-vertex O(1)-expander embeds with average distortion D into a finite dimensional normed space X, then necessarily the dimension of X is at least n^{c/D} for some universal constant c>0. This is sharp up to the value of the constant c, and it improves over the previously best-known estimate dim(X)> c(log n)^2/D^2 of Linial, London and Rabinovich, strengthens a theorem of Matousek, and answers a question of Andoni, Nikolov, Razenshteyn and Waingarten.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7182Computing the Geometric Intersection Number of Curves
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7183
The geometric intersection number of a curve on a surface is the minimal number of self-intersections of any homotopic curve, i.e. of any curve obtained by continuous deformation. Given a curve c represented by a closed walk of length at most l on a combinatorial surface of complexity n we describe simple algorithms to (1) compute the geometric intersection number of c in O(n+ l^2) time, (2) construct a curve homotopic to c that realizes this geometric intersection number in O(n+l^4) time, (3) decide if the geometric intersection number of c is zero, i.e. if c is homotopic to a simple curve, in O(n+l log^2 l) time. To our knowledge, no exact complexity analysis had yet appeared on those problems. An optimistic analysis of the complexity of the published algorithms for problems (1) and (3) gives at best a O(n+g^2l^2) time complexity on a genus g surface without boundary. No polynomial time algorithm was known for problem (2). Interestingly, our solution to problem (3) is the first quasi-linear algorithm since the problem was raised by Poincare more than a century ago. Finally, we note that our algorithm for problem (1) extends to computing the geometric intersection number of two curves of length at most l in O(n+ l^2) time.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7183Computing the Fréchet Gap Distance
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7184
Measuring the similarity of two polygonal curves is a fundamental computational task. Among alternatives, the Frechet distance is one of the most well studied similarity measures. Informally, the Fréchet distance is described as the minimum leash length required for a man on one of the curves to walk a dog on the other curve continuously from the starting to the ending points. In this paper we study a variant called the Fréchet gap distance. In the man and dog analogy, the Fréchet gap distance minimizes the difference of the longest and smallest leash lengths used over the entire walk. This measure in some ways better captures our intuitive notions of curve similarity, for example giving distance zero to translated copies of the same curve.The Fréchet gap distance was originally introduced by Filtser and Katz (2015) in the context of the discrete Fréchet distance. Here we study the continuous version, which presents a number of additional challenges not present in discrete case. In particular, the continuous nature makes bounding and searching over the critical events a rather difficult task.For this problem we give an O(n^5 log(n)) time exact algorithm and a more efficient O(n^2 log(n) + (n^2/epsilon) log(1/epsilon)) time (1+epsilon)-approximation algorithm, where n is the total number of vertices of the input curves. Note that for (small enough) constant epsilon and ignoring logarithmic factors, our approximation has quadratic running time, matching the lower bound, assuming SETH (Bringmann 2014), for approximating the standard Fréchet distance for general curves.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7184A Nearly Quadratic Bound for the Decision Tree Complexity of k-SUM
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7185
We show that the k-SUM problem can be solved by a linear decision tree of depth O(n^2 log^2 n),improving the recent bound O(n^3 log^3 n) of Cardinal et al. Our bound depends linearly on k, and allows us to conclude that the number of linear queries required to decide the n-dimensional Knapsack or SubsetSum problems is only O(n^3 log n), improving the currently best known bounds by a factor of n. Our algorithm extends to the RAM model, showing that the k-SUM problem can be solved in expected polynomial time, for any fixed k, with the above bound on the number of linear queries. Our approach relies on a new point-location mechanism, exploiting "Epsilon-cuttings" that are based on vertical decompositions in hyperplane arrangements in high dimensions. A major side result of the analysis in this paper is a sharper bound on the complexity of the vertical decomposition of such an arrangement (in terms of its dependence on the dimension). We hope that this study will reveal further structural properties of vertical decompositions in hyperplane arrangements.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7185Quickest Visibility Queries in Polygonal Domains
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7186
Let s be a point in a polygonal domain P of h-1 holes and n vertices. We consider the following quickest visibility query problem. Given a query point q in P, the goal is to find a shortest path in P to move from s to see q as quickly as possible. Previously, Arkin et al. (SoCG 2015) built a data structure of size O(n^2 2^alpha(n) log n) that can answer each query in O(K log^2 n) time, where alpha(n) is the inverse Ackermann function and K is the size of the visibility polygon of q in P (and K can be Theta(n) in the worst case). In this paper, we present a new data structure of size O(n log h + h^2) that can answer each query in O(h log h log n) time. Our result improves the previous work when h is relatively small. In particular, if h is a constant, then our result even matches the best result for the simple polygon case (i.e., h = 1), which is optimal. As a by-product, we also have a new algorithm for the following shortest-path-to-segment query problem. Given a query line segment tau in P, the query seeks a shortest path from s to all points of tau. Previously, Arkin et al. gave a data structure of size O(n^2 2^alpha(n) log n) that can answer each query in O(log^2 n) time, and another data structure of size O(n^3 log n) with O(log n) query time. We present a data structure of size O(n) with query time O(h log n/h), which favors small values of h and is optimal when h = O(1).Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7186Bicriteria Rectilinear Shortest Paths among Rectilinear Obstacles in the Plane
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7187
Given a rectilinear domain P of h pairwise-disjoint rectilinear obstacles with a total of n vertices in the plane, we study the problem of computing bicriteria rectilinear shortest paths between two points s and t in P. Three types of bicriteria rectilinear paths are considered: minimum-link shortest paths, shortest minimum-link paths, and minimum-cost paths where the cost of a path is a non-decreasing function of both the number of edges and the length of the path. The one-point and two-point path queries are also considered. Algorithms for these problems have been given previously. Our contributions are threefold. First, we find a critical error in all previous algorithms. Second, we correct the error in a not-so-trivial way. Third, we further improve the algorithms so that they are even faster than the previous (incorrect) algorithms when h is relatively small. For example, for computing a minimum-link shortest s-t path, the previous algorithm runs in O(n log^{3/2} n) time while the time of our new algorithm is O(n + h log^{3/2} h).Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7187On the Number of Ordinary Lines Determined by Sets in Complex Space
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7188
Kelly's theorem states that a set of n points affinely spanning C^3 must determine at least one ordinary complex line (a line passing through exactly two of the points). Our main theorem shows that such sets determine at least 3n/2 ordinary lines, unless the configuration has n-1 points in a plane and one point outside the plane (in which case there are at least n-1 ordinary lines). In addition, when at most n/2 points are contained in any plane, we prove a theorem giving stronger bounds that take advantage of the existence of lines with four and more points (in the spirit of Melchior's and Hirzebruch's inequalities). Furthermore, when the points span four or more dimensions, with at most n/2 points contained in any three dimensional affine subspace, we show that there must be a quadratic number of ordinary lines.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7188Adaptive Planar Point Location
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7189
We present a self-adjusting point location structure for convex subdivisions. Let n be the number of vertices in a convex subdivision S. Our structure for S uses O(n) space and processes any online query sequence sigma in O(n + OPT) time, where OPT is the minimum time required by any linear decision tree for answering point location queries in S to process sigma. The O(n + OPT) time bound includes the preprocessing time. Our result is a two-dimensional analog of the static optimality property of splay trees. For connected subdivisions, we achieve a processing time of O(|sigma| log log n + n + OPT).Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7189High Dimensional Consistent Digital Segments
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7190
We consider the problem of digitalizing Euclidean line segments from R^d to Z^d. Christ {et al.} (DCG, 2012) showed how to construct a set of {consistent digital segments} (CDS) for d=2: a collection of segments connecting any two points in Z^2 that satisfies the natural extension of the Euclidean axioms to Z^d. In this paper we study the construction of CDSs in higher dimensions. We show that any total order can be used to create a set of {consistent digital rays} CDR in Z^d (a set of rays emanating from a fixed point p that satisfies the extension of the Euclidean axioms). We fully characterize for which total orders the construction holds and study their Hausdorff distance, which in particular positively answers the question posed by Christ {et al.}.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7190A Universal Slope Set for 1-Bend Planar Drawings
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7191
We describe a set of Delta-1 slopes that are universal for 1-bend planar drawings of planar graphs of maximum degree Delta>=4; this establishes a new upper bound of Delta-1 on the 1-bend planar slope number. By universal we mean that every planar graph of degree Delta has a planar drawing with at most one bend per edge and such that the slopes of the segments forming the edges belong to the given set of slopes. This improves over previous results in two ways: Firstly, the best previously known upper bound for the 1-bend planar slope number was 3/2(Delta-1) (the known lower bound being 3/4(Delta-1)); secondly, all the known algorithms to construct 1-bend planar drawings with O(Delta) slopes use a different set of slopes for each graph and can have bad angular resolution, while our algorithm uses a universal set of slopes, which also guarantees that the minimum angle between any two edges incident to a vertex is pi/(Delta-1).Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7191Proper Coloring of Geometric Hypergraphs
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7192
We study whether for a given planar family F there is an m such that any finite set of points can be 3-colored such that any member of F that contains at least m points contains two points with different colors. We conjecture that if F is a family of pseudo-disks, then m=3 is sufficient. We prove that when F is the family of all homothetic copies of a given convex polygon, then such an m exists. We also study the problem in higher dimensions.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7192Barcodes of Towers and a Streaming Algorithm for Persistent Homology
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7193
A tower is a sequence of simplicial complexes connected by simplicial maps. We show how to compute a filtration, a sequence of nested simplicial complexes, with the same persistent barcode as the tower. Our approach is based on the coning strategy by Dey et al. (SoCG 2014). We show that a variant of this approach yields a filtration that is asymptotically only marginally larger than the tower and can be efficiently computed by a streaming algorithm, both in theory and in practice. Furthermore, we show that our approach can be combined with a streaming algorithm to compute the barcode of the tower via matrix reduction. The space complexity of the algorithm does not depend on the length of the tower, but the maximal size of any subcomplex within the tower. Experimental evaluations show that our approach can efficiently handle towers with billions of complexes.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7193Irrational Guards are Sometimes Needed
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7194
In this paper we study the art gallery problem, which is one of the fundamental problems in computational geometry. The objective is to place a minimum number of guards inside a simple polygon so that the guards together can see the whole polygon. We say that a guard at position x sees a point y if the line segment xy is contained in the polygon.Despite an extensive study of the art gallery problem, it remained an open question whether there are polygons given by integer coordinates that require guard positions with irrational coordinates in any optimal solution. We give a positive answer to this question by constructing a monotone polygon with integer coordinates that can be guarded by three guards only when we allow to place the guards at points with irrational coordinates. Otherwise, four guards are needed. By extending this example, we show that for every n, there is a polygon which can be guarded by 3n guards with irrational coordinates but needs 4n guards if the coordinates have to be rational. Subsequently, we show that there are rectilinear polygons given by integer coordinates that require guards with irrational coordinates in any optimal solution.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7194Covering Lattice Points by Subspaces and Counting Point-Hyperplane Incidences
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7195
Let d and k be integers with 1 <= k <= d-1. Let Lambda be a d-dimensional lattice and let K be a d-dimensional compact convex body symmetric about the origin. We provide estimates for the minimum number of k-dimensional linear subspaces needed to cover all points in the intersection of Lambda with K. In particular, our results imply that the minimum number of k-dimensional linear subspaces needed to cover the d-dimensional n * ... * n grid is at least Omega(n^(d(d-k)/(d-1)-epsilon)) and at most O(n^(d(d-k)/(d-1))), where epsilon > 0 is an arbitrarily small constant. This nearly settles a problem mentioned in the book of Brass, Moser, and Pach. We also find tight bounds for the minimum number of k-dimensional affine subspaces needed to cover the intersection of Lambda with K.We use these new results to improve the best known lower bound for the maximum number of point-hyperplane incidences by Brass and Knauer. For d > =3 and epsilon in (0,1), we show that there is an integer r=r(d,epsilon) such that for all positive integers n, m the following statement is true. There is a set of n points in R^d and an arrangement of m hyperplanes in R^d with no K_(r,r) in their incidence graph and with at least Omega((mn)^(1-(2d+3)/((d+2)(d+3)) - epsilon)) incidences if d is odd and Omega((mn)^(1-(2d^2+d-2)/((d+2)(d^2+2d-2)) - epsilon)) incidences if d is even.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7195Disjointness Graphs of Segments
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7196
The disjointness graph G=G(S) of a set of segments S in R^d, d>1 is a graph whose vertex set is S and two vertices are connected by an edge if and only if the corresponding segments are disjoint. We prove that the chromatic number of G satisfies chi(G)<=omega(G)^4+omega(G)^3 where omega(G) denotes the clique number of G. It follows, that S has at least cn^{1/5} pairwise intersecting or pairwise disjoint elements. Stronger bounds are established for lines in space, instead of segments.We show that computing omega(G) and chi(G) for disjointness graphs of lines in space are NP-hard tasks. However, we can design efficient algorithms to compute proper colorings of G in which the number of colors satisfies the above upper bounds. One cannot expect similar results for sets of continuous arcs, instead of segments, even in the plane. We construct families of arcs whose disjointness graphs are triangle-free (omega(G)=2), but whose chromatic numbers are arbitrarily large.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7196Exact Algorithms for Terrain Guarding
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7197
Given a 1.5-dimensional terrain T, also known as an x-monotone polygonal chain, the Terrain Guarding problem seeks a set of points of minimum size on T that guards all of the points on T. Here, we say that a point p guards a point q if no point of the line segment pq is strictly below T. The Terrain Guarding problem has been extensively studied for over 20 years. In 2005 it was already established that this problem admits a constant-factor approximation algorithm [SODA 2005]. However, only in 2010 King and Krohn [SODA 2010] finally showed that Terrain Guarding is NP-hard. In spite of the remarkable developments in approximation algorithms for Terrain Guarding, next to nothing is known about its parameterized complexity. In particular, the most intriguing open questions in this direction ask whether it admits a subexponential-time algorithm and whether it is fixed-parameter tractable. In this paper, we answer the first question affirmatively by developing an n^O(sqrt{k})-time algorithm for both Discrete Terrain Guarding and Continuous Terrain Guarding. We also make non-trivial progress with respect to the second question: we show that Discrete Orthogonal Terrain Guarding, a well-studied special case of Terrain Guarding, is fixed-parameter tractable.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7197Topological Data Analysis with Bregman Divergences
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7198
We show that the framework of topological data analysis can be extended from metrics to general Bregman divergences, widening the scope of possible applications. Examples are the Kullback-Leibler divergence, which is commonly used for comparing text and images, and the Itakura-Saito divergence, popular for speech and sound. In particular, we prove that appropriately generalized Cech and Delaunay (alpha) complexes capture the correct homotopy type, namely that of the corresponding union of Bregman balls. Consequently, their filtrations give the correct persistence diagram, namely the one generated by the uniformly growing Bregman balls. Moreover, we show that unlike the metric setting, the filtration of Vietoris-Rips complexes may fail to approximate the persistence diagram. We propose algorithms to compute the thus generalized Cech, Vietoris-Rips and Delaunay complexes and experimentally test their efficiency. Lastly, we explain their surprisingly good performance by making a connection with discrete Morse theory.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7198Shallow Packings, Semialgebraic Set Systems, Macbeath Regions, and Polynomial Partitioning
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7199
The packing lemma of Haussler states that given a set system (X,R) with bounded VC dimension, if every pair of sets in R have large symmetric difference, then R cannot contain too many sets. Recently it was generalized to the shallow packing lemma, applying to set systems as a function of their shallow-cell complexity.In this paper we present several new results and applications related to packings:* an optimal lower bound for shallow packings,* improved bounds on Mnets, providing a combinatorial analogue to Macbeath regions in convex geometry, * we observe that Mnets provide a general, more powerful framework from which the state-of-the-art unweighted epsilon-net results follow immediately, and * simplifying and generalizing one of the main technical tools in [Fox et al. , J. of the EMS, to appear].Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7199A Superlinear Lower Bound on the Number of 5-Holes
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7200
Let P be a finite set of points in the plane in general position, that is, no three points of P are on a common line. We say that a set H of five points from P is a 5-hole in P if H is the vertex set of a convex 5-gon containing no other points of P. For a positive integer n, let h_5(n) be the minimum number of 5-holes among all sets of n points in the plane in general position.Despite many efforts in the last 30 years, the best known asymptotic lower and upper bounds for h_5(n) have been of order Omega(n) and O(n^2), respectively. We show that h_5(n) = Omega(n(log n)^(4/5)), obtaining the first superlinear lower bound on h_5(n).The following structural result, which might be of independent interest, is a crucial step in the proof of this lower bound. If a finite set P of points in the plane in general position is partitioned by a line l into two subsets, each of size at least 5 and not in convex position, then l intersects the convex hull of some 5-hole in P. The proof of this result is computer-assisted.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7200Maximum Volume Subset Selection for Anchored Boxes
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7201
Let B be a set of n axis-parallel boxes in d-dimensions such that each box has a corner at the origin and the other corner in the positive quadrant, and let k be a positive integer. We study the problem of selecting k boxes in B that maximize the volume of the union of the selected boxes. The research is motivated by applications in skyline queries for databases and in multicriteria optimization, where the problem is known as the hypervolume subset selection problem. It is known that the problem can be solved in polynomial time in the plane, while the best known algorithms in any dimension d>2 enumerate all size-k subsets. We show that:* The problem is NP-hard already in 3 dimensions.* In 3 dimensions, we break the enumeration of all size-k subsets, by providing an n^O(sqrt(k)) algorithm.* For any constant dimension d, we give an efficient polynomial-time approximation scheme.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7201Reachability in a Planar Subdivision with Direction Constraints
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7202
Given a planar subdivision with n vertices, each face having a cone of possible directions of travel, our goal is to decide which vertices of the subdivision can be reached from a given starting point s. We give an O(n log n)-time algorithm for this problem, as well as an Omega(n log n) lower bound in the algebraic computation tree model. We prove that the generalization where two cones of directions per face are allowed is NP-hard.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7202Locality-Sensitive Hashing of Curves
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7203
We study data structures for storing a set of polygonal curves in R^d such that, given a query curve, we can efficiently retrieve similar curves from the set, where similarity is measured using the discrete Fréchet distance or the dynamic time warping distance. To this end we devise the first locality-sensitive hashing schemes for these distance measures. A major challenge is posed by the fact that these distance measures internally optimize the alignment between the curves. We give solutions for different types of alignments including constrained and unconstrained versions. For unconstrained alignments, we improve over a result by Indyk [SoCG 2002] for short curves. Let n be the number of input curves and let m be the maximum complexity of a curve in the input. In the particular case where m <= (a/(4d)) log n, for some fixed a>0, our solutions imply an approximate near-neighbor data structure for the discrete Fréchet distance that uses space in O(n^(1+a) log n) and achieves query time in O(n^a log^2 n) and constant approximation factor. Furthermore, our solutions provide a trade-off between approximation quality and computational performance: for any parameter k in [m], we can give a data structure that uses space in O(2^(2k) m^(k-1) n log n + nm), answers queries in O( 2^(2k) m^(k) log n) time and achieves approximation factor in O(m/k).Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7203Minimum Perimeter-Sum Partitions in the Plane
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7204
Let P be a set of n points in the plane. We consider the problem of partitioning P into two subsets P_1 and P_2 such that the sum of the perimeters of CH(P_1) and CH(P_2) is minimized, where CH(P_i) denotes the convex hull of P_i. The problem was first studied by Mitchell and Wynters in 1991 who gave an O(n^2) time algorithm. Despite considerable progress on related problems, no subquadratic time algorithm for this problem was found so far. We present an exact algorithm solving the problem in O(n log^4 n) time and a (1+e)-approximation algorithm running in O(n + 1/e^2 log^4(1/e)) time.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7204Best Laid Plans of Lions and Men
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7205
We answer the following question dating back to J.E. Littlewood (1885-1977): Can two lions catch a man in a bounded area with rectifiable lakes? The lions and the man are all assumed to be points moving with at most unit speed. That the lakes are rectifiable means that their boundaries are finitely long. This requirement is to avoid pathological examples where the man survives forever because any path to the lions is infinitely long. We show that the answer to the question is not always "yes", by giving an example of a region R in the plane where the man has a strategy to survive forever. R is a polygonal region with holes and the exterior and interior boundaries are pairwise disjoint, simple polygons. Our construction is the first truly two-dimensional example where the man can survive.Next, we consider the following game played on the entire plane instead of a bounded area: There is any finite number of unit speed lions and one fast man who can run with speed 1+epsilon for some value epsilon>0. Can the man always survive? We answer the question in the affirmative for any constant epsilon>0.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7205Anisotropic Triangulations via Discrete Riemannian Voronoi Diagrams
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7206
The construction of anisotropic triangulations is desirable for various applications, such as the numerical solving of partial differential equations and the representation of surfaces in graphics. To solve this notoriously difficult problem in a practical way, we introduce the discrete Riemannian Voronoi diagram, a discrete structure that approximates the Riemannian Voronoi diagram. This structure has been implemented and was shown to lead to good triangulations in R^2 and on surfaces embedded in R^3 as detailed in our experimental companion paper.In this paper, we study theoretical aspects of our structure. Given a finite set of points P in a domain Omega equipped with a Riemannian metric, we compare the discrete Riemannian Voronoi diagram of P to its Riemannian Voronoi diagram. Both diagrams have dual structures called the discrete Riemannian Delaunay and the Riemannian Delaunay complex. We provide conditions that guarantee that these dual structures are identical. It then follows from previous results that the discrete Riemannian Delaunay complex can be embedded in Omega under sufficient conditions, leading to an anisotropic triangulation with curved simplices. Furthermore, we show that, under similar conditions, the simplices of this triangulation can be straightened.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7206A Proof of the Orbit Conjecture for Flipping Edge-Labelled Triangulations
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7207
Given a triangulation of a point set in the plane, a flip deletes an edge e whose removal leaves a convex quadrilateral, and replaces e by the opposite diagonal of the quadrilateral. It is well known that any triangulation of a point set can be reconfigured to any other triangulation by some sequence of flips. We explore this question in the setting where each edge of a triangulation has a label, and a flip transfers the label of the removed edge to the new edge. It is not true that every labelled triangulation of a point set can be reconfigured to every other labelled triangulation via a sequence of flips, but we characterize when this is possible. There is an obvious necessary condition: for each label l, if edge e has label l in the first triangulation and edge f has label l in the second triangulation, then there must be some sequence of flips that moves label l from e to f, ignoring all other labels. Bose, Lubiw, Pathak and Verdonschot formulated the Orbit Conjecture, which states that this necessary condition is also sufficient, i.e. that all labels can be simultaneously mapped to their destination if and only if each label individually can be mapped to its destination. We prove this conjecture. Furthermore, we give a polynomial-time algorithm to find a sequence of flips to reconfigure one labelled triangulation to another, if such a sequence exists, and we prove an upper bound of O(n^7) on the length of the flip sequence. Our proof uses the topological result that the sets of pairwise non-crossing edges on a planar point set form a simplicial complex that is homeomorphic to a high-dimensional ball (this follows from a result of Orden and Santos; we give a different proof based on a shelling argument). The dual cell complex of this simplicial ball, called the flip complex, has the usual flip graph as its 1-skeleton. We use properties of the 2-skeleton of the flip complex to prove the Orbit Conjecture.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7207On Bend-Minimized Orthogonal Drawings of Planar 3-Graphs
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7208
An orthogonal drawing of a graph is a planar drawing where each edge is drawn as a sequence of horizontal and vertical line segments. Finding a bend-minimized orthogonal drawing of a planar graph of maximum degree 4 is NP-hard. The problem becomes tractable for planar graphs of maximum degree 3, and the fastest known algorithm takes O(n^5 log n) time. Whether a faster algorithm exists has been a long-standing open problem in graph drawing. In this paper we present an algorithm that takes only O~(n^{17/7}) time, which is a significant improvement over the previous state of the art.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7208On Planar Greedy Drawings of 3-Connected Planar Graphs
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7209
A graph drawing is greedy if, for every ordered pair of vertices (x,y), there is a path from x to y such that the Euclidean distance to y decreases monotonically at every vertex of the path. Greedy drawings support a simple geometric routing scheme, in which any node that has to send a packet to a destination "greedily" forwards the packet to any neighbor that is closer to the destination than itself, according to the Euclidean distance in the drawing. In a greedy drawing such a neighbor always exists and hence this routing scheme is guaranteed to succeed. In 2004 Papadimitriou and Ratajczak stated two conjectures related to greedy drawings. The greedy embedding conjecture states that every 3-connected planar graph admits a greedy drawing. The convex greedy embedding conjecture asserts that every 3-connected planar graph admits a planar greedy drawing in which the faces are delimited by convex polygons. In 2008 the greedy embedding conjecture was settled in the positive by Leighton and Moitra. In this paper we prove that every 3-connected planar graph admits a planar greedy drawing. Apart from being a strengthening of Leighton and Moitra's result, this theorem constitutes a natural intermediate step towards a proof of the convex greedy embedding conjecture.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7209From Crossing-Free Graphs on Wheel Sets to Embracing Simplices and Polytopes with Few Vertices
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7210
A set P = H cup {w} of n+1 points in the plane is called a wheel set if all points but w are extreme. We show that for the purpose of counting crossing-free geometric graphs on P, it suffices to know the so-called frequency vector of P. While there are roughly 2^n distinct order types that correspond to wheel sets, the number of frequency vectors is only about 2^{n/2}. We give simple formulas in terms of the frequency vector for the number of crossing-free spanning cycles, matchings, w-embracing triangles, and many more. Based on these formulas, the corresponding numbers of graphs can be computed efficiently. Also in higher dimensions, wheel sets turn out to be a suitable model to approach the problem of computing the simplicial depth of a point w in a set H, i.e., the number of simplices spanned by H that contain w. While the concept of frequency vectors does not generalize easily, we show how to apply similar methods in higher dimensions. The result is an O(n^{d-1}) time algorithm for computing the simplicial depth of a point w in a set H of n d-dimensional points, improving on the previously best bound of O(n^d log n). Configurations equivalent to wheel sets have already been used by Perles for counting the faces of high-dimensional polytopes with few vertices via the Gale dual. Based on that we can compute the number of facets of the convex hull of n=d+k points in general position in R^d in time O(n^max(omega,k-2)) where omega = 2.373, even though the asymptotic number of facets may be as large as n^k.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7210A Quest to Unravel the Metric Structure Behind Perturbed Networks
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7211
Graphs and network data are ubiquitous across a wide spectrum of scientific and application domains. Often in practice, an input graph can be considered as an observed snapshot of a (potentiallycontinuous) hidden domain or process. Subsequent analysis, processing, and inferences are then performed on this observed graph. In this paper we advocate the perspective that an observed graph is often a noisy version of some discretized 1-skeleton of a hidden domain, and specifically we will consider the following natural network model: We assume that there is a true graph G^* which is a certain proximity graph for points sampled from a hidden domain X; while the observed graph G is an Erdos-Renyi type perturbed version of G^*.Our network model is related to, and slightly generalizes, the much-celebrated small-world network model originally proposed by Watts and Strogatz. However, the main question we aim to answer is orthogonal to the usual studies of network models (which often focuses on characterizing / predicting behaviors and properties of real-world networks). Specifically, we aim to recover the metric structure of G^* (which reflects that of the hidden space X as we will show) from the observed graph G. Our main result is that a simple filtering process based on the Jaccard index can recover this metric within a multiplicative factor of 2 under our network model. Our work makes one step towards the general question of inferring structure of a hidden space from its observed noisy graph representation. In addition, our results also provide a theoretical understanding for Jaccard-Index-based denoising approaches.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7211Algorithmic Interpretations of Fractal Dimension
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7212
We study algorithmic problems on subsets of Euclidean space of low fractal dimension. These spaces are the subject of intensive study in various branches of mathematics, including geometry, topology, and measure theory. There are several well-studied notions of fractal dimension for sets and measures in Euclidean space. We consider a definition of fractal dimension for finite metric spaces which agrees with standard notions used to empirically estimate the fractal dimension of various sets. We define the fractal dimension of some metric space to be the infimum delta>0, such that for any eps>0, for any ball B of radius r >= 2eps, and for any eps-net N, we have |B cap N|=O((r/eps)^delta).Using this definition we obtain faster algorithms for a plethora of classical problems on sets of low fractal dimension in Euclidean space. Our results apply to exact and fixed-parameter algorithms, approximation schemes, and spanner constructions. Interestingly, the dependence of the performance of these algorithms on the fractal dimension nearly matches the currently best-known dependence on the standard Euclidean dimension. Thus, when the fractal dimension is strictly smaller than the ambient dimension, our results yield improved solutions in all of these settings.We remark that our definition of fractal definition is equivalent up to constant factors to the well-studied notion of doubling dimension.However, in the problems that we consider, the dimension appears in the exponent of the running time, and doubling dimension is not precise enough for capturing the best possible such exponent for subsets of Euclidean space. Thus our work is orthogonal to previous results on spaces of low doubling dimension; while algorithms on spaces of low doubling dimension seek to extend results from the case of low dimensional Euclidean spaces to more general metric spaces, our goal is to obtain faster algorithms for special pointsets in Euclidean space.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7212Declutter and Resample: Towards Parameter Free Denoising
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7213
In many data analysis applications the following scenario is commonplace: we are given a point set that is supposed to sample a hidden ground truth K in a metric space, but it got corrupted with noise so that some of the data points lie far away from K creating outliers also termed as ambient noise. One of the main goals of denoising algorithms is to eliminate such noise so that the curated data lie within a bounded Hausdorff distance of K. Popular denoising approaches such as deconvolution and thresholding often require the user to set several parameters and/or to choose an appropriate noise model while guaranteeing only asymptotic convergence. Our goal is to lighten this burden as much as possible while ensuring theoretical guarantees in all cases.Specifically, first, we propose a simple denoising algorithm that requires only a single parameter but provides a theoretical guarantee on the quality of the output on general input points. We argue that this single parameter cannot be avoided. We next present a simple algorithm that avoids even this parameter by paying for it with a slight strengthening of the sampling condition on the input points which is not unrealistic. We also provide some preliminary empirical evidence that our algorithmsare effective in practice. Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7213Range-Clustering Queries
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7214
In a geometric k-clustering problem the goal is to partition a set of points in R^d into k subsets such that a certain cost function of the clustering is minimized. We present data structures for orthogonal range-clustering queries on a point set S: given a query box Q and an integer k > 2, compute an optimal k-clustering for the subset of S inside Q. We obtain the following results.* We present a general method to compute a (1+epsilon)-approximation to a range-clustering query, where epsilon>0 is a parameter that can be specified as part of the query. Our method applies to a large class of clustering problems, including k-center clustering in any Lp-metric and a variant of k-center clustering where the goal is to minimize the sum (instead of maximum) of the cluster sizes.* We extend our method to deal with capacitated k-clustering problems, where each of the clusters should not contain more than a given number of points. * For the special cases of rectilinear k-center clustering in R^1, and in R^2 for k = 2 or 3, we present data structures that answer range-clustering queries exactly. Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7214An Approximation Algorithm for the Art Gallery Problem
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7215
Given a simple polygon P on n vertices, two points x, y in P are said to be visible to each other if the line segment between x and y is contained in P. The Point Guard Art Gallery problem asks for a minimum-size set S such that every point in P is visible from a point in S. The set S is referred to as guards. Assuming integer coordinates and a specific general position on the vertices of P, we present the first O(log OPT)-approximation algorithm for the point guard problem. This algorithm combines ideas in papers of Efrat and Har-Peled and Deshpande et al. We also point out a mistake in the latter.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7215Self-Approaching Paths in Simple Polygons
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7216
We study self-approaching paths that are contained in a simple polygon. A self-approaching path is a directed curve connecting two points such that the Euclidean distance between a point moving along the path and any future position does not increase, that is, for all points a, b, and c that appear in that order along the curve, |ac| >= |bc|. We analyze the properties, and present a characterization of shortest self-approaching paths. In particular, we show that a shortest self-approaching path connecting two points inside a polygon can be forced to follow a general class of non-algebraic curves. While this makes it difficult to design an exact algorithm, we show how to find a self-approaching path inside a polygon connecting two points under a model of computation which assumes that we can calculate involute curves of high order.Lastly, we provide an algorithm to test if a given simple polygon is self-approaching, that is, if there exists a self-approaching path for any two points inside the polygon.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7216Implementing Delaunay Triangulations of the Bolza Surface
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7217
The CGAL library offers software packages to compute Delaunay triangulations of the (flat) torus of genus one in two and three dimensions. To the best of our knowledge, there is no available software for the simplest possible extension, i.e., the Bolza surface, a hyperbolic manifold homeomorphic to a torus of genus two. In this paper, we present an implementation based on the theoretical results and the incremental algorithm proposed last year at SoCG by Bogdanov, Teillaud, and Vegter. We describe the representation of the triangulation, we detail the different steps of the algorithm, we study predicates, and report experimental results. Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7217Voronoi Diagrams for a Moderate-Sized Point-Set in a Simple Polygon
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7218
Given a set of sites in a simple polygon, a geodesic Voronoi diagram partitions the polygon into regions based on distances to sites under the geodesic metric. We present algorithms for computing the geodesic nearest-point, higher-order and farthest-point Voronoi diagrams of m point sites in a simple n-gon, which improve the best known ones for m < n/polylog n. Moreover, the algorithms for the nearest-point and farthest-point Voronoi diagrams are optimal for m < n/polylog n. This partially answers a question posed by Mitchell in the Handbook of Computational Geometry.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7218Dynamic Geodesic Convex Hulls in Dynamic Simple Polygons
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7219
We consider the geodesic convex hulls of points in a simple polygonal region in the presence of non-crossing line segments (barriers) that subdivide the region into simply connected faces. We present an algorithm together with data structures for maintaining the geodesic convex hull of points in each face in a sublinear update time under the fully-dynamic setting where both input points and barriers change by insertions and deletions. The algorithm processes a mixed update sequence of insertions and deletions of points and barriers. Each update takes O(n^2/3 log^2 n) time with high probability, where n is the total number of the points and barriers at the moment. Our data structures support basic queries on the geodesic convex hull, each of which takes O(polylog n) time. In addition, we present an algorithm together with data structures for geodesic triangle counting queries under the fully-dynamic setting. With high probability, each update takes O(n^2/3 log n) time, and each query takes O(n^2/3 log n) time.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7219Computing Representative Networks for Braided Rivers
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7220
Drainage networks on terrains have been studied extensively from an algorithmic perspective. However, in drainage networks water flow cannot bifurcate and hence they do not model braided rivers (multiple channels which split and join, separated by sediment bars). We initiate the algorithmic study of braided rivers by employing the descending quasi Morse-Smale complex on the river bed (a polyhedral terrain), and extending it with a certain ordering of bars from the one river bank to the other. This allows us to compute a graph that models a representative channel network, consisting of lowest paths. To ensure that channels in this network are sufficiently different we define a sand function that represents the volume of sediment separating them. We show that in general the problem of computing a maximum network of non-crossing channels which are delta-different from each other (as measured by the sand function) is NP-hard. However, using our ordering between the river banks, we can compute a maximum delta-different network that respects this order in polynomial time. We implemented our approach and applied it to simulated and real-world braided rivers.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7220Subquadratic Algorithms for Algebraic Generalizations of 3SUM
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7221
The 3SUM problem asks if an input n-set of real numbers contains a triple whose sum is zero. We consider the 3POL problem, a natural generalization of 3SUM where we replace the sum function by a constant-degree polynomial in three variables. The motivations are threefold. Raz, Sharir, and de Zeeuw gave an O(n^{11/6}) upper bound on the number of solutions of trivariate polynomial equations when the solutions are taken from the cartesian product of three n-sets of real numbers. We give algorithms for the corresponding problem of counting such solutions. Grønlund and Pettie recently designed subquadratic algorithms for 3SUM. We generalize their results to 3POL. Finally, we shed light on the General Position Testing (GPT) problem: "Given n points in the plane, do three of them lie on a line?", a key problem in computational geometry.We prove that there exist bounded-degree algebraic decision trees of depth O(n^{12/7+e}) that solve 3POL, and that 3POL can be solved in O(n^2 (log log n)^{3/2} / (log n)^{1/2}) time in the real-RAM model. Among the possible applications of those results, we show how to solve GPT in subquadratic time when the input points lie on o((log n)^{1/6}/(log log n)^{1/2}) constant-degree polynomial curves. This constitutes the first step towards closing the major open question of whether GPT can be solved in subquadratic time. To obtain these results, we generalize important tools - such as batch range searching and dominance reporting - to a polynomial setting. We expect these new tools to be useful in other applications.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7221Topological Analysis of Nerves, Reeb Spaces, Mappers, and Multiscale Mappers
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7222
Data analysis often concerns not only the space where data come from, but also various types of maps attached to data. In recent years, several related structures have been used to study maps on data, including Reeb spaces, mappers and multiscale mappers. The construction of these structures also relies on the so-called nerve of a cover of the domain.In this paper, we aim to analyze the topological information encoded in these structures in order to provide better understanding of these structures and facilitate their practical usage.More specifically, we show that the one-dimensional homology of the nerve complex N(U) of a path-connected cover U of a domain X cannot be richer than that of the domain X itself. Intuitively, this result means that no new H_1-homology class can be "created" under a natural map from X to the nerve complex N(U). Equipping X with a pseudometric d, we further refine this result and characterize the classes of H_1(X) that may survive in the nerve complex using the notion of size of the covering elements in U. These fundamental results about nerve complexes then lead to an analysis of the H_1-homology of Reeb spaces, mappers and multiscale mappers.The analysis of H_1-homology groups unfortunately does not extend to higher dimensions. Nevertheless, by using a map-induced metric, establishing a Gromov-Hausdorff convergence result between mappers and the domain, and interleaving relevant modules, we can still analyze the persistent homology groups of (multiscale) mappers to establish a connection to Reeb spaces. Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7222Towards a Topology-Shape-Metrics Framework for Ortho-Radial Drawings
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7223
Ortho-Radial drawings are a generalization of orthogonal drawings to grids that are formed by concentric circles and straight-line spokes emanating from the circles' center. Such drawings have applications in schematic graph layouts, e.g., for metro maps and destination maps.A plane graph is a planar graph with a fixed planar embedding. We give a combinatorial characterization of the plane graphs that admit a planar ortho-radial drawing without bends. Previously, such a characterization was only known for paths, cycles, and theta graphs, and in the special case of rectangular drawings for cubic graphs, where the contour of each face is required to be a rectangle.The characterization is expressed in terms of an ortho-radial representation that, similar to Tamassia's orthogonal representations for orthogonal drawings describes such a drawing combinatorially in terms of angles around vertices and bends on the edges. In this sense our characterization can be seen as a first step towards generalizing the Topology-Shape-Metrics framework of Tamassia to ortho-radial drawings.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7223Erdös-Hajnal Conjecture for Graphs with Bounded VC-Dimension
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7224
The Vapnik-Chervonenkis dimension (in short, VC-dimension) of a graph is defined as the VC-dimension of the set system induced by the neighborhoods of its vertices. We show that every n-vertex graph with bounded VC-dimension contains a clique or an independent set of size at least e^{(log n)^{1 - o(1)}}. The dependence on the VC-dimension is hidden in the o(1) term. This improves the general lower bound, e^{c sqrt{log n}}, due to Erdos and Hajnal, which is valid in the class of graphs satisfying any fixed nontrivial hereditary property. Our result is almost optimal and nearly matches the celebrated Erdos-Hajnal conjecture, according to which one can always find a clique or an independent set of size at least e^{Omega(log n)}. Our results partially explain why most geometric intersection graphs arising in discrete and computational geometry have exceptionally favorable Ramsey-type properties.Our main tool is a partitioning result found by Lovasz-Szegedy and Alon-Fischer-Newman, which is called the "ultra-strong regularity lemma" for graphs with bounded VC-dimension. We extend this lemma to k-uniform hypergraphs, and prove that the number of parts in the partition can be taken to be (1/epsilon)^{O(d)}, improving the original bound of (1/epsilon)^{O(d^2)} in the graph setting. We show that this bound is tight up to an absolute constant factor in the exponent. Moreover, we give an O(n^k)-time algorithm for finding a partition meeting the requirements in the k-uniform setting.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7224Near-Optimal epsilon-Kernel Construction and Related Problems
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7225
The computation of (i) eps-kernels, (ii) approximate diameter, and (iii) approximate bichromatic closest pair are fundamental problems in geometric approximation. In each case the input is a set of points in d-dimensional space for a constant d and an approximation parameter eps > 0. In this paper, we describe new algorithms for these problems, achieving significant improvements to the exponent of the eps-dependency in their running times, from roughly d to d/2 for the first two problems and from roughly d/3 to d/4 for problem (iii).These results are all based on an efficient decomposition of a convex body using a hierarchy of Macbeath regions, and contrast to previous solutions that decomposed the space using quadtrees and grids. By further application of these techniques, we also show that it is possible to obtain near-optimal preprocessing time for the most efficient data structures for (iv) approximate nearest neighbor searching, (v) directional width queries, and (vi) polytope membership queries.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7225Orthogonal Range Searching in Moderate Dimensions: k-d Trees and Range Trees Strike Back
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7226
We revisit the orthogonal range searching problem and the exact l_infinity nearest neighbor searching problem for a static set of n points when the dimension d is moderately large. We give the first data structure with near linear space that achieves truly sublinear query time when the dimension is any constant multiple of log n. Specifically, the preprocessing time and space are O(n^{1+delta}) for any constant delta>0, and the expected query time is n^{1-1/O(c log c)} for d = c log n. The data structure is simple and is based on a new "augmented, randomized, lopsided" variant of k-d trees. It matches (in fact, slightly improves) the performance of previous combinatorial algorithms that work only in the case of offline queries [Impagliazzo, Lovett, Paturi, and Schneider (2014) and Chan (SODA'15)]. It leads to slightly faster combinatorial algorithms for all-pairs shortest paths in general real-weighted graphs and rectangular Boolean matrix multiplication.In the offline case, we show that the problem can be reduced to the Boolean orthogonal vectors problem and thus admits an n^{2-1/O(log c)}-time non-combinatorial algorithm [Abboud, Williams, and Yu (SODA'15)]. This reduction is also simple and is based on range trees.Finally, we use a similar approach to obtain a small improvement to Indyk's data structure [FOCS'98] for approximate l_infinity nearest neighbor search when d = c log n.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7226Applications of Chebyshev Polynomials to Low-Dimensional Computational Geometry
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7227
We apply the polynomial method - specifically, Chebyshev polynomials - to obtain a number of new results on geometric approximation algorithms in low constant dimensions. For example, we give an algorithm for constructing epsilon-kernels (coresets for approximate width and approximate convex hull) in close to optimal time O(n + (1/epsilon)^{(d-1)/2}), up to a small near-(1/epsilon)^{3/2} factor, for any d-dimensional n-point set. We obtain an improved data structure for Euclidean *approximate nearest neighbor search* with close to O(n log n + (1/epsilon)^{d/4} n) preprocessing time and O((1/epsilon)^{d/4} log n) query time. We obtain improved approximation algorithms for discrete Voronoi diagrams, diameter, and bichromatic closest pair in the L_s-metric for any even integer constant s >= 2. The techniques are general and may have further applications.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7227Finding Small Hitting Sets in Infinite Range Spaces of Bounded VC-Dimension
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7228
We consider the problem of finding a small hitting set in an infinite range space F=(Q,R) of bounded VC-dimension. We show that, under reasonably general assumptions, the infinite-dimensional convex relaxation can be solved (approximately) efficiently by multiplicative weight updates. As a consequence, we get an algorithm that finds, for any delta>0, a set of size O(s_F(z^*_F)) that hits (1-delta)-fraction of R (with respect to a given measure) in time proportional to log(1/delta), where s_F(1/epsilon) is the size of the smallest epsilon-net the range space admits, and z^*_F is the value of the fractional optimal solution. This exponentially improves upon previous results which achieve the same approximation guarantees with running time proportional to poly(1/delta). Our assumptions hold, for instance, in the case when the range space represents the visibility regions of a polygon in the plane, giving thus a deterministic polynomial-time O(log z^*_F)-approximation algorithm for guarding (1-delta)-fraction of the area of any given simple polygon, with running time proportional to polylog(1/delta). Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7228Dynamic Orthogonal Range Searching on the RAM, Revisited
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7229
We study a longstanding problem in computational geometry: 2-d dynamic orthogonal range reporting. We present a new data structure achieving O(log n / log log n + k) optimal query time and O(log^{2/3+o(1)}n) update time (amortized) in the word RAM model, where n is the number of data points and k is the output size. This is the first improvement in over 10 years of Mortensen's previous result [SIAM J. Comput., 2006], which has O(log^{7/8+epsilon}n) update time for an arbitrarily small constant epsilon.In the case of 3-sided queries, our update time reduces to O(log^{1/2+epsilon}n), improving Wilkinson's previous bound [ESA 2014] of O(log^{2/3+epsilon}n).Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7229On Optimal 2- and 3-Planar Graphs
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7230
A graph is k-planar if it can be drawn in the plane such that no edge is crossed more than k times. While for k=1, optimal 1-planar graphs, i.e., those with n vertices and exactly 4n-8 edges, have been completely characterized, this has not been the case for k > 1. For k=2,3 and 4, upper bounds on the edge density have been developed for the case of simple graphs by Pach and Tóth, Pach et al. and Ackerman, which have been used to improve the well-known "Crossing Lemma". Recently, we proved that these bounds also apply to non-simple 2- and 3-planar graphs without homotopic parallel edges and self-loops.In this paper, we completely characterize optimal 2- and 3-planar graphs, i.e., those that achieve the aforementioned upper bounds. We prove that they have a remarkably simple regular structure, although they might be non-simple. The new characterization allows us to develop notable insights concerning new inclusion relationships with other graph classes.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7230Origamizer: A Practical Algorithm for Folding Any Polyhedron
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7231
It was established at SoCG'99 that every polyhedral complex can be folded from a sufficiently large square of paper, but the known algorithms are extremely impractical, wasting most of the material and making folds through many layers of paper. At a deeper level, these foldings get the topology wrong, introducing many gaps (boundaries) in the surface, which results in flimsy foldings in practice. We develop a new algorithm designed specifically for the practical folding of real paper into complicated polyhedral models. We prove that the algorithm correctly folds any oriented polyhedral manifold, plus an arbitrarily small amount of additional structure on one side of the surface (so for closed manifolds, inside the model). This algorithm is the first to attain the watertight property: for a specified cutting of the manifold into a topological disk with boundary, the folding maps the boundary of the paper to within epsilon of the specified boundary of the surface (in Fréchet distance). Our foldings also have the geometric feature that every convex face is folded seamlessly, i.e., as one unfolded convex polygon of the piece of paper. This work provides the theoretical underpinnings for Origamizer, freely available software written by the second author, which has enabled practical folding of many complex polyhedral models such as the Stanford bunny.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7231Ham Sandwich is Equivalent to Borsuk-Ulam
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7232
The Borsuk-Ulam theorem is a fundamental result in algebraic topology, with applications to various areas of Mathematics. A classical application of the Borsuk-Ulam theorem is the Ham Sandwich theorem: The volumes of any n compact sets in R^n can always be simultaneously bisected by an (n-1)-dimensional hyperplane.In this paper, we demonstrate the equivalence between the Borsuk-Ulam theorem and the Ham Sandwich theorem. The main technical result we show towards establishing the equivalence is the following: For every odd polynomial restricted to the hypersphere f:S^n->R, there exists a compact set A in R^{n+1}, such that for every x in S^n we have f(x)=vol(A cap H^+) - vol(A cap H^-), where H is the oriented hyperplane containing the origin with x as the normal. A noteworthy aspect of the proof of the above result is the use of hyperspherical harmonics. Finally, using the above result we prove that there exist constants n_0, epsilon_0>0 such that for every n>= n_0 and epsilon <= epsilon_0/sqrt{48n}, any query algorithm to find an epsilon-bisecting (n-1)-dimensional hyperplane of n compact set in [-n^4.51,n^4.51]^n, even with success probability 2^-Omega(n), requires 2^Omega(n) queries.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7232TSP With Locational Uncertainty: The Adversarial Model
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7233
In this paper we study a natural special case of the Traveling Salesman Problem (TSP) with point-locational-uncertainty which we will call the adversarial TSP problem (ATSP). Given a metric space (X, d) and a set of subsets R = {R_1, R_2, ... , R_n} : R_i subseteq X, the goal is to devise an ordering of the regions, sigma_R, that the tour will visit such that when a single point is chosen from each region, the induced tour over those points in the ordering prescribed by sigma_R is as short as possible. Unlike the classical locational-uncertainty-TSP problem, which focuses on minimizing the expected length of such a tour when the point within each region is chosen according to some probability distribution, here, we focus on the adversarial model in which once the choice of sigma_R is announced, an adversary selects a point from each region in order to make the resulting tour as long as possible. In other words, we consider an offline problem in which the goal is to determine an ordering of the regions R that is optimal with respect to the ``worst'' point possible within each region being chosen by an adversary, who knows the chosen ordering. We give a 3-approximation when R is a set of arbitrary regions/sets of points in a metric space. We show how geometry leads to improved constant factor approximations when regions are parallel line segments of the same lengths, and a polynomial-time approximation scheme (PTAS) for the important special case in which R is a set of disjoint unit disks in the plane.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7233Faster Algorithms for the Geometric Transportation Problem
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7234
Let R, B be a set of n points in R^d, for constant d, where the points of R have integer supplies, points of B have integer demands, and the sum of supply is equal to the sum of demand. Let d(.,.) be a suitable distance function such as the L_p distance. The transportation problem asks to find a map tau : R x B --> N such that sum_{b in B}tau(r,b) = supply(r), sum_{r in R}tau(r,b) = demand(b), and sum_{r in R, b in B} tau(r,b) d(r,b) is minimized. We present three new results for the transportation problem when d(.,.) is any L_p metric:* For any constant epsilon > 0, an O(n^{1+epsilon}) expected time randomized algorithm that returns a transportation map with expected cost O(log^2(1/epsilon)) times the optimal cost.* For any epsilon > 0, a (1+epsilon)-approximation in O(n^{3/2}epsilon^{-d}polylog(U)polylog(n)) time, where U is the maximum supply or demand of any point.* An exact strongly polynomial O(n^2 polylog n) time algorithm, for d = 2.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7234Approximate Range Counting Revisited
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7235
We study range-searching for colored objects, where one has to count (approximately) the number of colors present in a query range. The problems studied mostly involve orthogonal range-searching in two and three dimensions, and the dual setting of rectangle stabbing by points. We present optimal and near-optimal solutions for these problems. Most of the results are obtained via reductions to the approximate uncolored version, and improved data-structures for them. An additional contribution of this work is the introduction of nested shallow cuttings.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7235Lower Bounds for Differential Privacy from Gaussian Width
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7236
We study the optimal sample complexity of a given workload of linear queries under the constraints of differential privacy. The sample complexity of a query answering mechanism under error parameter alpha is the smallest n such that the mechanism answers the workload with error at most alpha on any database of size n. Following a line of research started by Hardt and Talwar [STOC 2010], we analyze sample complexity using the tools of asymptotic convex geometry. We study the sensitivity polytope, a natural convex body associated with a query workload that quantifies how query answers can change between neighboring databases. This is the information that, roughly speaking, is protected by a differentially private algorithm, and, for this reason, we expect that a "bigger" sensitivity polytope implies larger sample complexity. Our results identify the mean Gaussian width as an appropriate measure of the size of the polytope, and show sample complexity lower bounds in terms of this quantity. Our lower bounds completely characterize the workloads for which the Gaussian noise mechanism is optimal up to constants as those having asymptotically maximal Gaussian width. Our techniques also yield an alternative proof of Pisier's Volume Number Theorem which also suggests an approach to improving the parameters of the theorem. Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7236The Geometry and Topology of Crystals: From Sphere-Packing to Tiling, Nets, and Knots (Invited Talk)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7237
Crystal structures have inspired developments in geometry since the Ancient Greeks conceived of Platonic solids after observing tetrahedral, cubical and octahedral mineral forms in their local environment. The internal structure of crystals became accessible with the development of x-ray diffraction techniques just over 100 years ago, and a key step in developing this method was understanding the arrangement of atoms in the simplest crystals as close-packings of spheres. Determining a crystal structure via x-ray diffraction unavoidably requires prior models, and this has led to the intense study of sphere packing, atom-bond networks, and arrangements of polyhedra by crystallographers investigating ever more complex compounds. In the 21st century, chemists are exploring the possibilities of coordination polymers, a wide class of crystalline materials that self-assemble from metal cations and organic ligands into periodic framework materials. Longer organic ligands mean these compounds can form multi-component interwoven network structures where the "edges" are no longer constrained to join nearest-neighbour "nodes" as in simpler atom-bond networks. The challenge for geometers is to devise algorithms for enumerating relevant structures and to devise invariants that will distinguish between different modes of interweaving. This talk will survey various methods from computational geometry and topology that are currently used to describe crystalline structures and outline research directions to address some of the open questions suggested above. Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7237The Algebraic Revolution in Combinatorial and Computational Geometry: State of the Art (Invited Talk)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7238
For the past 10 years, combinatorial geometry (and to some extent, computational geometry too) has gone through a dramatic revolution, due to the infusion of techniques from algebraic geometry and algebra that have proven effective in solving a variety of hard problems that were thought to be unreachable with more traditional techniques. The new era has begun with two groundbreaking papers of Guth and Katz, the second of which has (almost completely) solved the distinct distances problem of Erdos, open since 1946.In this talk I will survey some of the progress that has been made since then, including a variety of problems on distinct and repeated distances and other configurations, on incidences between points and lines, curves, and surfaces in two, three, and higher dimensions, on polynomials vanishing on Cartesian products with applications, on cycle elimination for lines and triangles in three dimensions, on range searching with semialgebraic sets, and I will most certainly run out of time while doing so.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7238Zapping Zika with a Mosquito-Managing Drone: Computing Optimal Flight Patterns with Minimum Turn Cost (Multimedia Contribution)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7239
We present results arising from the problem of sweeping a mosquito-infested area with an Un-manned Aerial Vehicle (UAV) equipped with an electrified metal grid. This is related to the Traveling Salesman Problem, the Lawn Mower Problem and, most closely, Milling with TurnCost. Planning a good trajectory can be reduced to considering penalty and budget variants of covering a grid graph with minimum turn cost. On the theoretical side, we show the solution of a problem from The Open Problems Project that had been open for more than 15 years, and hint at approximation algorithms. On the practical side, we describe an exact method based on Integer Programming that is able to compute provably optimal instances with over 500 pixels. These solutions are actually used for practical trajectories, as demonstrated in the video.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7239Ruler of the Plane - Games of Geometry (Multimedia Contribution)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7240
Ruler of the Plane is a set of games illustrating concepts from combinatorial and computational geometry. The games are based on the art gallery problem, ham-sandwich cuts, the Voronoi game, and geometric network connectivity problems like the Euclidean minimum spanning tree and traveling salesperson problem.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7240Folding Free-Space Diagrams: Computing the Fréchet Distance between 1-Dimensional Curves (Multimedia Contribution)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7241
By folding the free-space diagram for efficient preprocessing, we show that the Frechet distance between 1D curves can be computed in O(nk log n) time, assuming one curve has ply k.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7241Cardiac Trabeculae Segmentation: an Application of Computational Topology (Multimedia Contribution)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7242
In this video, we present a research project on cardiac trabeculae segmentation. Trabeculae are fine muscle columns within human ventricles whose both ends are attached to the wall. Extracting these structures are very challenging even with state-of-the-art image segmentation techniques. We observed that these structures form natural topological handles. Based on such observation, we developed a topological approach, which employs advanced computational topology methods and achieve high quality segmentation results.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7242MatchTheNet - An Educational Game on 3-Dimensional Polytopes (Multimedia Contribution)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7243
We present an interactive game which challenges a single player to match 3-dimensional polytopes to their planar nets. It is open source, and it runs in standard web browsers.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7243On Balls in a Hilbert Polygonal Geometry (Multimedia Contribution)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7244
Hilbert geometry is a metric geometry that extends the hyperbolic Cayley-Klein geometry. In this video, we explain the shape of balls and their properties in a convex polygonal Hilbert geometry. First, we study the combinatorial properties of Hilbert balls, showing that the shapes of Hilbert polygonal balls depend both on the center location and on the complexity of the Hilbert domain but not on their radii. We give an explicit description of the Hilbert ball for any given center and radius. We then study the intersection of two Hilbert balls. In particular, we consider the cases of empty intersection and internal/external tangencies.Thu, 08 Jun 2017 13:40:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7244Automated Program Repair (Dagstuhl Seminar 17022)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7176
This report documents the program and the outcomes of Dagstuhl Seminar 17022 "Automated Program Repair". The seminar participants presented and discussed their research through formal and informal presentations. In particular, the seminar covered work related to search-based program repair, semantic program repair, and repair of non-functional properties. As a result of the seminar, several participants plan to launch various follow-up activities, such as a program repair competition, which would help to further establish and guide this young field of research.Fri, 02 Jun 2017 10:12:27 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7176Front Matter, Table of Contents, Preface, Committees, List of Authors
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7149
Front Matter, Table of Contents, Preface, Committees, List of AuthorsWed, 31 May 2017 08:52:48 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7149VCDC: The Virtualized Complicated Device Controller
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7150
I/O virtualization enables time and space multiplexing of I/O devices, by mapping multiple logical I/O devices upon a smaller number of physical devices. However, due to the existence of additional virtualization layers, requesting an I/O from a guest virtual machine requires complicated sequences of operations. This leads to I/O performance losses, and makes precise timing of I/O operations unpredictable.This paper proposes a hardware I/O virtualization system, termed the Virtualized Complicated Device Controller (VCDC). This I/O system allows user applications to access and operate I/O devices directly from guest VMs, and bypasses the guest OS, the Virtual Machine Monitor (VMM) and low layer I/O drivers. We show that the VCDC efficiently reduces the software overhead and enhances the I/O performance and timing predictability. Furthermore, VCDC also exhibits good scalability that can handle I/O requests from variable number of CPUs in a system.Wed, 31 May 2017 08:52:48 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7150Applying Real-Time Scheduling Theory to the Synchronous Data Flow Model of Computation
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7151
Schedulability analysis techniques that are well understood within the real-time scheduling community are applied to the analysis of recurrent real-time workloads that are modeled using the synchronous data-flow graph (SDFG) model. An enhancement to the standard SDFG model is proposed, that permits the specification of a real-time latency constraint between a specified input and a specified output of an SDFG. A technique is derived for transforming such an enhanced SDFG to a collection of traditional 3-parameter sporadic tasks, thereby allowing for the analysis of systems of SDFG tasks using the methods and algorithms that have previously been developed within the real-time scheduling community for the analysis of systems of such sporadic tasks. The applicability of this approach is illustrated by applying prior results from real-time scheduling theory to construct an exact preemptive uniprocessor schedulability test for collections of recurrent processes that are each represented using the enhanced SDFG model. Wed, 31 May 2017 08:52:48 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7151Replica-Aware Co-Scheduling for Mixed-Criticality
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7152
Cross-layer fault-tolerance solutions are the key to effectively and efficiently increase the reliability in future safety-critical real-time systems. Replicated software execution with hardware support for error detection is a cross-layer approach that exploits future many-core platforms to increase reliability without resorting to redundancy in hardware. The performance of such systems, however, strongly depends on the scheduler. Standard schedulers, such as Partitioned~Strict Priority Preemptive (SPP) and Time-Division Multiplexing (TDM)-based ones, although widely employed, provide poor performance in face of replicated execution. In this paper, we propose the replica-aware co-scheduling for mixed-critical systems. Experimental results show schedulability improvements of more than 1.5x when compared to TDM and 6.9x when compared to SPP.Wed, 31 May 2017 08:52:48 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7152LTZVisor: TrustZone is the Key
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7153
Virtualization technology starts becoming more and more widespread in the embedded systems arena, driven by the upward trend for integrating multiple environments into the same hardware platform. The penalties incurred by standard software-based virtualization, altogether with the strict timing requirements imposed by real-time virtualization are pushing research towards hardware-assisted solutions. Among existing commercial off-the-shelf (COTS) technologies, ARM TrustZone promises to be a game-changer for virtualization, despite of this technology still being seen with a lot of obscurity and scepticism. In this paper we present a Lightweight TrustZone-assisted Hypervisor (LTZVisor) as a tool to understand, evaluate and discuss the benefits and limitations of using TrustZone hardware to assist virtualization. We demonstrate how TrustZone can be adequately exploited for meeting the real-time needs, while presenting a low performance cost on running unmodified rich operating systems. While ARM continues to spread TrustZone technology from the applications processors to the smallest of microcontrollers, it is undeniable that this technology is gaining an increasing relevance. Our intent is to encourage research and drive the next generation of TrustZone-assisted virtualization solutions. Wed, 31 May 2017 08:52:48 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7153VOSYSmonitor, a Low Latency Monitor Layer for Mixed-Criticality Systems on ARMv8-A
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7154
With the emergence of multicore embedded System on Chip (SoC), the integration of several applications with different levels of criticality on the same platform is becoming increasingly popular. These platforms, known as mixed-criticality systems, need to meet numerous requirements such as real-time constraints, Operating System (OS) scheduling, memory and OSes isolation.To construct mixed-criticality systems, various solutions, based on virtualization extensions, have been presented where OSes are contained in a Virtual Machine (VM) through the use of a hypervisor. However, such implementations usually lack hardware features to ensure a full isolation of other bus masters (e.g., Direct Memory Access (DMA) peripherals, Graphics Processing Unit (GPU)) between OSes. Furthermore on multicore implementation, one core is usually dedicated to one OS, causing CPU underutilization.To address these issues, this paper presents VOSYSmonitor, a multi-core software layer, which allows the co-execution of a safety-critical Real-Time Operating System (RTOS) and a non-critical General Purpose Operating System (GPOS) on the same hardware ARMv8-A platform.VOSYSmonitor main differentiation factors with the known solutions is the possibility for a processor to switch between secure and non-secure code execution at runtime. The partitioning is ensured by the ARM TrustZone technology, thus allowing to preserve the usage of virtualization features for the GPOS.VOSYSmonitor architecture will be detailed in this paper, while benchmarking its performance versus other known solutions.Wed, 31 May 2017 08:52:48 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7154The Multi-Domain Frame Packing Problem for CAN-FD
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7155
The Controller Area Network with Flexible Data-Rate (CAN-FD) is a new communication protocol to meet the bandwidth requirements for the constantly growing volume of data exchanged in modern vehicles. The problem of frame packing for CAN-FD, as studied in the literature, assumes a single sub-system where one CAN-FD bus serves as the communication medium among several Electronic Control Units (ECUs). Modern automotive electronic systems, on the other hand, consist of several sub-systems, each facilitating a certain functional domain such as powertrain, chassis and suspension. A substantial fraction of all signals is exchanged across sub-systems. In this work, we study the frame packing problem for CAN-FD with multiple sub-systems, and propose a two-stage optimization framework. In the first stage, we pack the signals into frames with the objective of minimizing the bandwidth utilization. In the second stage, we extend Audsley's algorithm to assign priorities/identifiers to the frames. In case the resulting solution is not schedulable, our framework provides a potential repacking method. We propose two solution approaches: (a) an Integer Linear Programming (ILP) formulation that provides an optimal solution but is computationally expensive for industrial-size problems; and (b) a greedy heuristic that scales well and provides solutions that are comparable to optimal solutions. Experimental results show the efficiency of our optimization framework in achieving feasible solutions with low bandwidth utilization. The results also show a significant improvement over the case when there is no cross-domain consideration (as in prior work).Wed, 31 May 2017 08:52:48 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7155Optimal Dataflow Scheduling on a Heterogeneous Multiprocessor With Reduced Response Time Bounds
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7156
Heterogeneous computing platforms with multiple types of computing resources have been widely used in many industrial systems to process dataflow tasks with pre-defined affinity of tasks to subgroups of resources. For many dataflow workloads with soft real-time requirements, guaranteeing fast and bounded response times is often the objective. This paper presents a new set of analysis techniques showing that a classical real-time scheduler, namely earliest-deadline first (EDF), is able to support dataflow tasks scheduled on such heterogeneous platforms with provably bounded response times while incurring no resource capacity loss, thus proving EDF to be an optimal solution for this scheduling problem. Experiments using synthetic workloads with widely varied parameters also demonstrate that the magnitude of the response time bounds yielded under the proposed analysis is reasonably small under all scenarios. Compared to the state-of-the-art soft real-time analysis techniques, our test yields a 68% reduction on response time bounds on average. This work demonstrates the potential of applying EDF into practical industrial systems containing dataflow-based workloads that desire guaranteed bounded response times.Wed, 31 May 2017 08:52:48 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7156Improving the Quality-of-Service for Scheduling Mixed-Criticality Systems on Multiprocessors
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7157
The traditional Vestal's model of Mixed-Criticality (MC) systems was recently extended to Imprecise Mixed-Critical task model (IMC) to guarantee some minimum level of (degraded) service to the low-critical tasks even after the system switches to the high-critical behavior. This paper extends the IMC task model by associating specific Quality-of-Service (QoS) values with the low-critical tasks and proposes a fluid-based scheduling algorithm, called MCFQ, for such task model. The MCFQ algorithm allows some low-critical tasks to provide full service even during the high-critical behavior so that the QoS of the overall system is increased. To the best of our knowledge MCFQ is the first algorithm for IMC task sets considering multiprocessor platform and QoS values.By extending the recently proposed MC-Fluid and MCF fluid-based multiprocessor scheduling algorithms for IMC task model, empirical results show that MCFQ algorithm can significantly improve the QoS of the system in comparison to that of both MC-Fluid and MCF. In addition, the schedulability performance of MCFQ is very close to the optimal MC-Fluid algorithm. Finally, we prove that the MCFQ algorithm has a speedup bound of 4/3, which is optimal for IMC tasks.Wed, 31 May 2017 08:52:48 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7157Write-Back Caches in WCET Analysis
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7158
Write-back caches are a popular choice in embedded microprocessors as they promise higher performance than write-through caches. So far, however, their use in hard real-time systems has been prohibited by the lack of adequate worst-case execution time (WCET) analysis support.In this paper, we introduce a new approach to statically analyze the behavior of write-back caches. Prior work took an "eviction-focussed perspective", answering for each potential cache miss: May this miss evict a dirty cache line and thus cause a write back? We complement this approach by exploring a "store-focussed perspective", answering for each store: May this store dirtify a clean cache line and thus cause a write back later on?Experimental evaluation demonstrates substantial precision improvements when both perspectives are combined. For most benchmarks, write-back caches are then preferable to write-through caches in terms of the computed WCET bounds.Wed, 31 May 2017 08:52:48 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7158Refinement of Workload Models for Engine Controllers by State Space Partitioning
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7159
We study an engine control application where the behavior of engine controllers depends on the engine's rotational speed. For efficient and precise timing analysis, we use the Digraph Real-Time (DRT) task model to specify the workload of control tasks where we employ optimal control theory to faithfully calculate the respective minimum inter-release times. We show how DRT models can be refined by finer grained partitioning of the state space of the engine up to a model which enables an exact timing analysis. Compared to previously proposed methods which are either unsafe or pessimistic, our work provides both abstract and tight characterizations of the corresponding workload.Wed, 31 May 2017 08:52:48 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7159Bus-Aware Static Instruction SPM Allocation for Multicore Hard Real-Time Systems
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7160
Over the past years, multicore systems emerged into the domain of hard real-time systems. These systems introduce common buses and shared memories which heavily influence the timing behavior. We show that existing WCET optimizations may lead to suboptimal results when applied to multicore setups. Additionally we provide both a genetic and a precise Integer Linear Programming (ILP)-based static instruction scratchpad memory allocation optimization which are capable of exploiting multicore properties, resulting in a WCET reduction of 26% in average compared with a bus-unaware optimization. Furthermore, we show that our ILP-based optimization's average runtime is distinctively lower in comparison to the genetic approach. Although limiting the number of tasks per core to one and partially exploiting private instruction SPMs, we cover the most crucial elements of a multicore setup: the interconnection and shared resources.Wed, 31 May 2017 08:52:48 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7160On the Pitfalls of Resource Augmentation Factors and Utilization Bounds in Real-Time Scheduling
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7161
In this paper, we take a careful look at speedup factors, utilization bounds, and capacity augmentation bounds. These three metrics have been widely adopted in real-time scheduling research as the de facto standard theoretical tools for assessing scheduling algorithms and schedulability tests. Despite that, it is not always clear how researchers and designers should interpret or use these metrics. In studying this area, we found a number of surprising results, and related to them, ways in which the metrics may be misinterpreted or misunderstood. In this paper, we provide a perspective on the use of these metrics, guiding researchers on their meaning and interpretation, and helping to avoid pitfalls in their use. Finally, we propose and demonstrate the use of parametric augmentation functions as a means of providing nuanced information that may be more relevant in practical settings.Wed, 31 May 2017 08:52:48 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7161Communication Centric Design in Complex Automotive Embedded Systems
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7162
Automotive embedded applications like the engine management system are composed of multiple functional components that are tightly coupled via numerous communication dependencies and intensive data sharing, while also having real-time requirements. In order to cope with complexity, especially in multi-core settings, various communication mechanisms are used to ensure data consistency and temporal determinism along functional cause-effect chains. However, existing timing analysis methods generally only support very basic communication models that need to be extended to handle the analysis of industry grade problems which involve more complex communication semantics. In this work, we give an overview of communication semantics used in the automotive industry and the different constraints to be considered in the design process. We also propose a method for model transformation to increase the expressiveness of current timing analysis methods enabling them to work with more complex communication semantics. We demonstrate this transformation approach for concrete implementations of two communication semantics, namely, implicit and LET communication. We discuss the impact on end-to-end latencies and communication overheads based on a full blown engine management system.Wed, 31 May 2017 08:52:48 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7162Budgeting Under-Specified Tasks for Weakly-Hard Real-Time Systems
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7163
In this paper, we present an extension of slack analysis for budgeting in the design of weakly-hard real-time systems. During design, it often happens that some parts of a task set are fully specified while other parameters, e.g. regarding recovery or monitoring tasks, will be available only much later. In such cases, slack analysis can help anticipate how these missing parameters can influence the behavior of the whole system so that a resource budget can be allocated to them. It is, however, sufficient in many application contexts to budget these tasks in order to preserve weakly-hard rather than hard guarantees. We thus present an extension of slack analysis for deriving task budgets for systems with hard and weakly-hard requirements. This work is motivated by and validated on a realistic case study inspired by industrial practice.Wed, 31 May 2017 08:52:48 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7163Cache-Conscious Offline Real-Time Task Scheduling for Multi-Core Processors
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7164
Most schedulability analysis techniques for multi-core architectures assume a single Worst-Case Execution Time (WCET) per task, which is valid in all execution conditions. This assumption is too pessimistic for parallel applications running on multi-core architectures with local instruction or data caches, for which the WCET of a task depends on the cache contents at the beginning of its execution, itself depending on the task that was executed before the task under study. In this paper, we propose two scheduling techniques for multi-core architectures equipped with local instruction and data caches. The two techniques schedule a parallel application modeled as a task graph, and generate a static partitioned non-preemptive schedule. We propose an optimal method, using an Integer Linear Programming (ILP) formulation, as well as a heuristic method based on list scheduling. Experimental results show that by taking into account the effect of private caches on tasks' WCETs, the length of generated schedules is significantly reduced as compared to schedules generated by cache-unaware scheduling methods. The observed schedule length reduction on streaming applications is 11% on average for the optimal method and 9% on average for the heuristic method.Wed, 31 May 2017 08:52:48 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7164Semi-Partitioned Scheduling of Dynamic Real-Time Workload: A Practical Approach Based on Analysis-Driven Load Balancing
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7165
Recent work showed that semi-partitioned scheduling can achieve near-optimal schedulability performance, is simpler to implement compared to global scheduling, and less heavier in terms of runtime overhead, thus resulting in an excellent choice for implementing real-world systems. However, semi-partitioned scheduling typically leverages an off-line design to allocate tasks across the available processors, which requires a-priori knowledge of the workload. Conversely, several simple global schedulers, as global earliest-deadline first (G-EDF), can transparently support dynamic workload without requiring a task-allocation phase. Nonetheless, such schedulers exhibit poor worst-case performance.This work proposes a semi-partitioned approach to efficiently schedule dynamic real-time workload on a multiprocessor system. A linear-time approximation for the C=D splitting scheme under partitioned EDF scheduling is first presented to reduce the complexity of online scheduling decisions. Then, a load-balancing algorithm is proposed for admitting new real-time workload in the system with limited workload re-allocation. A large-scale experimental study shows that the linear-time approximation has a very limited utilization loss compared to the exact technique and the proposed approach achieves very high schedulability performance, with a consistent improvement on G-EDF and pure partitioned EDF scheduling.Wed, 31 May 2017 08:52:48 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7165Thermal Implications of Energy-Saving Schedulers
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7166
In many real-time systems, continuous operation can raise processor temperature, potentially leading to system failure, bodily harm to users, or a reduction in the functional lifetime of a system. Static power dominates the total power consumption, and is also directly proportional to the operating temperature. This reduces the effectiveness of frequency scaling and necessitates the use of sleep states. In this work, we explore the relationship between energy savings and system temperature in the context of fixed-priority energy-saving schedulers, which utilize a processor’s deep-sleep state to save energy. We derive insights from a well-known thermal model, and are able to identify proactive design choices which are independent of system constants and can be used to reduce processor temperature. Our observations indicate that, while energy savings are key to lower temperatures, not all energy-efficient solutions yield low temperatures. Based on these insights, we propose the SysSleep and ThermoSleep algorithms, which enable a thermally-effective sleep schedule. We also derive a lower bound on the optimal temperature achievable by energy-saving schedulers. Additionally, we discuss partitioning and task phasing techniques for multi-core processors, which require all cores to synchronously transition into deep sleep, as well as those which support independent deep-sleep transitions. We observe that, while energy optimization is straightforward in some cases, the dependence of temperature on partitioning and task phasing makes temperature minimization non-trivial. Evaluations show that compared to the existing purely energy-efficient design methodology, our proposed techniques yield lower temperatures along with significant energy savings.Wed, 31 May 2017 08:52:48 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7166Energy-Efficient Multi-Core Scheduling for Real-Time DAG Tasks
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7167
In this work, we study energy-aware real-time scheduling of a set of sporadic Directed Acyclic Graph (DAG) tasks with implicit deadlines. While meeting all real-time constraints, we try to identify the best task allocation and execution pattern such that the average power consumption of the whole platform is minimized. To the best of our knowledge, this is the first work that addresses the power consumption issue in scheduling multiple DAG tasks on multi-cores and allows intra-task processor sharing. We first adapt the decomposition-based framework for federated scheduling and propose an energy-sub-optimal scheduler. Then we derive an approximation algorithm to identify processors to be merged together for further improvements in energy-efficiency and to prove the bound of the approximation ratio. We perform a simulation study to demonstrate the effectiveness and efficiency of the proposed scheduling. The simulation results show that our algorithms achieve an energy saving of 27% to 41% compared to existing DAG taskschedulers.Wed, 31 May 2017 08:52:48 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7167WCET Derivation under Single Core Equivalence with Explicit Memory Budget Assignment
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7168
In the last decade there has been a steady uptrend in the popularity of embedded multi-core platforms. This represents a turning point in the theory and implementation of real-time systems. From a real-time standpoint, however, the extensive sharing of hardware resources (e.g. caches, DRAM subsystem, I/O channels) represents a major source of unpredictability. Budget-based memory regulation (throttling) has been extensively studied to enforce a strict partitioning of the DRAM subsystem’s bandwidth. The common approach to analyze a task under memory bandwidth regulation is to consider the budget of the core where the task is executing, and assume the worst-case about the remaining cores' budgets.In this work, we propose a novel analysis strategy to derive the WCET of a task under memory bandwidth regulation that takes into account the exact distribution of memory budgets to cores. In this sense, the proposed analysis represents a generalization of approaches that consider (i) even budget distribution across cores; and (ii) uneven but unknown (except for the core under analysis) budget assignment. By exploiting the additional piece of information, we show that it is possible to derive a more accurate WCET estimation. Our evaluations highlight that the proposed technique can reduce overestimation by 30% in average, and up to 60%, compared to the state of the art.Wed, 31 May 2017 08:52:48 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7168A Hierarchical Scheduling Model for Dynamic Soft-Realtime System
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7169
We present a new hierarchical approximation and scheduling approach for applications and tasks with multiple modes on a single processor. Our model allows for a temporal and spatial distribution of the feasibility problem for a variable set of tasks with non-deterministic and fluctuating costs at runtime. In case of overloads an optimal degradation strategy selects one of several application modes or even temporarily deactivates applications. Hence, transient and permanent bottlenecks can be overcome with an optimal system quality, which is dynamically decided. This paper gives the first comprehensive and complete overview of all aspects of our research, including a novel CBS concept to confine entire applications, an evaluation of our system by using a video-on-demand application, an outline for adding further resource dimension, and aspects of our protoype implementation based on RTSJ.Wed, 31 May 2017 08:52:48 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7169A Linux Real-Time Packet Scheduler for Reliable Static SDN Routing
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7170
In a distributed computing environment, guaranteeing the hard deadline for real-time messages is essential to ensure schedulability of real-time tasks. Since capabilities of the shared resources for transmission are limited, e.g., the buffer size is limited on network devices, it becomes a challenge to design an effective and feasible resource sharing policy based on both the demand of real-time packet transmissions and the limitation of resource capabilities. We address this challenge in two cooperative mechanisms. First, we design a static routing algorithm to find forwarding paths for packets to guarantee their hard deadlines. The routing algorithm employs a validation-based backtracking procedure capable of deriving the demand of a set of real-time packets on each shared network device, and it checks whether this demand can be met on the device. Second, we design a packet scheduler that runs on network devices to transmit messages according to our routing requirements. We implement these mechanisms on virtual software-defined network (SDN) switches and evaluate them on real hardware in a local cluster to demonstrate the feasibility and effectiveness of our routing algorithm and packet scheduler.Wed, 31 May 2017 08:52:48 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7170Mixed-Criticality Scheduling with Dynamic Redistribution of Shared Cache
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7171
The design of mixed-criticality systems often involves painful tradeoffs between safety guarantees and performance. However, the use of more detailed architectural models in the design and analysis of scheduling arrangements for mixed-criticality systems can provide greater confidence in the analysis, but also opportunities for better performance. Motivated by this view, we propose an extension of Vestal's model for mixed-criticality multicore systems that (i) accounts for the per-task partitioning of the last-level cache and (ii) supports the dynamic reassignment, for better schedulability, of cache portions initially reserved for lower-criticality tasks to the higher-criticality tasks, when the system switches to high-criticality mode. To this model, we apply partitioned EDF scheduling with Ekberg and Yi's deadline-scaling technique. Our schedulability analysis and scalefactor calculation is cognisant of the cache resources assigned to each task, by using WCET estimates that take into account these resources. It is hence able to leverage the dynamic reconfiguration of the cache partitioning, at mode change, for better performance, in terms of provable schedulability. We also propose heuristics for partitioning the cache in low- and high-criticality mode, that promote schedulability. Our experiments with synthetic task sets, indicate tangible improvements in schedulability compared to a baseline cache-aware arrangement where there is no redistribution of cache resources from low- to high-criticality tasks in the event of a mode change.Wed, 31 May 2017 08:52:48 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7171Contego: An Adaptive Framework for Integrating Security Tasks in Real-Time Systems
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7172
Embedded real-time systems (RTS) are pervasive. Many modern RTS are exposed to unknown security flaws, and threats to RTS are growing in both number and sophistication. However, until recently, cyber-security considerations were an afterthought in the design of such systems. Any security mechanisms integrated into RTS must (a) co-exist with the real-time tasks in the system and (b) operate without impacting the timing and safety constraints of the control logic. We introduce Contego, an approach to integrating security tasks into RTS without affecting temporal requirements. Contego is specifically designed for legacy systems, viz., the real-time control systems in which major alterations of the system parameters for constituent tasks is not always feasible. Contego combines the concept of opportunistic execution with hierarchical scheduling to maintain compatibility with legacy systems while still providing flexibility by allowing security tasks to operate in different modes. We also define a metric to measure the effectiveness of such integration. We evaluate Contego using synthetic workloads as well as with an implementation on a realistic embedded platform (an open-source ARM CPU running real-time Linux).Wed, 31 May 2017 08:52:48 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7172Design and Implementation of a Time Predictable Processor: Evaluation With a Space Case Study
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7173
Embedded real-time systems like those found in automotive, rail and aerospace, steadily require higher levels of guaranteed computing performance (and hence time predictability) motivated by the increasing number of functionalities provided by software. However, high-performance processor design is driven by the average-performance needs of mainstream market. To make things worse, changing those designs is hard since the embedded real-time market is comparatively a small market. A path to address this mismatch is designing low-complexity hardware features that favor time predictability and can be enabled/disabled not to affect average performance when performance guarantees are not required. In this line, we present the lessons learned designing and implementing LEOPARD, a four-core processor facilitating measurement-based timing analysis (widely used in most domains). LEOPARD has been designed adding low-overhead hardware mechanisms to a LEON3 processor baseline that allow capturing the impact of jittery resources (i.e. with variable latency) in the measurements performed at analysis time. In particular, at core level we handle the jitter of caches, TLBs and variable-latency floating point units; and at the chip level, we deal with contention so that time-composable timing guarantees can be obtained. The result of our applied study with a Space application shows how per-resource jitter is controlled facilitating the computation of high-quality WCET estimates.Wed, 31 May 2017 08:52:48 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7173Contention-Aware Dynamic Memory Bandwidth Isolation with Predictability in COTS Multicores: An Avionics Case Study
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7174
Airbus is investigating COTS multicore platforms for safety-critical avionics applications, pursuing helicopter-style autonomous and electric aircraft. These aircraft need to be ultra-lightweight for future mobility in the urban city landscape. As a step towards certification, Airbus identified the need for new methods that preserve the ARINC 653 single core schedule of a Helicopter Terrain Awareness and Warning System (HTAWS) application while scheduling additional safety-critical partitions on the other cores. As some partitions in the HTAWS application are memory-intensive, static memory bandwidth throttling may lead to slow down of such partitions or provide only little remaining bandwidth to the other cores. Thus, there is a need for dynamic memory bandwidth isolation. This poses new challenges for scheduling, as execution times and scheduling become interdependent: scheduling requires execution times as input, which depends on memory latencies and contention from memory accesses of other cores - which are determined by scheduling. Furthermore, execution times depend on memory access patterns. In this paper, we propose a method to solve this problem for slot-based time-triggered systems without requiring application source-code modifications using a number of dynamic memory bandwidth levels. It is NoC and DRAM controller contention-aware and based on the existing interference-sensitive WCET computation and the memory bandwidth throttling mechanism. It constructs schedule tables by assigning partitions and dynamic memory bandwidth to each slot on each core, considering worst case memory access patterns. Then at runtime, two servers - for processing time and memory bandwidth - run on each core, jointly controlling the contention between the cores and the amount of memory accesses per slot.As a proof-of-concept, we use a constraint solver to construct tables. Experiments on the P4080 COTS multicore platform, using a research OS from Airbus and EEMBC benchmarks, demonstrate that our proposed method enables preserving existing schedules on a core while scheduling additional safety-critical partitions on other cores, and meets dynamic memory bandwidth isolation requirements.Wed, 31 May 2017 08:52:48 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7174WCET-Driven Dynamic Data Scratchpad Management With Compiler-Directed Prefetching
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7175
In recent years, the real-time community has produced a variety of approaches targeted at managing on-chip memory (scratchpads and caches) in a predictable way. However, to obtain safe WCET bounds, such techniques generally assume that the processor is stalled while waiting to reload the content of the on-chip memory; hence, they are less effective at hiding main memory latency compared to speculation-based techniques, such as hardware prefetching, that are largely used in general-purpose systems. In this work, we introduce a novel compiler-directed prefetching scheme for scratchpad memory that effectively hides the latency of main memory accesses by overlapping data transfers with the program execution. We implement and test an automated program compilation and optimization flow within the LLVM framework, and we show how to obtain improved WCET bounds through static analysis.Wed, 31 May 2017 08:52:48 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7175Functoriality in Geometric Data (Dagstuhl Seminar 17021)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7148
This report provides an overview of the talks at the Dagstuhl Seminar 17021 "Functoriality in Geometric Data". The seminar brought together researchers interested in the fundamental questions of similarity and correspondence across geometric data sets, which include collections of GPS traces, images, 3D shapes and other types of geometric data. A recent trend, emerging independently in multiple theoretical and applied communities, is to understand networks of geometric data sets through their relations and interconnections, a point of view that can be broadly described as exploiting the functoriality of data, which has a long tradition associated with it in mathematics. Functoriality, in its broadest form, is the notion that in dealing with any kind of mathematical object, it is at least as important to understand the transformations or symmetries possessed by the object or the family of objects to which it belongs, as it is to study the object itself. This general idea has led to deep insights into the structure of various geometric spaces as well as to state-of-the-art methods in various application domains. The talks spanned a wide array of subjects under the common theme of functoriality, including: the analysis of geometric collections, optimal transport for geometric datasets, deep learning applications and many more.Tue, 30 May 2017 09:46:43 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7148