concurrency.md

title: Concurrency
project_id: concurrency
menu: true
parent_menu: Research
menu_order: 4
sub_menu_order: 1

We develop formal reasoning techniques for concurrent programs, with a particular emphasis on concurrent program logics. Recently, various logics based on separation logic have been developed, by ourselves and others, to provide more modular abstract reasoning about concurrent programs. Our work has tackled a range of problems including data abstraction, abstract atomicity, fault-tolerance and progress. In particular, we have recently developed {% cite_details Dinsdale-Young2010Concurrent --text Concurrent Abstract Predicates %}, {% cite_details Dinsdale-Young2013Views --text Views %}, {% cite_details daRochaPinto2014TaDA --text TaDA %}, {% cite_details Raad2015CoLoSL --text CoLoSL %}, {% cite_details Ntzik2015Fault --text Fault-tolerant Concurrent Separation Logic %} and {% cite_details daRochaPinto2016Modular --text Total-TaDA %}.

We have applied our reasoning to, for example, algorithms for manipulating concurrent B-trees, skip lists from java.util.concurrent, graph algorithms and the POSIX file system. Our goal is to challenge and improve the state-of-the-art in concurrent reasoning, refining our logics to deal with more advanced concurrent programs, developing automated reasoning tools based on these logics, and applying our work to real-world concurrent programs.

Research Support

This research is supported by the EPSRC programme grant EP/K008528/1: REMS: Rigorous Engineering of Mainstream Systems and previously by the EPSRC programme grant EP/H008373/2: Resource Reasoning. We also have substantial collaboration with Thomas Dinsdale-Young, previously a PhD student and RA of Gardner and now an independent research fellow at the University of Aarhus.