2018/07/21 by Melliès, Paul-André, Stefanesco, Léo
#F.3.1 #F.3.2 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Programming Languages (cs.PL)
paper · doi:10.48550/arxiv.1807.08117
Concurrent separation logic (CSL) is a specification logic for concurrent imperative programs with shared memory and locks. In this paper, we develop a concurrent and interactive account of the logic inspired by asynchronous game semantics. To every program C, we associate a pair of asynchronous transition systems [C]S and [C]L which describe the operational behavior of the Code when confronted to its Environment or Frame --- both at the level of machine states (S) and of machine instructions and locks (L). We then establish that every derivation tree π of a judgment Γ\vdash\P\C\Q\ defines a winning and asynchronous strategy [π]Sep with respect to both asynchronous semantics [C]S and [C]L. From this, we deduce an asynchronous soundness theorem for CSL, which states that the canonical map L:[C]S→[C]L from the stateful semantics [C]S to the stateless semantics [C]L satisfies a basic fibrational property. We advocate that this provides a clean and conceptual explanation for the usual soundness theorem of CSL, including the absence of data races.