Formalization of Habanero phasers using Coq

DOI10.1016/J.JLAMP.2017.02.006MaRDI QIDQ2360652zbMATH OpenOpenAlexFDO

Authors Tiago Cogumbreiro, Jun Shirako, Vivek Sarkar

Publication date 4 July 2017

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

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

zbMATH Keywords

synchronizationbarriersCoqformalizationphasers

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Abstract: Phasers pose an interesting synchronization mechanism that generalizes many collective synchronization patterns seen in parallel programming languages, including barriers, clocks, and point-to-point synchronization using latches or semaphores. This work characterizes scheduling constraints on phaser operations, by relating the execution state of two tasks that operate on the same phaser. We propose a formalization of Habanero phasers, May-Happen-In-Parallel, and Happens-Before relations for phaser operations, and show that these relations conform with the semantics. Our formalization and proofs are fully mechanized using the Coq proof assistant, and are available online.

Recommendations

• Design and verification of distributed phasers
• scientific article; zbMATH DE number 3958701
• Certifying synchrony for free
• scientific article; zbMATH DE number 1543321
• scientific article; zbMATH DE number 1361139

Cites work

• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• Detecting causal relationships in distributed computations: In search of the holy grail
• Time, clocks, and the ordering of events in a distributed system

Cited in

(3)

• Design and verification of distributed phasers
• On Reachability in Parameterized Phaser Programs
• Importing HOL Light into Coq

Describes a project that uses

Uses Software

• Coq
• Goldilocks

This page was built for publication: Formalization of Habanero phasers using Coq

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