Publications
122 results found
da Rocha Pinto PM, Dinsdale-Young T, Gardner P, et al., 2016, Modular termination veri cation for non-blocking concurrency (extended version), Departmental Technical Report: 16/6, Publisher: Department of Computing, Imperial College London, 16/6
We present Total-TaDA, a program logic for verifying thetotal correctness of concurrent programs: that such programs both terminateand produce the correct result. With Total-TaDA, we can specifyconstraints on a thread's concurrent environment that are necessary toguarantee termination. This allows us to verify total correctness for nonblockingalgorithms, e.g. a counter and a stack. Our speci cations canexpress lock- and wait-freedom. More generally, they can express thatone operation cannot impede the progress of another, a new non-blockingproperty we call non-impedance. Moreover, our approach is modular.We can verify the operations of a module independently, and build upmodules on top of each other.
da Rocha Pinto P, Gardner PA, Dinsdale-Young T, 2015, Steps in Modular Specifications for Concurrent Modules (Invited Tutorial Paper), Mathematical Foundations of Programming Semantics XXXI (MFPS 2015), ISSN: 1571-0661
Ntzik G, da Rocha Pinto P, Gardner PA, et al., 2015, Fault-tolerant resource reasoning, 13th Asian Symposium on Programming Languages and Systems, Publisher: Springer International Publishing, Pages: 169-188, ISSN: 0302-9743
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.
Ntzik G, Gardner P, 2015, Reasoning about the POSIX file system: Local update and global pathnames, 2015 ACM SIGPLAN International Conference on Object-Oriented Programming Systems Languages and Applications (OOPSLA 2015), Publisher: ACM, Pages: 201-220
We introduce a program logic for specifying a core sequential subset of the POSIX file system and for reasoning abstractly about client programs working with the file system. The challenge is to reason about the combination of local directory update and global pathname traversal (including '..' and symbolic links) which may overlap the directories being updated. Existing reasoning techniques are either based on first-order logic and do not scale, or on separation logic and can only handle linear pathnames (no '..' or symbolic links). We introduce fusion logic for reasoning about local update and global pathname traversal, introducing a novel effect frame rule to propagate the effect of a local update on overlapping pathnames. We apply our reasoning to the standard recursive remove utility (rm -r), discovering bugs in well-known implementations.
Ntzik G, da Rocha Pinto P, Gardner P, 2015, Fault-tolerant Resource Reasoning (Extended Version), London, United Kingdom, Publisher: Department of Computing, Imperial College London
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.
Ntzik G, Gardner P, 2015, Reasoning about the POSIX File System: Local Update and Global Pathnames, Technical Report
We introduce a program logic for specifying a core sequential subset of the POSIX file system and for reasoning abstractly about client programs working with the file system. The challenge is to reason about the combination of local directory update and global pathname traversal (including '..' and symbolic links) which may overlap the directories being updated. Existing reasoning techniques are either based on first-order logic and do not scale, or on separation logic and can only handle linear pathnames (no '..' or symbolic links). We introduce fusion logic for reasoning about local update and global pathname traversal, introducing a novel effect frame rule to propagate the effect of a local update on overlapping pathnames. We apply our reasoning to the standard recursive remove utility (rm -r), discovering bugs in well-known implementations.
Gardner P, Smith G, Watt C, et al., 2015, A Trusted Mechanised Specification of JavaScript: One Year On, 27th International Conference on Computer Aided Verification, Publisher: Springer, Pages: 3-10, ISSN: 0302-9743
The JSCert project provides a Coq mechanised specification of the core JavaScript language. A key part of the project was to develop a methodology for establishing trust, by designing JSCert in such a way as to provide a strong connection with the JavaScript standard, and by developing JSRef, a reference interpreter which was proved correct with respect to JSCert and tested using the standard Test262 test suite. In this paper, we assess the previous state of the project at POPL’14 and the current state of the project at CAV’15. We evaluate the work of POPL’14, providing an analysis of the methodology as a whole and a more detailed analysis of the tests. We also describe recent work on extending JSRef to include Google’s V8 Array library, enabling us to cover more of the language and to pass more tests.
Gardner PA, Raad A, Villard J, 2015, CoLoSL: Concurrent Local Subjective Logic, 24th European Symposium on Programming, ESOP 2015, Publisher: Springer, Pages: 710-735, ISSN: 0302-9743
Gardner P, Raad A, Wheelhouse M, et al., 2014, Abstract Local Reasoning for Concurrent Libraries: Mind the Gap, Mathematical Foundations of Programming Semantics Thirtieth Conference, MFPS 2014
Gardner P, Ntzik G, Wright A, 2014, Local Reasoning for the POSIX File System, 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014
da Rocha Pinto P, Dinsdale-Young T, Gardner P, 2014, TaDA: A logic for time and data abstraction (extended version), Departmental Technical Report: 14/7, Publisher: Department of Computing, Imperial College London, 14/7
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.
Bodin M, Chargueraud A, Filaretti D, et al., 2014, A Trusted Mechanised JavaScript Specification, 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Publisher: Association for Computing Machinery (ACM), Pages: 87-100, ISSN: 1523-2867
da Rocha Pinto P, Gardner P, Dinsdale-Young T, 2014, TaDA: A Logic for Time and Data Abstraction, European Conference on Object-Oriented Programming, ECOOP 2014, Publisher: Springer, Pages: 207-231, ISSN: 0302-9743
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.
Wood T, 2013, A Program Logic for Verification of Security Properties of Secure ECMAScript Programs
We present an Operational Semantics of the Secure ECMAScript (SES) language. We extend Separation Logic with a backpointer operator to permit reasoning about reachability in the object graph whilst maintaining local reasoning. We define inference rules in the extended logic for SES. Finally, we prove the correctness of the Membrane design pattern.
Felleisen M, Gardner P, 2013, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): Preface, ISBN: 9783642370359
Dinsdale-Young T, Birkedal L, Gardner P, et al., 2013, Views: compositional reasoning for concurrent programs, 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2013), Publisher: ACM, Pages: 287-300
Compositional abstractions underly many reasoning principles for concurrent programs: the concurrent environment is abstracted in order to reason about a thread in isolation; and these abstractions are composed to reason about a program consisting of many threads. For instance, separation logic uses formulae that describe part of the state, abstracting the rest; when two threads use disjoint state, their specifications can be composed with the separating conjunction. Type systems abstract the state to the types of variables; threads may be composed when they agree on the types of shared variables.In this paper, we present the "Concurrent Views Framework", a metatheory of concurrent reasoning principles. The theory is parameterised by an abstraction of state with a notion of composition, which we call views. The metatheory is remarkably simple, but highly applicable: the rely-guarantee method, concurrent separation logic, concurrent abstract predicates, type systems for recursive references and for unique pointers, and even an adaptation of the Owicki-Gries method can all be seen as instances of the Concurrent Views Framework. Moreover, our metatheory proves each of these systems is sound without requiring induction on the operational semantics.
Wickerson J, Dodds M, Parkinson MJ, 2013, Ribbon Proofs for Separation Logic., European Symposium on Programming (ESOP), Publisher: Springer, Pages: 189-208
Cardelli L, Gardner PA, 2012, Processes in space, Theoretical Computer Science, Vol: 431, Pages: 40-55, ISSN: 0304-3975
We introduce a geometric process algebra based on affine geometry, with the aim of describing the concurrent evolution of geometric structures in 3D space. We prove a relativity theorem stating that algebraic equations are invariant under rigid body transformations.
Gardner P, Maffeis S, Smith G, et al., 2012, Towards a program logic for JavaScript, POPL 2012, Publisher: ACM, Pages: 31-44
JavaScript has become the most widely used language for clientsideweb programming. The dynamic nature of JavaScript makesunderstanding its code notoriously difficult, leading to buggy programsand a lack of adequate static-analysis tools. We believe thatlogical reasoning has much to offer JavaScript: a simple descriptionof program behaviour, a clear understanding of module boundaries,and the ability to verify security contracts.We introduce a program logic for reasoning about a broad subsetof JavaScript, including challenging features such as prototypeinheritance and with. We adapt ideas from separation logic toprovide tractable reasoning about JavaScript code: reasoning abouteasy programs is easy; reasoning about hard programs is possible.We prove a strong soundness result. All libraries written in oursubset and proved correct with respect to their specifications willbe well-behaved, even when called by arbitrary JavaScript code.
Gardner P, Maffeis S, Smith G, 2012, Towards a Program Logic for JavaScript, ACM SIGPLAN NOTICES, Vol: 47, Pages: 31-44, ISSN: 0362-1340
JavaScript has become the most widely used language for client-side web programming. The dynamic nature of JavaScript makes understanding its code notoriously difficult, leading to buggy programs and a lack of adequate static-analysis tools. We believe that logical reasoning has much to offer JavaScript: a simple description of program behaviour, a clear understanding of module boundaries, and the ability to verify security contracts.We introduce a program logic for reasoning about a broad subset of JavaScript, including challenging features such as prototype inheritance and with. We adapt ideas from separation logic to provide tractable reasoning about JavaScript code: reasoning about easy programs is easy; reasoning about hard programs is possible. We prove a strong soundness result. All libraries written in our subset and proved correct with respect to their specifications will be well-behaved, even when called by arbitrary JavaScript code.
da Rocha Pinto P, Dinsdale-Young T, Dodds M, et al., 2011, A Simple Abstraction for Complex Concurrent Indexes, 2011 ACM international conference on Object oriented programming systems languages and applications, Publisher: Association for Computing Machinery, Pages: 845-864
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 insufficient for reasoning about indexes 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.
Pinto PDR, Dinsdale-Young T, Dodds M, et al., 2011, A Simple Abstraction for Complex Concurrent Indexes, ACM Sigplan Notices, Vol: 46, Pages: 845-864, ISSN: 1523-2867
Indexes – also known as associative arrays, dictionaries,maps, or hashes – are abstract data-structures with myriadapplications, from databases to dynamic languages. Abstractly,an index is a partial function from keys to values.Values can be queried by their keys, and the index can bemutated by adding or removing mappings. While appealinglysimple, this abstract view is insufficient for reasoningabout indexes that are accessed concurrently.In this paper, we introduce an abstract specification whichviews an index as a divisible resource. Multiple threads canaccess the index concurrently, yet threads can still reason locally.We show that this specification can be used to verifya number of client applications. Our abstract specificationwould mean little if it were not satisfied by the implementationsof concurrent indexes. We verify that our specificationis satisfied by linked list, hash table and BLink tree index implementations.During verification, we uncovered a subtlebug in the BLink tree algorithm.
Dinsdale-Young T, Gardner P, Wheelhouse M, 2011, Abstract local reasoning for program modules, Algebra and Coalgebra in Computer Science: 4th International Conference, CALCO 2011, Publisher: Springer Verlag, Pages: 36-39, ISSN: 0302-9743
Hoare logic ([7]) is an important tool for formally proving correctness properties of programs. It takes advantage of modularity by treating program fragments in terms of provable specifications. However, heap programs tend to break this type of modular reasoning by permitting pointer aliasing. For instance, the specification that a program reverses one list does not imply that it leaves a second list alone. To achieve this disjointness property, it is necessary to establish disjointness conditions throughout the proof. © 2011 Springer-Verlag.
da Rocha Pinto PM, Dinsdale-Young T, Dodds M, et al., 2011, A simple abstraction for complex concurrent indexes, Departmental Technical Report: 11/10, Publisher: Department of Computing, Imperial College London, 11/10
Indexes are ubiquitous. Examples include associative arrays,dictionaries, maps and hashes used in applications such asdatabases, file systems and dynamic languages. Abstractly, asequential index can be viewed as a partial function fromkeys to values. Values can be queried by their keys, andthe index can be mutated by adding or removing mappings.Whilst appealingly simple, this abstract specification is insufficientfor reasoning about indexes that are accessed concurrently.We present an abstract specification for concurrent indexes.We verify several representative concurrent client applicationsusing our specification, demonstrating that clientscan reason abstractly without having to consider specificunderlying implementations. Our specification would, however,mean nothing if it were not satisfied by standard implementationsof concurrent indexes. We verify that our specificationis satisfied by algorithms based on linked lists, hashtables and BLink trees. The complexity of these algorithms, inparticular the BLink tree algorithm, can be completely hiddenfrom the client’s view by our abstract specification.
Gardner P, Maffeis S, Smith G, 2011, Towards a program logic of JavaScript, Departmental Technical Report: 11/11, Publisher: Department of Computing, Imperial College London, 11/11
JavaScript has become the most widely used language for clientsideweb programming. The dynamic nature of JavaScript makesunderstanding its code notoriously difficult, leading to buggy programsand a lack of adequate static-analysis tools. We believe thatlogical reasoning has much to offer JavaScript: a simple descriptionof program behaviour, a clear understanding of module boundaries,and the ability to verify security contracts.We introduce a program logic for reasoning about a broad subsetof JavaScript, including challenging features such as prototypeinheritance and with. We adapt ideas from separation logic toprovide tractable reasoning about JavaScript code: reasoning abouteasy programs is easy; reasoning about hard programs is possible.We prove a strong soundness result. All libraries written in oursubset and proved correct with respect to their specifications willbe well-behaved, even when called by arbitrary JavaScript code.
Dinsdale-Young T, Gardner PA, Wheelhouse M, 2010, Abstraction and refinement in local reasoning, VSTTE 2010, Publisher: Springer Berlin Heidelberg, Pages: 199-215
Local reasoning has become a well-established technique in program verification, which has been shown to be useful at many different levels of abstraction. In separation logic, we use a low-level abstraction that is close to how the machine sees the program state. In context logic, we work with high-level abstractions that are close to how the clients of modules see the program state.We apply program refinement to local reasoning, demonstrating that high-level local reasoning is sound for module implementations.We consider two approaches: one that preserves the high-level locality at the low level; and one that breaks the high-level ’fiction’ of locality.
Gardner P, 2010, Reasoning about client-side web programs: invited talk, 2010 EDBT/ICDT Workshops (EDBT '10), Publisher: Association for Computing Machinery
Benedikt M, Florescu D, Gardner P, et al., 2010, Report on the EDBT/ICDT 2010 Workshop on Updates in XML, SIGMOD RECORD, Vol: 39, Pages: 54-57, ISSN: 0163-5808
Dinsdale-Young T, Gardner P, Wheelhouse M, 2010, Locality Refinement
We study refinement in the setting of local reasoning. Inparticular, we explore general translations that preserve and that breaklocality.
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.