VaST - Validation of Software Transactional Memory

点击翻译按钮获取中文摘要

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.