The TAU Programming Languages and Systems Seminar - Program logics for asynchronous concurrency
Johannes Kloos, MPI-SWS
In this talk, I will be presenting work on capturing the semantics of this concurrency model in program logics. I will start by talking about a simple extension to concurrent separation logic that captures the behavior of such programs. After that, I will show how this logic can be extended to relational reasoning: We can use it to define a logic that allows us to provide observational refinement between two asynchronous programs. In particular, we introduce the notion of /delayed refinement/; in contrast to previous notions, which (roughly) required the pair of executions to start and end at the same time, delayed refinement allows us to reason about execution pairs whose components are executed at different times.