VaST - Validation of Software Transactional Memory

软件事务内存（STM）是一种用于具有共享内存的并发程序的同步机制。STM为程序员提供了一个高级的，易于使用的并发控制抽象，使他们从同步概念（如锁或信号量）的显式使用中解放出来。基本上，STM允许程序员将代码放入事务中，并让STM算法以全有或全无的方式保证事务的原子执行。到目前为止，已经提出了大量的事务存储器概念，以硬件，软件或组合（所谓的混合TM）实现TM，并且这些已经进入主流编程语言和处理器设计。为了实现高性能，即使面对数千个并行进程，STM也会尝试允许尽可能多的并发，将同步限制在正确性所需的最小量。STM的正确性通常形式化为称为不透明性的概念，说明事务的“看似原子的”执行。不透明度可以被看作是一个概念转移的数据库概念的可串行化的软件transactions;特别是增强它的意义中止transactions.The该项目的主要目标是开发一个验证工具箱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.