Building on the standard theory of process algebra with priorities, we identify a new scheduling mechanism, called "constructive reduction" which is designed to capture the essence of synchronous programming. The distinctive property of this evaluation strategy is to achieve determinacy-by-construction for multi-cast concurrent communication with shared memory. In the technical setting of CCS extended by clocks and priorities, we prove for a large class of "coherent" processes a confluence property for constructive reductions. We show that under some restrictions, called "pivotability", coherence is preserved by the operators of prefix, summation, parallel composition, restriction and hiding. Since this permits memory and sharing, we are able to cover a strictly larger class of processes compared to those in Milner's classical confluence theory for CCS without priorities.
翻译:在带有优先级的进程代数标准理论基础上,我们识别出一种称为"构造性归约"的新型调度机制,旨在捕捉同步编程的本质。该求值策略的独特属性在于,它能够针对具有共享内存的多播并发通信实现"构造即确定性"。在通过时钟和优先级扩展的CCS技术框架下,我们针对一大类"相干"进程证明了构造性归约的汇合性质。我们证明,在称为"轴心性"的某些限制条件下,前缀、求和、并行组合、限制和隐藏算子能够保持相干性。由于这允许内存与共享操作,因此相较于米勒在无优先级CCS经典汇合理论中所覆盖的进程类,我们能够涵盖严格更大规模的进程类别。