[博客翻译]当最简单的并发程序违背所有直觉时

当最简单的并发程序违背所有直觉 我在模型检查器上运行一个看似简单的并发程序时，发现了一个令人着迷且出乎意料的现象。考虑以下代码： 如果我们同时运行P和Q，且n初始化为0，那么当这两个进程执行完它们的语句后，n的值会是多少呢？ 我原本以为n的最终值会在10到20之间。你怎么看？猜一猜。 我在Ben-Ari关于SPIN模型检查器的书中[1]看到了这个例子。他说他惊讶地发现，n的最终值可能低至2。我也感到震惊——这个结果完全违背了我的直觉...