Expressing the Behavior of Three Very Different Concurrent Systems by Using Natural Extensions of Separation Logic

TL;DR

This paper demonstrates how natural extensions of Separation Logic can serve as a specification language for designing and expressing the behavior of diverse concurrent systems, including a Subway, Stopwatch, and 2x2 Switch.

Contribution

It introduces the use of Separation Logic extensions as a unified specification framework for various concurrent systems, bridging logic and system design.

Findings

Successfully expressed behaviors of three different systems

Extended Separation Logic effectively models concurrent system specifications

Shows potential for logic-based design in diverse hardware and software systems

Abstract

Separation Logic is a non-classical logic used to verify pointer-intensive code. In this paper, however, we show that Separation Logic, along with its natural extensions, can also be used as a specification language for concurrent-system design. To do so, we express the behavior of three very different concurrent systems: a Subway, a Stopwatch, and a 2x2 Switch. The Subway is originally implemented in LUSTRE, the Stopwatch in Esterel, and the 2x2 Switch in Bluespec.