Technical reports

Concurrent Abstract Predicates

Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew Parkinson, Viktor Vafeiadis

April 2010, 43 pages

DOI: 10.48456/tr-777

Abstract

Abstraction is key to understanding and reasoning about large computer systems. Abstraction is simple to achieve if the relevant data structures are disjoint, but rather difficult when they are partially shared, as is the case for concurrent modules. We present a program logic for reasoning abstractly about data structures, that provides a fiction of disjointness and permits compositional reasoning. The internal details of a module are completely hidden from the client by concurrent abstract predicates. We reason about a module’s implementation using separation logic with permissions, and provide abstract specifications for use by client programs using concurrent abstract predicates. We illustrate our abstract reasoning by building two implementations of a lock module on top of hardware instructions, and two implementations of a concurrent set module on top of the lock module.

Full text

PDF (0.5 MB)

BibTeX record

@TechReport{UCAM-CL-TR-777,
  author =	 {Dinsdale-Young, Thomas and Dodds, Mike and Gardner,
          	  Philippa and Parkinson, Matthew and Vafeiadis, Viktor},
  title = 	 {{Concurrent Abstract Predicates}},
  year = 	 2010,
  month = 	 apr,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-777.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-777},
  number = 	 {UCAM-CL-TR-777}
}