相序的形式化
Formalization of Phase Ordering
摘要：
相位器提出了一种有趣的同步机制，它概括了并行程序设计语言中的许多集体同步模式，包括屏障、时钟和使用锁存器或信号量的点对点同步。这项工作的特点调度约束相位器操作，有关的两个任务，在同一相位器上操作的执行状态。我们提出了一个形式化的Habanero相位器，可能发生的并行，和发生之前的相位器操作的关系，并表明这些关系符合语义。我们的形式化和证明是完全机械化的使用Coq证明助手，并可在网上。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
