并发形式模型简述

网络基础设施在现代生活中的普及要求我们对网络基础进行审视，以确保其安全性。并发算法的形式化是网络的基石，也是分布式系统描述模型与框架研究中的一个长期领域。尽管已有多年研究，简洁表示并验证并发算法的挑战仍未解决。现有的形式化方法虽然强大，但往往无法以既全面又可扩展的方式捕捉真实世界并发的动态特性。本文回顾了并发形式模型随时间的演变，探讨了它们在推理真实世界网络程序方面的通用性和实用性。我们考察了四篇关于形式化并发的基础性论文：Hoare的《并行编程：一种公理化方法》、Milner的《移动过程演算》、O'Hearn的《资源、并发与局部推理》，以及近期Coq的Iris框架的发展。