![]() |
COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. | ![]() |
University of Cambridge > Talks.cam > Semantics Lunch (Computer Laboratory) > Deny-guarantee reasoning
Deny-guarantee reasoningAdd to your list(s) Download to your calendar using vCal
If you have a question about this talk, please contact Sam Staton. NOTE THE UNUSUAL DAY AND VENUE. This talk is in the ARG lunch slot. Rely-guarantee is a well-established approach to reasoning about concurrent programs that use parallel composition. However, parallel composition is not how concurrency is structured in real systems. Instead, threads are started by `fork’ and collected with `join’ commands. This style of concurrency cannot be reasoned about using rely-guarantee, as the life-time of a thread can be scoped dynamically. With parallel composition the scope is static. In this paper, we introduce deny-guarantee reasoning, a reformulation of rely-guarantee that enables reasoning about dynamically scoped concurrency. We build on ideas from separation logic to allow interference to be dynamically split and recombined, in a similar way that separation logic splits and joins heaps. To allow this splitting, we use deny and guarantee permissions: a deny permission specifies that the environment cannot do an action, and guarantee permission allow us to do an action. We illustrate the use of our proof system with examples, and show that it can encode all the original rely-guarantee proofs. We also present the semantics and soundness of the deny-guarantee method. Joint work by Mike Dodds, Xinyu Feng, Matthew Parkinson, Viktor Vafeiadis. This talk is part of the Semantics Lunch (Computer Laboratory) series. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsCambridge Cancer Centre seminars Medieval Art Seminar Series Department of Pharmacology Lecture Theatre, Tennis Court RoadOther talksGraph Convolutional Networks for Natural Language Processing and Relational Modeling Characterizing Immunogenetic Mechanisms through HIV Disease Analysis Kidney cancer: the most lethal urological malignancy Zoo and Wildlife Work Finding the past: Medieval Coin Finds at the Fitzwilliam Museum CANCELLED DUE TO STRIKE ACTION Recent advances in understanding climate, glacier and river dynamics in high mountain Asia |