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汇合理论中严格更广的进程类。