PROGRAMME.
09:00 - 10:30: Parallel graph algorithms
09:00 - 09:45: David Safranek (Masaryk University)
Parallel Algorithms for Parameter Synthesis from Temporal Logic Specifications
ABSTRACT. We will present a set of parallel algorithms for parameter synthesis in parametrised dynamical systems from temporal logic specifications. The problem is for a dynamical system represented in terms of a finite-state transition system with parametrised transition relation to synthesise parameter values satisfying the given specification. Technically, the method is based on model checking algorithms adapted to such kind of transition systems. Additionally, we will address a specific subproblem of parameter synthesis targeting identification of attractors in systems dynamics. To that end, a novel parallel algorithm for detection of strongly connected components in a parameterised system will be presented. We will show that the underlying algorithms can gain advantages from efficient symbolic representations of sets of parameter valuations. To demonstrate the method, we will describe applications to models representing dynamics of biological systems with complex non-linear behaviour.
16:45 - 17:30: Loredana Sorrentino, Aniello Murano, Rossella Arcucci and Umberto Marotta (University of Naples, Imperial College London)
An Efficient Zielonka's Algorithm for Parallel Parity Games
ABSTRACT. Parity games are abstract infinite-duration two-player games, widely studied in computer science. Several solution algorithms have been proposed and also implemented in the community tool of choice called PGSolver, which has declared the Zielonka Recursive (ZR) algorithm the best performing on randomly generated games. With the aim of scaling and solving wider classes of parity games, several improvements and optimizations have been proposed over the existing algorithms. However, no one has yet explored the benefit of using the full computational power of which even common modern multicore processors are capable of. This is even more surprisingly by considering that most of the advanced algorithms in PGSolver are sequential. In this work we introduce and implement, on a multicore architecture, a parallel version of the Attractor algorithm, that is the main kernel of the ZR algorithm. This choice follows our investigation that more of the 99% of the execution time of the ZR algorithm is spent in this module.
10:30 - 11:00: Coffee break
11:00 - 12:30: Verifying parallel programs
11:00 - 11:45: Jérôme Dohrau, Alexander Summers, Caterina Urban, Severin Münger and Peter Müller (ETH Zürich)
Permission Inference for Array Programs
ABSTRACT. Information about the memory locations accessed by a program is, for instance, required for program parallelisation and program verification. Existing inference techniques for this information provide only partial solutions for the important class of array-manipulating programs. In this paper, we present a static analysis that infers the memory footprint of an array program in terms of permission pre- and postconditions as used, for example, in separation logic. This formulation allows our analysis to handle concurrent programs and produces specifications that can be used by verification tools.
Our analysis expresses the permissions required by a loop via maximum expressions over the individual loop iterations. These maximum expressions are then solved by a novel maximum elimination algorithm, in the spirit of quantifier elimination.
Our approach is sound and is implemented; an evaluation on existing benchmarks for memory safety of array programs demonstrates accurate results, even for programs with complex access patterns and nested loops.
11:45 - 12:30: Yatin Manerkar, Daniel Lustig, Margaret Martonosi and Michael Pellauer (Princeton University, NVIDIA)
RTLCheck: Automatically Verifying the Memory Consistency of Processor RTL
ABSTRACT. We propose the presentation of our recent work on RTLCheck, the first ever methodology and tool for automated memory consistency verification of processor RTL. We would also like to present a tool demonstration of RTLCheck's verification of a multicore version of the open-source RISC-V V-scale processor. RTLCheck is open-source and available at github.com/ymanerka/rtlcheck.
12:30 - 14:00: Lunch break
14:00 - 15:30: Parallel SAT solving
16:00 - 18:00: Parallel parity game solving
15:30 - 16:00: Coffee break
ABSTRACT. For multi-core computers, an important paradigm for parallel execution is task-based or fork-join parallelism. Typically this is implemented using work-stealing. This paradigm is a good fit for algorithms that contain recursion, but is also suitable in other contexts, for example the load-balancing of parallel computations on arrays. We apply work-stealing in several verification contexts. We parallelize operations on binary decision diagrams and on verification tools that use binary decision diagrams, where we apply work-stealing both on the low level of the individual operations and on the higher level of the search algorithms. We parallelize parity game solvers in the following two ways. We use work-stealing to parallelize backward search for attractor computation. We also use work-stealing to parallelize all steps of the strategy improvement algorithm. In these applications, using work-stealing is necessary but not sufficient to obtain a good performance. We must also avoid locking techniques and instead use lock-free techniques for scalable performance. We use lock-free techniques not only for the parallelized algorithms but also to implement the scalable work-stealing framework Lace with high multi-core scaling.
16:00 - 16:45: Tom van Dijk (Johannes Kepler University Linz)
Using work-stealing to parallelize symbolic algorithms and parity game solvers
19:00 - 21:30: Workshops dinner at Magdalen College
ABSTRACT. There has been an increasing interest in recent years towards the development of efficient solvers for Answer Set Programming (ASP) and towards the application of ASP to solve increasing more challenging problems. In particular, several recent efforts have explored the issue of scalability of ASP solvers when addressing the challenges caused by the need to ground the program before resolution. This paper offers an alternative solution to this challenge, focused on the use of distributed programming techniques to reason about ASP programs whose grounding would be prohibitive for mainstream ASP solvers. The work builds on the work proposed by Konczak et al. in 2004, which proposed a characterization of answer set solving as a form of non-standard graph coloring. The paper expands this characterization to include syntactic extensions used in modern ASP (e.g., choice rules, weight constraints). We present an implementation of the solver using a distributed programming framework specifically designed to manipulate very large graphs, as provided by Apache Spark, which in turn builds on the MapReduce programming framework. Finally, we provide a few preliminary results obtained from the first prototype implementation of this approach.
09:45 - 10:30: Federico Igne, Agostino Dovier and Enrico Pontelli (University of Udine and New Mexico State University)
MASP-Reduce: a proposal for distributed computation of stable models
17:30 - 18:00: Discussion and closing
14:00 - 14:45: Thorsten Ehlers and Dirk Nowotka (Universität Kiel)
Tuning Parallel SAT Solvers
ABSTRACT. In this paper we present new implementation details and benchmarking results for our parallel portfolio solver TOPO. In particular, we discuss ideas and implementation details for the exchange of learned clauses in a massively-parallel SAT solver which is designed to run more that 1,000 solver threads in parallel. Furthermore, we go back to the roots of portfolio SAT solving, and discuss the impact of diversifying the solver by using different restart- , branching- and clause database management heuristics. We show that these techniques can be used to tune the solver towards different problems. However, in a case study on formulas derived from Bounded Model Checking problems we see the best performance when using a rather simple clause exchange strategy. We show details of these tests and discuss possible explanations for this phenomenon.
14:45 - 15:30: Muhammad Osama and Anton Wijs (Eindhoven University of Technology)
GPU Accelerated SAT Solving
ABSTRACT. Details will follow shortly.