同步调度接口的代数

在本文中，我们提出了一种同步调度接口的代数，它将布尔代数在逻辑和功能行为方面的表达能力与最小-最大-加算术在量化同步接口非功能方面相结合。该接口理论源于直觉模态逻辑的可实现性解释（也称为Curry-Howard同构或命题即类型原理）。由此产生的接口类型代数旨在为指定类型导向的、组合式的最坏情况调度界限分析提供一个通用框架。它涵盖了并发、多处理或多线程执行下的同步控制流，并允许对支持各种抽象的分析的精确性和覆盖范围做出精确陈述。本文通过一些取自网络流问题、最短路径、任务调度和同步编程中最坏情况响应时间的例子，说明了该代数的表达能力。