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 > Logic and Semantics Seminar (Computer Laboratory) > Fine-grained concurrency with separation logic
Fine-grained concurrency with separation logicAdd to your list(s) Download to your calendar using vCal
If you have a question about this talk, please contact Tom Ridge. (joint work with Kalpesh Kapoor and Kamal Lodaya) Separation Logic is a recent development in programming logic which has been applied by Peter O’Hearn to concurrency based on critical sections as well as semaphores. In this work, we go one step further and apply it to fine-grained concurrency. We note that O’Hearn’s formulation of Concurrent Separation Logic is by and large applicable to fine-grained concurrent programs with only minor adaptations. However, proving substantial properties of such programs involves the employment of sophisticated ``permissions’’ frameworks so that different processes can have different levels of access and exchange such access. We illustrate these techniques by showing the correctness proof of a concurrent garbage collector originally studied by Dijkstra et al. The original proof is based on informal reasoning, and it is said to have been very challenging to ensure its validity. Our techniques formalise this proof, but we find that there are significant details that need to be filled in. This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsAll Biological Anthropology Seminars and Events Darwin College Lecture Series Infrastructural Geographies - Department of GeographyOther talksRefugees and Migration Index of Suspicion: Predicting Cancer from Prescriptions Imaging techniques and novel tools for early detection and intervention TO A TRILLION AND BEYOND: THE FUTURE OF COMPUTING AND THE INTERNET OF THINGS - The IET Cambridge Prestige Lecture Development of a Broadly-Neutralising Vaccine against Blood-Stage P. falciparum Malaria Colorectal cancer. Part 1. Presentation, Diagnosis and Intervention. Part 2. Cellular signalling networks in colon cancer and the models to study them - a basic research perspective Lunchtime Talk: Helen's Bedroom Scale and anisotropic effects in necking of metallic tensile specimens From Euler to Poincare 'Cryptocurrency and BLOCKCHAIN – PAST, PRESENT AND FUTURE' Singularities of Hermitian-Yang-Mills connections and the Harder-Narasimhan-Seshadri filtration Panel Discussion: Climate Change Is Now |