Context-aware Trace Contracts

TL;DR

This paper introduces a program logic for context-aware trace contracts that specify the global behavior of asynchronous procedures, addressing the limitations of traditional contracts by incorporating call context and reducing complexity.

Contribution

It proposes a novel logic and proof system for context-aware trace contracts, enabling precise specification and analysis of asynchronous procedures' global behavior.

Findings

Introduces the observation quantifier for state observation during execution

Transfers behavioral subtyping principles to asynchronous procedure analysis

Provides a sound proof system for context-aware trace contracts

Abstract

The behavior of concurrent, asynchronous procedures depends in general on the call context, because of the global protocol that governs scheduling. This context cannot be specified with the state-based Hoare-style contracts common in deductive verification. Recent work generalized state-based to trace contracts, which permit to specify the internal behavior of a procedure, such as calls or state changes, but not its call context. In this article we propose a program logic of context-aware trace contracts for specifying global behavior of asynchronous programs. We also provide a sound proof system that addresses two challenges: To observe the program state not merely at the end points of a procedure, we introduce the novel concept of an observation quantifier. And to combat combinatorial explosion of possible call sequences of procedures, we transfer Liskov's principle of behavioral subtyping to the analysis of asynchronous procedures.