White Rose University Consortium logo
University of Leeds logo University of Sheffield logo York University logo

A framework for automated concurrency verification

Windsor, Matthew Bernard (2019) A framework for automated concurrency verification. PhD thesis, University of York.

[img]
Preview
Text
thesis.pdf - Examined Thesis (PDF)
Available under License Creative Commons Attribution-Noncommercial-No Derivative Works 2.0 UK: England & Wales.

Download (1458Kb) | Preview

Abstract

Reasoning systems based on Concurrent Separation Logic make verifying complex concurrent algorithms readily possible. Such algorithms contain subtle protocols of permission and resource transfer between threads; to cope with these intricacies, modern concurrent separation logics contain many moving parts and integrate many bespoke logical components. Verifying concurrent algorithms by hand consumes much time, effort, and expertise. As a result, computer-assisted verification is a fertile research topic, and fully automated verification is a popular research goal. Unfortunately, the complexity of modern concurrent separation logics makes them hard to automate, and the proliferation and fast turnover of such logics causes a downward pressure against building tools for new logics. As a result, many such logics lack tooling. This dissertation proposes Starling: a scheme for creating concurrent program logics that are automatable by construction. Starling adapts the existing Concurrent Views Framework for sound concurrent reasoning systems, overlaying a framework for reducing concurrent proof outlines to verification conditions in existing theories (such as those accepted by off-the-shelf sequential solvers). This dissertation describes Starling in a bottom-up, modular manner. First, it shows the derivation of a series of general concurrency proof rules from the Views framework. Next, it shows how one such rule leads to the Starling framework itself. From there, it outlines a series of increasingly elaborate frontends: ways of decomposing individual Hoare triples over atomic actions into verification conditions suitable for encoding into backend theories. Each frontend leads to a concurrent program logic. Finally, the dissertation presents a tool for verifying C-style concurrent proof outlines, based on one of the above frontends. It gives examples of such outlines, covering a variety of algorithms, backend solvers, and proof techniques.

Item Type: Thesis (PhD)
Related URLs:
Keywords: program verification, separation logic, formal methods, concurrency, program logics, Hoare logic
Academic Units: The University of York > Computer Science (York)
Identification Number/EthosID: uk.bl.ethos.794241
Depositing User: Mr Matthew Bernard Windsor
Date Deposited: 14 Jan 2020 17:02
Last Modified: 21 Feb 2020 10:53
URI: http://etheses.whiterose.ac.uk/id/eprint/25214

You do not need to contact us to get a copy of this thesis. Please use the 'Download' link(s) above to get a copy.
You can contact us about this thesis. If you need to make a general enquiry, please see the Contact us page.

Actions (repository staff only: login required)