Brand and Zafiropulo's notion of Communicating Finite-State Machines (CFSMs) provides a succinct and powerful model of message-passing concurrency, based around channels. However, a major variant of message-passing concurrency is not readily captured by CFSMs: the actor model. In this work, we define a variant of CFSMs, called Communicating Actor Automata, to capture the actor model of concurrency as provided by Erlang: with mailboxes, from which messages are received according to repeated application of pattern matching. Furthermore, this variant of CFSMs supports dynamic process topologies, capturing common programming idioms in the context of actor-based message-passing concurrency. This gives a new basis for modelling, specifying, and verifying Erlang programs. We also consider a class of CAAs that give rise to freedom from race conditions.
翻译：Brand 和 Zafiropulo 提出的“通信有限状态机”（CFSMs）提供了一种简洁而强大的消息传递并发模型，基于通道。然而，一种重要的消息传递并发的变体不易被 CFSMs 捕获：Actor 模型。在这项工作中，我们定义了一种 CFSMs 的变体，称为“通信 Actor 自动机”，以捕捉 Erlang 的 Actor 模型：具有邮箱，其中根据重复应用模式匹配接收消息。此外，这种 CFSMs 的变体支持动态进程拓扑，捕捉与基于 Actor 的消息传递并发相关的常见编程习惯。这为建模、规范和验证 Erlang 程序提供了新的基础。我们还考虑了一类导致自由竞态条件的 CAA。
相关内容
微信扫码咨询专知VIP会员