A key difficulty in verifying shared-memory concurrent programs is reasoning compositionally about each thread in isolation. Existing verification techniques for fine-grained concurrency require reasoning about static global shared resource, impeding compositionality. This paper introduces the program logic of \colosl, where each thread is verified with respect to its subjective view of the global shared state. This subjective view describes only that part of the global shared resource accessed by the thread. Subjective views may arbitrarily overlap with each other, and expand and contract depending on the resource required by the thread.
Thu 16 AprDisplayed time zone: Azores change
Thu 16 Apr
Displayed time zone: Azores change
14:00 - 16:00 | |||
14:00 30mTalk | Propositional Reasoning about Safety and Termination of Heap-Manipulating Programs ESOP Cristina David University of Oxford, Daniel Kroening University of Oxford, Matt Lewis University of Oxford | ||
14:30 30mTalk | Full reduction in the face of absurdity ESOP | ||
15:00 30mTalk | CoLoSL: Concurrent Local Subjective Logic ESOP Azalea Raad Imperial College London, Jules Villard Imperial College London, Philippa Gardner Imperial College London | ||
15:30 30mTalk | A Separation Logic for Fictional Sequential Consistency ESOP Filip Sieczkowski Aarhus University, Kasper Svendsen Aarhus University, Lars Birkedal Aarhus University, Jean Pichon-Pharabod University of Cambridge |