Pedro da Rocha Pinto

2018

Thomas Dinsdale-Young, Pedro da Rocha Pinto, Philippa Gardner. A Perspective on Specifying and Verifying Concurrent Modules. In Proceedings of the Journal of Logical and Algebraic Methods in Programming, 2018. [DOI]

The specification of a concurrent program module, and the verification of implementations and clients with respect to such a specification, are dicult problems. A specification should be general enough that any reasonable implementation satisfies it, yet precise enough that it can be used by any reasonable client. We survey a range of techniques for specifying concurrent modules, using the example of a counter module to illustrate the benefits and limitations of each. In particular, we highlight four key concepts underpinning these techniques: auxiliary state, interference abstraction, resource ownership and atomicity. We demonstrate how these concepts can be combined to achieve two powerful approaches for specifying concurrent modules and verifying implementations and clients, which remove the limitations highlighted by the counter example.
Gian Ntzik, Pedro da Rocha Pinto, Julian Sutherland, Philippa Gardner. A Concurrent Specification of POSIX File Systems. In Proceedings of the European Conference on Object-Oriented Programming, 2018. [DOI] [Technical report]

POSIX is a standard for operating systems, with a substantial part devoted to specifying file-system operations. File-system operations exhibit complex concurrent behaviour, comprising multiple actions affecting different parts of the state: typically, multiple atomic reads followed by an atomic update. However, the standard’s description of concurrent behaviour is unsatisfactory: it is fragmented; contains ambiguities; and is generally under-specified. We provide a formal concurrent specification of POSIX file systems and demonstrate scalable reasoning for clients. Our specification is based on a concurrent specification language, which uses a modern concurrent separation logic for reasoning about abstract atomic operations, and an associated refinement calculus. Our reasoning about clients highlights an important difference between reasoning about modules built over a heap, where the interference on the shared state is restricted to the operations of the module, and modules built over a file system, where the interference cannot be restricted as the file system is a public namespace. We introduce specifications conditional on context invariants used to restrict the interference, and apply our reasoning to the example of lock files

2017

Thomas Dinsdale-Young, Pedro da Rocha Pinto, Kristoffer Just Andersen, Lars Birkedal. Caper: Automatic Verification for Fine-grained Concurrency. In Proceedings of the European Symposium on Programming, 2017. [DOI] [Tool]

Recent program logics based on separation logic emphasise a modular approach to proving functional correctness for fine-grained concurrent programs. However, these logics have no automation support. In this paper, we present Caper, a prototype tool for automated reasoning in such a logic. Caper is based on symbolic execution, integrating reasoning about interference on shared data and about ghost resources that are used to mediate this interference. This enables Caper to verify the functional correctness of fine-grained concurrent algorithms.
Shale Xiong, Pedro da Rocha Pinto, Gian Ntzik, Philippa Gardner. Abstract Specifications for Concurrent Maps. In Proceedings of the European Symposium on Programming, 2017. [DOI] [Technical report]

Despite recent advances in reasoning about concurrent data structure libraries, the largest implementations in java.util.concurrent have yet to be verified. The key issue lies in the development of modular specifications, which provide clear logical boundaries between clients and implementations. A solution is to use recent advances in fine-grained concurrency reasoning, in particular the introduction of abstract atomicity to concurrent separation logic reasoning. We present two specifications of concurrent maps, both providing the clear boundaries we seek. We show that these specifications are equivalent, in that they can be built from each other. We show how we can verify client programs, such as a concurrent set and a producer-consumer client. We also give a substantial first proof that the main operations of ConcurrentSkipListMap in java.util.concurrent satisfy the map specification. This work demonstrates that we now have the technology to verify the largest implementations in java.util.concurrent.

2016

Pedro da Rocha Pinto. Reasoning with Time and Data Abstractions. PhD thesis, Imperial College London, 2016.

In this thesis, we address the problem of verifying the functional correctness of concurrent programs, with emphasis on fine-grained concurrent data structures. Reasoning about such programs is challenging since data can be concurrently accessed by multiple threads: the reasoning must account for the interference between threads, which is often subtle. To reason about interference, concurrent operations should either be at distinct times or on distinct data.
We present TaDA, a sound program logic for verifying clients and implementations that use abstract specifications that incorporate both abstract atomicity—the abstraction that operations take effect at a single, discrete instant in time—and abstract disjointness—the abstraction that operations act on distinct data resources. Our key contribution is the introduction of atomic triples, which offer an expressive approach for specifying program modules.
We also present Total-TaDA, a sound extension of TaDA with which we can verify total correctness of concurrent programs, i.e. that such programs both produce the correct result and terminate. With Total-TaDA, we can specify constraints on a thread's concurrent environment that are necessary to guarantee termination. This allows us to verify total correctness for nonblocking algorithms and express lock- and wait-freedom. More generally, the abstract specifications can express that one operation cannot impede the progress of another, a new non-blocking property that we call non-impedance.
Finally, we describe how to extend TaDA for proving abstract atomicity for data structures that make use of helping—where one thread is performing an abstract operation on behalf of another—and speculation—where an abstract operation is determined by future behaviour.
Pedro da Rocha Pinto, Thomas Dinsdale-Young, Philippa Gardner, Julian Sutherland. Modular Termination Verification for Non-blocking Concurrency. In Proceedings of the European Symposium on Programming, 2016. [DOI] [Technical report]

We present Total-TaDA, a program logic for verifying the total correctness of concurrent programs: that such programs both terminate and produce the correct result. With Total-TaDA, we can specify constraints on a thread's concurrent environment that are necessary to guarantee termination. This allows us to verify total correctness for non-blocking algorithms, e.g. a counter and a stack. Our specifications can express lock- and wait-freedom. More generally, they can express that one operation cannot impede the progress of another, a new non-blocking property we call non-impedance. Moreover, our approach is modular. We can verify the operations of a module independently, and build up modules on top of each other.

2015

Gian Ntzik, Pedro da Rocha Pinto, Philippa Gardner. Fault-tolerant Resource Reasoning. In Proceedings of the Asian Symposium on Programming Languages and Systems, 2015. [DOI]

Separation logic has been successful at verifying that programs do not crash due to illegal use of resources. The underlying assumption, however, is that machines do not fail. In practice, machines can fail unpredictably for various reasons, e.g. power loss, corrupting resources. Critical software, e.g. file systems, employ recovery methods to mitigate these effects. We introduce an extension of the Views framework to reason about such methods. We use concurrent separation logic as an instance of the framework to illustrate our reasoning, and explore programs using write-ahead logging, e.g. an ARIES recovery algorithm.
Pedro da Rocha Pinto, Thomas Dinsdale-Young, Philippa Gardner. Steps in Modular Specifications for Concurrent Modules (Invited Tutorial Paper). In Proceedings of the Conference on the Mathematical Foundations of Programming Semantics, 2015. [DOI]

The specification of a concurrent program module is a difficult problem. The specifications must be strong enough to enable reasoning about the intended clients without reference to the underlying module implementation. We survey a range of verification techniques for specifying concurrent modules, in particular highlighting four key concepts: auxiliary state, interference abstraction, resource ownership and atomicity. We show how these concepts combine to provide powerful approaches to specifying concurrent modules.

2014

Pedro da Rocha Pinto, Thomas Dinsdale-Young, Philippa Gardner. TaDA: A Logic for Time and Data Abstraction. In Proceedings of the European Conference on Object-Oriented Programming, 2014. [DOI] [Technical report]

To avoid data races, concurrent operations should either be at distinct times or on distinct data. Atomicity is the abstraction that an operation takes effect at a single, discrete instant in time, with linearisability being a well-known correctness condition which asserts that concurrent operations appear to behave atomically. Disjointness is the abstraction that operations act on distinct data resource, with concurrent separation logics enabling reasoning about threads that appear to operate independently on disjoint resources.
We present TaDA, a program logic that combines the benefits of abstract atomicity and abstract disjointness. Our key contribution is the introduction of atomic triples, which offer an expressive approach to specifying program modules. By building up examples, we show that TaDA supports elegant modular reasoning in a way that was not previously possible.

2011

Pedro da Rocha Pinto, Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, and Mark Wheelhouse. A Simple Abstraction for Complex Concurrent Indexes. In Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications, 2011. [DOI] [Technical report]

Indexes are ubiquitous. Examples include associative arrays, dictionaries, maps and hashes used in applications such as databases, file systems and dynamic languages. Abstractly, a sequential index can be viewed as a partial function from keys to values. Values can be queried by their keys, and the index can be mutated by adding or removing mappings. Whilst appealingly simple, this abstract specification is in sufficient for reasoning about indexes that are accessed concurrently.
We present an abstract specification for concurrent indexes. We verify several representative concurrent client applications using our specification, demonstrating that clients can reason abstractly without having to consider specific underlying implementations. Our specification would, however, mean nothing if it were not satisfied by standard implementations of concurrent indexes. We verify that our specification is satisfied by algorithms based on linked lists, hash tables and B-Link trees. The complexity of these algorithms, in particular the B-Link tree algorithm, can be completely hidden from the client’s view by our abstract specification.
Pedro da Rocha Pinto, Thomas Dinsdale-Young, Philippa Gardner, and Mark Wheelhouse. Abstract Reasoning for Concurrent Indexes. In Proceedings of Verification of Concurrent Data Structures, 2011.

2010

Pedro da Rocha Pinto. Reasoning about Concurrent Indexes. Master's thesis, Imperial College London, 2010.

Index data structures such as B+ trees and hash tables are used widely as the core of databases and file systems. In a world where concurrent systems are common as servers and largely increasing as personal computers, we need a way to make sure concurrent implementations do not contain bugs. We use the fact that multiple implementations share a common high-level specification and use concurrent abstract predicates to prove that an implementation satisfies such a specification. This approach allows us to reuse the abstract specification and enables high-level reasoning independent from the low-level implementation.

About Me

Research Interests

Publications

2018

2017

2016

2015

2014

2011

2010

Contact