Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Separation logic
O’Hearn P. Communications of the ACM62 (2):86-95,2019.Type:Article
Date Reviewed: Oct 28 2020

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.

Reviewer:  A. Squassabia Review #: CR147092 (2103-0060)
Bookmark and Share
  Featured Reviewer  
 
Classes And Objects (D.3.3 ... )
 
 
Semantics (D.3.1 ... )
 
 
General (F.0 )
 
Would you recommend this review?
yes
no
Other reviews under "Classes And Objects": Date
AFC developer’s workshop
Young M., Microsoft Press, Redmond, WA, 1998. Type: Book (9781572316973)
Nov 1 1998
Intermediate MFC
Broquard V., Prentice Hall PTR, Upper Saddle River, NJ, 1998. Type: Book (9780138482763)
Sep 1 1998
Objects, components, and frameworks with UML
D’Souza D., Wills A., Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999. Type: Book (9780201310122)
Mar 1 1999
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy