热门标签：
Mac 多显示器 显示器扩展 requests patch 并发 Alpine Linux BSD Linux 电动汽车 全部标签

并发程序的非直觉行为：一个简单的例子

2025-01-18

作者在使用模型检查器检查一个简单的并发程序时，发现了令人惊讶的结果。程序包含两个并发进程P和Q，它们分别对变量n进行10次加1操作。直觉上，n的最终值应该在10到20之间。然而，模型检查器却发现了一种极端的交错执行，导致n的值最终为2。作者尝试用Go语言编写程序来重现这种行为，但未能成功，这表明这种极端交错在实际应用中极少出现。这个例子展示了并发程序中隐藏的复杂性，以及直觉在理解并发行为时的局限性。

阅读更多
(wyounas.github.io)
开发 非直觉行为

并发编程可视化指南：理解程序状态空间

2024-12-20

并发编程的复杂性在于难以枚举所有可能的状态。本文通过可视化方法，解释如何理解并发程序运行机制。文章首先介绍了程序状态的概念，即变量值和指令位置的组合，然后通过一个简单的C语言程序示例，展示了程序状态的转换过程以及状态空间的生成。接着，文章引入了并发程序，通过两个并发执行的程序P和Q，阐述了如何表示并发程序的状态以及状态空间的构建。最后，文章探讨了如何利用模型检查工具SPIN和LTL语言验证并发程序的正确性，强调了模型检查在确保并发程序正确性中的重要作用。

阅读更多
(wyounas.github.io)
开发 状态空间