Deductive Verification of Weak Memory Programs with View-based Protocols (extended version)

TL;DR

This paper presents an extension of the VerCors verification tool to automatically verify weak memory concurrent programs using view-based protocols, bridging the gap between manual proofs and automation.

Contribution

It introduces VerCors-relaxed, an extension supporting weak memory models and automates verification of concurrent programs with permission-based separation logic.

Findings

Successfully encoded the SLR logic in VerCors-relaxed.

Automatically verified several weak memory concurrency examples.

Extended VerCors to support weak memory protocols and automations.

Abstract

Concurrent programming under weak memory concurrency faces substantial challenges to ensure correctness due to program behaviors that cannot be explained by thread interleaving, a.k.a. sequential consistency. While several program logics are proposed to reason about weak memory concurrency, their usage has been limited to intricate manual proofs. On the other hand, the VerCors verifier provides a rich toolset for automated deductive verification for sequential consistency. In this paper, we bridge this gap for automated deductive verification of weak memory concurrent programs with the VerCors deductive verification tool. We propose an approach to encode weak memory concurrency in VerCors. We develop VerCors-relaxed, where we extend the VerCors atomics support and bring concepts from several protocol automata to encode permission-based separation logics for weak memory concurrency models. To demonstrate the effectiveness of our approach, we encode the relaxed fragment of the SLR program logic, a recent state-of-the-art permission-based separation logic for weak memory concurrency in VerCors-relaxed, our extension of VerCors. We use the SLR encoding on VerCors-relaxed to automatically verify several examples from the literature within realistic performance.