Building on the classical theory of process algebra with priorities, we identify a new scheduling mechanism, called "sequentially constructive reduction" which is designed to capture the essence of synchronous programming. The distinctive property of this evaluation strategy is to achieve determinism-by-construction for multi-cast concurrent communication. In particular, it permits us to model shared memory multi-threading with reaction to absence as it lies at the core of the programming language Esterel. In the technical setting of CCS extended by clocks and priorities, we prove for a large class of processes, which we call "structurally coherent" the confluence property for constructive reductions. We further show that under some syntactic restrictions, called "pivotable" the operators of prefix, summation, parallel composition, restriction and hiding preserve structural coherence. This covers a strictly larger class of processes compared to those that are confluent in Milner's classical theory of CCS without priorities.
翻译:基于带有优先级的经典进程代数理论,我们定义了一种新的调度机制,称为“顺序构造性规约”,旨在捕捉同步编程的本质。该评估策略的独特性质在于实现多播并发通信的“构造即确定”。特别是,它允许我们对响应缺失的共享内存多线程进行建模,这正是编程语言Esterel的核心所在。在通过时钟与优先级扩展的CCS技术框架中,我们针对一类称为“结构协调”的广泛进程,证明了构造性规约的汇聚性质。进一步地,我们表明在称为“枢轴性”的某种语法限制下,前缀、求和、并行组合、限制及隐藏算子均保持结构协调性。与米勒无优先级经典CCS理论中汇聚的进程类相比,本文所覆盖的进程类严格更大。