Partial order semantics for concurrent program verification

多处理器机器现在占主导地位，因为大多数笔记本电脑，台式机，服务器，移动的电话和飞机通常都有多个到多个核心。不幸的是，并发编程容易出错，这现在影响了越来越多的并发趋势。让我们举个例子，最近在PostgreSQL数据库中发现的并发错误（参见http：//archives.postgresql.org/pgsql-hackers/2011-08/msg00330.php）。PostgreSQL是当今最流行的数据库之一，许多网站都依赖于它的正确功能。这个bug特别难以观察（而且还没有修复），因为它只发生在多核机器和特定的硬件平台IBM Power上。重现这样的bug和观察它们一样困难;因此测试很难发现它们。为了证明一个程序没有错误，我们希望设计出自动化的技术来分析代码而不执行它。这样，我们就可以减轻程序员编写程序证明的负担。然而，并发程序的自动验证是一个挑战，无论它是否旨在证明程序的完全正确性（例如，一个程序对一个列表进行排序实际上是对列表进行排序），或者在检查特定属性（例如，程序没有数据竞争）时缺乏完全正确性。我们在这里关注后者：我们想增强工具的可扩展性，检查并发程序是否违反某些安全关键属性的兴趣。我们想表明，可扩展的自动验证可以通过利用丰富的历史偏序建模并发实现。

Multiprocessor machines are now predominant, as most laptops, desktops,servers, mobile phones and aircrafts routinely have multiple to many cores.Unfortunately, concurrent programming is error-prone, which now affectseveryone given this trend towards more and more concurrency.Let us mention for example a recent concurrency bug found in the PostgreSQLdatabase (seehttp://archives.postgresql.org/pgsql-hackers/2011-08/msg00330.php). PostgreSQLis one of the most popular database nowadays, and many websites rely on itscorrect functioning. This bug was particularly difficult to observe (andindeed is not fixed yet) because it only occurred on a multicore machine, and aparticular hardware platform, IBM Power.Reproducing such bugs is as hard as observing them; thus testing can hardlydiscover them. To prove a program free of errors, we would like to deviseautomated techniques that analyse the code without executing it. Thus,we can relieve programmers from the burden of writing the proofs of theirprograms.Yet, automatic verification of concurrent programs represents a challenge,whether it aims at proving the full correctness of a program (e.g. aprogram sorting a list actually sorts the list), or at checking specificproperties (e.g. the program is free of data races) short of fullcorrectness. We focus here on the latter: we would like to enhancethe scalability of tools checking that a concurrent program does not violatecertain safety-critical properties of interest.We would like to show that scalable automatic verification can be achieved byexploiting the rich history of partial orders for modeling concurrency.