Coq Formalization of the Habanero programming model

Formalization of the Habanero programming model programming model. We focus primarily on the formalization of safety properties, such as deadlock freedom and race freedom. The overarching goal of the project is to provide theoretical framework, read a Coq library, for the verification of synchronization mechanisms.

Publications

• Formalization of Habanero Phasers using Coq. Tiago Cogumbreiro, Jun Shirako, and Vivek Sarkar. JLAMP, 90:50–60, 2017. [Download PDF] [Online interpreter]
• Formalization of phase ordering. Tiago Cogumbreiro, Jun Shirako, and Vivek Sarkar. In Proceedings of PLACES'16, 2016. [Download PDF]

Overview

We are currently working on:

• deadlock-free subset of phaser operations
• async-finish

Using

Make sure you have OPAM installed.

To setup the requirements of this software do:

./configure.sh # to install dependencies and setup the environment

Dependencies

• OPAM for the development.
• Aniceto (installed automatically)