VaST - Validation of Software Transactional Memory

软件事务存储器(STM)是一种用于具有共享存储器的并发程序的同步机制。STM为程序员提供了一种高级的、易于使用的并发控制抽象，将他们从锁或信号量等同步概念的显式使用中解放出来。基本上，STM允许程序员将代码放入事务中，并让STM算法以全有或全无的方式自动保证事务的执行。到目前为止，已经提出了大量的事务存储器的概念，以硬件、软件或两者相结合的方式实现TMS(所谓的混合TMS)，并已进入主流编程语言和处理器设计。为了实现高性能，即使面对数千个并行进程，STM也试图允许尽可能多的并发性，将同步限制在正确所需的最低数量。STM的正确性通常在一个称为不透明度的概念中形式化，说明事务的“看似原子”执行。不透明度可被视为数据库可序列化概念向软件事务的概念转移；特别是通过中止事务的意义来增强它。该项目的主要目标是开发用于STM的验证工具箱。它将包括三个主要组成部分：(1)用于测试STM的方法(和工具)，(2)用于模型检测STM的方法(和工具)，以及(3)用于机械证明STM正确性的方法。因此，该项目将支持STM设计的整个生命周期，从早期设计阶段的快速原型到高性能、正式验证的STM算法的最终产品。

Software transactional memory (STM) is a synchronisation mechanism for concurrent programs with shared memory. STM provides programmers with a high-level, easy to use abstraction of concurrency control, freeing them from explicit usage of synchronisation concepts like locks or semaphores. Basically, an STM allows a programmer to put code into a transaction, and let the STM algorithm guarantee execution of the transaction atomically in an all-or-nothing fashion. Up to now, a large number of transactional memory concepts have been proposed, implementing TMs in hardware, in software or in a combination (so called hybrid TMs), and these have found their way into mainstream programming language and processor design. To achieve high performance even in the face of thousands of parallel processes, STMs try to allow for as much concurrency as possible, restricting synchronisation to the minimal amount necessary for correctness. Correctness of STMs is typically formalized in a notion called opacity, stating "seemingly atomic" execution of transactions. Opacity can be seen as a conceptual transferal of the database concept of serializability to software transactions; in particular enhancing it with meaning for aborting transactions.The key objective of this project is the development of a validation toolbox for STMs. It will include three main ingredients: (1) a method (and tool) for testing STMs, (2) a method (and tool) for model checking STMs and (3) a method for mechanically proving correctness of STMs. Thereby, this project shall support the whole lifecycle of STM design, from rapid prototyping in early design stages to the final product of a high performant, formally verified STM algorithm.