Publications
118 results found
Deligiannis P, Donaldson AF, 2014, Automatic verification of data race freedom in device drivers, Pages: 36-39, ISSN: 2190-6807
Device drivers are notoriously hard to develop and even harder to debug. They are typically prone to many serious issues such as data races. In this paper, we present static pair-wise lock set analysis, a novel sound verification technique for proving data race freedom in device drivers. Our approach not only avoids reasoning about thread interleavings, but also allows the reuse of existing successful sequential verification techniques.
Bardsley E, Betts A, Chong N, et al., 2014, Engineering a static verification tool for GPU kernels, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol: 8559, Pages: 226-242, ISSN: 0302-9743
We report on practical experiences over the last 2.5 years related to the engineering of GPUVerify, a static verification tool for OpenCL and CUDA GPU kernels, plotting the progress of GPUVerify from a prototype to a fully functional and relatively efficient analysis tool. Our hope is that this experience report will serve the verification community by helping to inform future tooling efforts. © 2014 Springer International Publishing.
Amani S, Chubb P, Donaldson AF, et al., 2014, Automatic verification of active device drivers, Pages: 106-118, ISSN: 0163-5980
We develop a practical solution to the problem of automatic verification of the interface between device drivers and the operating system. Our solution relies on a combination of improved driver architecture and verification tools. Unlike previous proposals for verification-friendly drivers, our methodology supports drivers written in C and can be implemented in any existing OS. Our Linuxbased evaluation shows that this methodology amplifies the power of existing model checking tools in detecting driver bugs, making it possible to verify properties that are beyond the reach of traditional techniques.
Bardsley E, Donaldson AF, Wickerson J, 2014, Kernelinterceptor: Automating GPU kernel verification by intercepting kernels and their parameters, International Workshop on OpenCL (IWOCL)
Copyright 2014 ACM.GPUVerify is a static analysis tool for verifying that GPU kernels are free from data races and barrier divergence. It is intended as an automatic tool, but its usability is impaired by the fact that the user must explicitly supply the kernel source code, the number of work items and work groups, and preconditions on key kernel arguments. Extracting this information from non-trivial OpenCL applications is laborious and error-prone. We describe an extension to GPUVerify, called KernelInterceptor, that automates the extraction of this information from a given OpenCL application. After recompiling the application having included an additional header file, and linking with an additional library, KernelInterceptor is able to detect each dynamic kernel launch and record the values of the various parameters in a series of log files. GPUVerify can then be invoked to examine these log files and verify each kernel instance. We explain how the interception mechanism works, and comment on the extent to which it improves the usability of GPUVerify.
Bardsley E, Donaldson AF, 2014, Warps and atomics: beyond barrier synchronization in the verification of GPU kernels, 6th International Symposium, NFM 2014, Publisher: Springer, Pages: 230-245
We describe the design and implementation of methods to support reasoning about data races in GPU kernels where constructs other than the standard barrier primitive are used for synchronization. At one extreme we consider kernels that exploit implicit, coarse-grained synchronization between threads in the same warp, a feature provided by many architectures. At the other extreme we consider kernels that reduce or avoid barrier synchronization through the use of atomic operations. We discuss design decisions associated with providing support for warps and atomics in GPUVerify, a formal verification tool for OpenCL and CUDA kernels. We evaluate the practical impact of these design decisions using a large set of benchmarks, showing that warps can be supported in a scalable manner, that a coarse abstraction suffices for efficient reasoning about most practical uses of atomic operations, and that a novel, refined abstraction captures an important design pattern where atomic operations are used to compute unique array indices. Our evaluation revealed two previously unknown bugs in publicly available benchmark suites.
Chong N, Donaldson AF, Ketema J, 2014, A Sound and Complete Abstraction for Reasoning about Parallel Prefix Sums, 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Publisher: ASSOC COMPUTING MACHINERY, Pages: 397-409, ISSN: 0362-1340
Chong N, Donaldson AF, Ketema J, 2014, A sound and complete abstraction for reasoning about parallel prefix sums, ACM SIGPLAN Notices, Vol: 49, Pages: 397-409, ISSN: 1523-2867
Prefix sums are key building blocks in the implementation of many concurrent software applications, and recently much work has gone into efficiently implementing prefix sums to run on massively parallel graphics processing units (GPUs). Because they lie at the heart of many GPU-accelerated applications, the correctness of prefix sum implementations is of prime importance. We introduce a novel abstraction, the interval of summations, that allows scalable reasoning about implementations of prefix sums. We present this abstraction as a monoid, and prove a soundness and completeness result showing that a generic sequential prefix sum implementation is correct for an array of length n if and only if it computes the correct result for a specific test case when instantiated with the interval of summations monoid. This allows correctness to be established by running a single test where the input and result require O(n lg(n)) space. This improves upon an existing result by Sheeran where the input requires O(n lg(n)) space and the result O(n2 lg(n)) space, and is more feasible for large n than a method by Voigtländer that usesO(n) space for the input and result but requires running O(n2) tests.We then extend our abstraction and results to the context of data-parallel programs, developing an automated verification method for GPU implementations of prefix sums. Our method uses static verification to prove that a generic prefix sum implementation is data race-free, after which functional correctness of the implementation can be determined by running a single test case under the interval of summations abstraction. We present an experimental evaluation using four different prefix sum algorithms, showing that our method is highly automatic, scales to large thread counts, and significantly outperforms Voigtländer's method when applied to large arrays.
Donaldson AF, 2014, The GPUVerify method: A tutorial overview
I present a tutorial overview demonstrating the key technique used by GPUVerify, a static verification tool for graphics processing unit (GPU) kernels. The technique is a method for translating a massively parallel GPU kernel into a sequential program such that correctness of the sequential program implies data race-freedom of the parallel kernel.
Thomson P, Donaldson AF, Betts A, 2014, Concurrency testing using schedule bounding: an empirical study, Publisher: ACM, Pages: 15-28
Chong N, Donaldson AF, Kelly PHJ, et al., 2013, Barrier Invariants: A Shared State Abstraction for the Analysis of Data-Dependent GPU Kernels, 2013 ACM SIGPLAN international conference on Object oriented programming systems languages & applications (OOPSLA'13), Publisher: ASSOC COMPUTING MACHINERY, Pages: 605-621, ISSN: 0362-1340
Collingbourne P, Donaldson AF, Ketema J, et al., 2013, Interleaving and lock-step semantics for analysis and verification of GPU kernels, 22nd European Symposium on Programming, ESOP 2013, Publisher: Springer Verlag, Pages: 270-289, ISSN: 0302-9743
Baghdadi R, Cohen A, Guelton S, et al., 2013, PENCIL: Towards a Platform-Neutral Compute Intermediate Language for DSLs, CoRR, Vol: abs/1302.5586
Betts A, Donaldson A, 2013, Estimating the WCET of GPU-Accelerated Applications using Hybrid Analysis, 25th Euromicro Conference on Real-Time Systems (ECRTS), Publisher: IEEE, Pages: 193-202, ISSN: 1068-3070
- Author Web Link
- Open Access Link
- Cite
- Citations: 20
Betts A, Chong N, Donaldson AF, et al., 2012, GPU verify: A verifier for GPU kernels, Pages: 113-131
We present a technique for verifying race- and divergencefreedom of GPU kernels that are written in mainstream kernel programming languages such as OpenCL and CUDA. Our approach is founded on a novel formal operational semantics for GPU programming termed synchronous, delayed visibility (SDV) semantics. The SDV semantics provides a precise definition of barrier divergence in GPU kernels and allows kernel verification to be reduced to analysis of a sequential program, thereby completely avoiding the need to reason about thread interleavings, and allowing existing modular techniques for program verification to be leveraged. We describe an efficient encoding for data race detection and propose a method for automatically inferring loop invariants required for verification. We have implemented these techniques as a practical verification tool, GPUVerify, which can be applied directly to OpenCL and CUDA source code. We evaluate GPUVerify with respect to a set of 163 kernels drawn from public and commercial sources. Our evaluation demonstrates that GPUVerify is capable of efficient, automatic verification of a large number of real-world kernels.
Betts A, Chong N, Donaldson AF, et al., 2012, GPUVerify: a Verifier for GPU Kernels, 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2012), Publisher: ACM, Pages: 113-132, ISSN: 1523-2867
Alastair F Donaldson, Alexander Kaiser, Daniel Kroening, et al., 2012, Counterexample-guided abstraction refinement for symmetric concurrent programs, Formal Methods in System Design
Basler G, Donaldson AF, Kaiser A, et al., 2012, SatAbs: A Bit-Precise Verifier for C Programs - (Competition Contribution)., Publisher: Springer, Pages: 552-555
Amani S, Ryzhyk L, Donaldson AF, et al., 2011, Static analysis of device drivers: We can do better!
We argue that the device driver architecture enforced by current operating systems complicates both manual and automatic reasoning about driver behaviour. In particular, it makes it hard and in some cases impossible to statically verify that the driver correctly interacts with the rest of the kernel. This limitation cannot be addressed solely via better verification tools. We maintain that qualitative improvement in the effectiveness of static driver verification must rely on an improved driver architecture, leading to drivers that are easier to write, understand, and verify. To support our claims, we present a device driver architecture, called active drivers, that satisfies these requirements. We outline our methodology for specifying and verifying active driver protocols using existing model checking tools and describe initial experimental results. © 2011 ACM.
- Abstract
- Open Access Link
- Cite
- Citations: 5
Botincan M, Dodds M, Donaldson AF, et al., 2011, Safe asynchronous multicore memory operations, 26th IEEE/ACM International Conference on Automated Software Engineering, Publisher: IEEE, Pages: 153-162
Donaldson AF, Kroening D, Ruemmer P, 2011, SCRATCH: a Tool for Automatic Analysis of DMA Races, 16th ACM Symposium on Principles and Practice of Parallel Programming, Publisher: ASSOC COMPUTING MACHINERY, Pages: 311-312, ISSN: 0362-1340
- Author Web Link
- Cite
- Citations: 5
Donaldson AF, Kroeining D, Ruemmer P, 2011, Automatic analysis of DMA races using model checking and k-induction, Formal Methods in System Design, Vol: 39, Pages: 83-113
Botincan M, Dodds M, Donaldson AF, et al., 2011, Automatic Safety Proofs for Asynchronous Memory Operations, 16th ACM Symposium on Principles and Practice of Parallel Programming, Publisher: ASSOC COMPUTING MACHINERY, Pages: 313-314, ISSN: 0362-1340
Donaldson AF, Kroening D, Rümmer P, 2011, SCRATCH: A tool for automatic analysis of DMA races, Pages: 311-312
We present the SCRATCH tool, which uses bounded model checking and k-induction to automatically analyse software for multicore processors such as the Cell BE, in order to detect DMA races. Copyright © 2011 ACM.
Russel G, Riley C, Henning N, et al., 2011, The impact of diverse memory architectures on multicore consumer software: An industrial perspective from the video games domain, Pages: 37-42
Memory architectures need to adapt in order for performance and scalability to be achieved in software for multicore systems. In this paper, we discuss the impact of techniques for scalable memory architectures, especially the use of multiple, non-cache-coherent memory spaces, on the implementation and performance of consumer software. Primarily, we report extensive real-world experience in this area gained by Codeplay Software Ltd., a software tools company working in the area of compilers for video games and GPU software. We discuss the solutions we use to handle variations in memory architecture in consumer software, and the impact such variations have on software development effort and, consequently, development cost. This paper introduces preliminary findings regarding impact on software, in advance of a larger-scale analysis planned over the next few years. The techniques discussed have been employed successfully in the development and optimisation of a shipping AAA cross-platform video game. © 2011 ACM.
Donaldson AF, Haller L, Kroening D, 2011, Strengthening Induction-Based Race Checking with Lightweight Static Analysis, 12th International Conference on Verification, Model Checking, and Abstract Interpretation, Publisher: SPRINGER-VERLAG BERLIN, Pages: 169-183, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 6
Donaldson AF, Kaiser A, Kroening D, et al., 2011, Symmetry-Aware Predicate Abstraction for Shared-Variable Concurrent Programs (Extended Technical Report), CoRR, Vol: abs/1102.2330
Donaldson AF, Haller L, Kroening D, et al., 2011, Software Verification Using <i>k</i>-Induction, 18th International Static Analysis Symposium (SAS 2011), Publisher: SPRINGER-VERLAG BERLIN, Pages: 351-+, ISSN: 0302-9743
- Author Web Link
- Open Access Link
- Cite
- Citations: 53
Alglave J, Donaldson AF, Kroening D, et al., 2011, Making Software Verification Tools Really Work, 9th International Symposium on Automated Technology for Verification and Analysis (ATVA), Publisher: SPRINGER-VERLAG BERLIN, Pages: 28-42, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 11
Donaldson AF, Gay SJ, 2010, Type inference and strong static type checking for Promela, SCIENCE OF COMPUTER PROGRAMMING, Vol: 75, Pages: 1165-1191, ISSN: 0167-6423
Wahl T, Donaldson A, 2010, Replication and Abstraction: Symmetry in Automated Formal Verification, Symmetry, Vol: 2, Pages: 799-847
This data is extracted from the Web of Science and reproduced under a licence from Thomson Reuters. You may not copy or re-distribute this data in whole or in part without the written consent of the Science business of Thomson Reuters.