Separation logic

Reviewer: A. Squassabia

Formal reasoning about mutable data can be difficult when concurrency is present, for instance, when attempting mutation of the same data at the same time from multiple processors; or when aliasing is present, for instance, when the same data is non-local and mutation occurs within possibly sequential but independent contexts. This paper is a cursory introduction to, and a historical overview of, separation logic: a formal framework for reasoning about mutable data under concurrency. The reader interested in a deeper treatment will be pleased with the large and encompassing set of references provided. Separation logic allows for the construction of internally consistent models that, after excluding aliasing, provide formal means for either mechanical or human-assisted verification of the correctness of code. Past attempts at formal reasoning encompassing aliasing proved to be less fruitful than separation logic, which in turn, over the last couple of decades, has evolved into software tools of practical utility. The principles backing this value insist on developments affording the ability of separation logic to constrain reasoning within a local scope; to establish artifact ownership; to generate preconditions with mechanized reasoning; and to analyze code fragments compositionally-as opposed to needing to digest an entire code base. This latter ability in particular enables analysis to scale incrementally, validating larger codes a cluster at a time. According to the authors, there are vast opportunities for further work in this field. Progress with practical applications could be a panacea. As an observation, formal verification of correct behavior under partial failure was neither excluded nor explicitly mentioned as an area of opportunity for further work.