Ghost signals: verifying termination of busy waiting

DOI10.1007/978-3-030-81688-9_2MaRDI QIDQ832247zbMATH OpenOpenAlexFDO

Authors Tobias Reinhard, Bart Jacobs

Publication date 25 March 2022

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2010.11762

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Abstract: Programs for multiprocessor machines commonly perform busy waiting for synchronization. We propose the first separation logic for modularly verifying termination of such programs under fair scheduling. Our logic requires the proof author to associate a ghost signal with each busy-waiting loop and allows such loops to iterate while their corresponding signal $s$ is not set. The proof author further has to define a well-founded order on signals and to prove that if the looping thread holds an obligation to set a signal $s^{p}rime$, then $s^{p}rime$ is ordered above $s$. By using conventional shared state invariants to associate the state of ghost signals with the state of data structures, programs busy-waiting for arbitrary conditions over arbitrary data structures can be verified.

Recommendations

• Modular termination verification for non-blocking concurrency
• scientific article; zbMATH DE number 2011469
• A program logic for concurrent objects under fair scheduling
• Barriers in Concurrent Separation Logic
• Synchronizing the asynchronous

Cites work

• scientific article; zbMATH DE number 1841809 (Why is no real title available?)
• A Basis for Verifying Multi-threaded Programs
• A New Type System for Deadlock-Free Processes
• A program logic for concurrent objects under fair scheduling
• An axiomatic basis for computer programming
• Concurrent separation logic and operational semantics
• Deadlock-free channels and locks
• Deadlock-free monitors
• Higher-order ghost state
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• Modular termination verification for non-blocking concurrency
• The category-theoretic solution of recursive metric-space equations

Cited in

(1)

• scientific article; zbMATH DE number 2011469 (Why is no real title available?)

Describes a project that uses

Uses Software

• GitHub
• VeriFast
• ESC/Java

This page was built for publication: Ghost signals: verifying termination of busy waiting

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q832247)