Extending the theory of Owicki and Gries with a logic of progress

TL;DR

This paper develops a logic of progress for concurrent programs by integrating UNITY with the Owicki-Gries theory, using auxiliary variables and program counters to extend the existing framework.

Contribution

It introduces a novel approach to incorporate progress reasoning into the Owicki-Gries theory by adapting UNITY's rules with auxiliary variables and program counters.

Findings

Unified framework for progress in concurrent programs

Compatibility of UNITY-based progress logic with Owicki-Gries theory

Systematic use of auxiliary variables and program counters

Abstract

This paper describes a logic of progress for concurrent programs. The logic is based on that of UNITY, molded to fit a sequential programming model. Integration of the two is achieved by using auxiliary variables in a systematic way that incorporates program counters into the program text. The rules for progress in UNITY are then modified to suit this new system. This modification is however subtle enough to allow the theory of Owicki and Gries to be used without change.