Local Reasoning for Global Graph Properties

Siddharth Krishna, Alexander J. Summers, Thomas Wies

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Separation logics are widely used for verifying programs that manipulate complex heap-based data structures. These logics build on so-called separation algebras, which allow expressing properties of heap regions such that modifications to a region do not invalidate properties stated about the remainder of the heap. This concept is key to enabling modular reasoning and also extends to concurrency. While heaps are naturally related to mathematical graphs, many ubiquitous graph properties are non-local in character, such as reachability between nodes, path lengths, acyclicity and other structural invariants, as well as data invariants which combine with these notions. Reasoning modularly about such graph properties remains notoriously difficult, since a local modification can have side-effects on a global property that cannot be easily confined to a small region. In this paper, we address the question: What separation algebra can be used to avoid proof arguments reverting back to tedious global reasoning in such cases? To this end, we consider a general class of global graph properties expressed as fixpoints of algebraic equations over graphs. We present mathematical foundations for reasoning about this class of properties, imposing minimal requirements on the underlying theory that allow us to define a suitable separation algebra. Building on this theory, we develop a general proof technique for modular reasoning about global graph properties expressed over program heaps, in a way which can be directly integrated with existing separation logics. To demonstrate our approach, we present local proofs for two challenging examples: a priority inheritance protocol and the non-blocking concurrent Harris list.

Original languageEnglish (US)
Title of host publicationProgramming Languages and Systems- 29th European Symposium on Programming, ESOP 2020 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings
EditorsPeter Müller
PublisherSpringer
Pages308-335
Number of pages28
ISBN (Print)9783030449131
DOIs
StatePublished - 2020
Event29th European Symposium on Programming, ESOP 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020 - Dublin, Ireland
Duration: Apr 25 2020Apr 30 2020

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12075 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference29th European Symposium on Programming, ESOP 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020
CountryIreland
CityDublin
Period4/25/204/30/20

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Local Reasoning for Global Graph Properties'. Together they form a unique fingerprint.

Cite this