Santa Claus: Formal analysis of a process-oriented solution
Santa Claus: Formal analysis of a process-oriented solution
复制标题
圣诞老人：面向过程的解决方案的形式分析
DOI：
10.1145/1734206.1734211
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
J. Pedersen
中科院分区：
文献类型：
--
作者：
P. Welch;J. Pedersen
随着多核处理器的商业化发展，编写多线程程序以利用这些新的硬件体系结构的挑战变得越来越紧迫。并发编程对于实现硬件提供的性能是必要的。传统方法将并发性作为一个高级主题呈现：它们已被证明难以使用，可以自信地进行推理，并扩展到高并发性水平。本文回顾了基于Hoare的通信顺序进程代数（CSP）的面向过程的设计，并提出这种并发性方法可以提供新手程序员易于管理的解决方案；也就是说，它们很容易设计和维护，它们的复杂性是可伸缩的，显然是正确的，并且相对容易使用形式推理和/或模型检查器进行验证。这些解决方案可以用传统的编程语言（通过CSP库）或专门的语言（如occam-π）以直接反映其形式表达式的方式开发。系统的开发不需要CSP形式化的专业知识，因为支持的数学已经融入了支持它的工具和语言。我们用Santa Claus问题来说明这些概念，该问题自1994年以来一直被用作并发机制的挑战。我们把这个问题看作一个控制系统的例子，产生外部信号报告内部状态的变化（对外部世界建模）。我们声称我们的occam-π解决方案是设计正确的，但随后进行了正式验证（使用CSP的FDR模型检查器），证明系统没有死锁和活动锁，产生的控制信号服从关键的顺序约束，并且系统具有关键的活动特性。
With the commercial development of multicore processors, the challenges of writing multithreaded programs to take advantage of these new hardware architectures are becoming more and more pertinent. Concurrent programming is necessary to achieve the performance that the hardware offers. Traditional approaches present concurrency as an advanced topic: they have proven difficult to use, reason about with confidence, and scale up to high levels of concurrency. This article reviews process-oriented design, based on Hoare's algebra of Communicating Sequential Processes (CSP), and proposes that this approach to concurrency leads to solutions that are manageable by novice programmers; that is, they are easy to design and maintain, that they are scalable for complexity, obviously correct, and relatively easy to verify using formal reasoning and/or model checkers. These solutions can be developed in conventional programming languages (through CSP libraries) or specialized ones (such as occam-π) in a manner that directly reflects their formal expression. Systems can be developed without needing specialist knowledge of the CSP formalism, since the supporting mathematics is burnt into the tools and languages supporting it. We illustrate these concepts with the Santa Claus problem, which has been used as a challenge for concurrency mechanisms since 1994. We consider this problem as an example control system, producing external signals reporting changes of internal state (that model the external world). We claim our occam-π solution is correct-by-design, but follow this up with formal verification (using the FDR model checker for CSP) that the system is free from deadlock and livelock, that the produced control signals obey crucial ordering constraints, and that the system has key liveness properties.
影响因子：
1.3
作者：
Ritson C
通讯作者：
Ritson C