MikroKosmos: A Verification-Oriented Model Implementation of an STM in C#

This model implementation of software transactional memory (STM) is based on a 2006 version of the Bartok STM developed at Microsoft and this PLDI ’06 paper: Tim Harris, Mark Plesko, Avraham Shinnar, David Tarditi. "Optimizing Memory Transactions," June 2006. PLDI '06: ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation. This STM implementation is intended to serve as a benchmark for research on the verification of such implementations; it is not intended to provide a practical STM. To keep the code simple, it abstracts away features such as the multiuse object header word that the Bartok STM uses for interoperability with the rest of the runtime. Interaction with the garbage collector and contention manager are similarly abstracted away, and only features of the STM that ensure serializability of concurrent transactions are included in the code. This model STM implementation has the same API as the Bartok STM library, and its operations and atomic actions have the same granularity level as those of the Bartok STM. This distinguishes this detailed model implementation from an algorithm-level description of an STM implementation. This release also contains a simple test-bed demonstrating the usage of the STM primitives. This harness is the TestHarness class in the “modelSTM” project—Ali Sezgin, Serdar Tasiran, Tim Harris; August 2008.