84 results found
The development of mechanised language specification based on structured operational semantics, with applications to verified compilers and sound program analysis, requires huge effort. General theory and frameworks have been proposed to help with this effort. However, none of this work provides a systematic way of developing concrete and abstract semantics, connected together by a general consistency result. We introduce a skeletal semantics of a language, where each skeleton describes the complete semantic behaviour of a language construct. We define a general notion of interpretation, which provides a systematic and language-independent way of deriving semantic judgements from the skeletal semantics. We explore four generic interpretations: a simple well-formedness interpretation; a concrete interpretation; an abstract interpretation; and a constraint generator for flow-sensitive analysis. We prove general consistency results between interpretations, depending only on simple language-dependent lemmas. We illustrate our ideas using a simple While language.
Dinsdale-Young T, Pinto PDR, Gardner P, 2018, A perspective on specifying and verifying concurrent modules, JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, Vol: 98, Pages: 1-25, ISSN: 2352-2208
© Gian Ntzik, Pedro da Rocha Pinto, Julian Sutherland, and Philippa Gardner. POSIX is a standard for operating systems, with a substantial part devoted to specifying filesystem 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.
Gardner P, 2017, Verified trustworthy software systems, PHILOSOPHICAL TRANSACTIONS OF THE ROYAL SOCIETY A-MATHEMATICAL PHYSICAL AND ENGINEERING SCIENCES, Vol: 375, ISSN: 1364-503X
Xiong S, da Rocha Pinto P, Ntzik G, et al., 2017, Abstract Specifications for Concurrent Maps (Extended Version), Abstract Specifications for Concurrent Maps, Publisher: Department of Computing, Imperial College London, 2017/1
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.
© Springer-Verlag GmbH Germany 2017. 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.
Dinsdale-Young T, da Rocha Pinto P, Andersen KJ, et al., 2017, CAPER: Automatic verification for fine-grained concurrency, Pages: 420-447, ISSN: 0302-9743
© Springer-Verlag GmbH Germany 2017. 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.
da Rocha Pinto P, Dinsdale-Young T, Gardner P, et al., 2016, Modular Termination Verification for Non-blocking Concurrency (Extended Version), Modular Termination Verification for Non-blocking Concurrency, Publisher: Department of Computing, Imperial College London, 2016/6
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.
Pinto PDR, Dinsdale-Young T, Gardner P, et al., 2016, Modular Termination Verification for Non-blocking Concurrency, 25th European Symposium on Programming (ESOP) Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS), Publisher: SPRINGER-VERLAG BERLIN, Pages: 176-201, ISSN: 0302-9743
Raad A, Santos JF, Gardner P, 2016, DOM: Specification and client reasoning, Pages: 401-422, ISSN: 0302-9743
© Springer International Publishing AG 2016. We present an axiomatic specification of a key fragment of DOM using structural separation logic. This specification allows us to develop modular reasoning about client programs that call the DOM.
© Springer International Publishing AG 2016. We show how to verify four challenging concurrent finegrained graph-manipulating algorithms, including graph copy, a speculatively parallel Dijkstra, graph marking and spanning tree. We develop a reasoning method for such algorithms that dynamically tracks the contributions and responsibilities of each thread operating on a graph, even in cases of arbitrary recursive thread creation. We demonstrate how to use a logic without abstraction (CoLoSL) to carry out abstract reasoning in the style of iCAP, by building the abstraction into the proof structure rather than incorporating it into the semantic model of the logic.
Pinto PDR, Dinsdale-Young T, Gardner P, 2015, Steps in Modular Specifications for Concurrent Modules, Publisher: ELSEVIER SCIENCE BV, Pages: 3-18, ISSN: 1571-0661
Ntzik G, Gardner P, 2015, Reasoning about the POSIX File System Local Update and Global Pathnames, ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), Publisher: ASSOC COMPUTING MACHINERY, Pages: 201-220, ISSN: 0362-1340
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 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
Ntzik G, Pinto PDR, Gardner P, 2015, Fault-Tolerant Resource Reasoning, 13th Asian Symposium on Programming Languages and Systems (APLAS), Publisher: SPRINGER INT PUBLISHING AG, Pages: 169-188, ISSN: 0302-9743
Pinto PDR, Dinsdale-Young T, Gardner P, 2014, TaDA: A Logic for Time and Data Abstraction, 28th European Conference on Object-Oriented Programming (ECOOP), Publisher: SPRINGER-VERLAG BERLIN, Pages: 207-231, ISSN: 0302-9743
Gardner P, Raad A, Wheelhouse M, et al., 2014, Abstract local reasoning for concurrent libraries: Mind the gap, Pages: 147-166, ISSN: 1571-0661
© 2014 The Authors. We study abstract local reasoning for concurrent libraries. There are two main approaches: provide a specification of a library by abstracting from concrete reasoning about an implementation; or provide a direct abstract library specification, justified by refining to an implementation. Both approaches have a significant gap in their reasoning, due to a mismatch between the abstract connectivity of the abstract data structures and the concrete connectivity of the concrete heap representations. We demonstrate this gap using structural separation logic (SSL) for specifying a concurrent tree library and concurrent abstract predicates (CAP) for reasoning about a concrete tree implementation. The gap between the abstract and concrete connectivity emerges as a mismatch between the SSL tree predicates and CAP heap predicates. This gap is closed by an interface function I which links the abstract and concrete connectivity. In the accompanying technical report, we generalise our SSL reasoning and results to arbitrary concurrent data libraries.
Gardner P, Ntzik G, Wright A, 2014, Local Reasoning for the POSIX File System, 23rd European Symposium on Programming (ESOP), Publisher: SPRINGER-VERLAG BERLIN, Pages: 169-188, ISSN: 0302-9743
da Rocha Pinto P, Dinsdale-Young T, Gardner P, 2014, TaDA: A Logic for Time and Data Abstraction (Extended Version), TaDA: A Logic for Time and Data Abstraction, London, United Kingdom, Publisher: Department of Computing, Imperial College London, DTR14-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.
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
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.