TLDS provides a framework for developing transactional containers from lock-free ones. It includes five examples of transactional data structures, lock-free and obstruction-free versions of a linked list, and a skip list, and a lock-free hash map. We are currently working on supporting transactional data structures for non-linked containers and also transactions that are executed on multiple containers.
CCSpec is a tool that allows the user to check that their concurrent data structure meets a specified correctness condition. A correctness condition for a concurrent data structure defines the expected behavior of method calls. CCSpec can check any correctness condition in which a concurrent data structure is expected to exhibit equivalent behavior to the sequential counterpart.
Publications in Refereed Journals
, Damian Dechev, Transactional Correctness Tool for Abstract Data Types
, ACM Transactions on Architecture and Code Optimization, Vol. 14, No. 4, Article 37, November 2017.
Zachary Painter, Christina Peterson
, Damian Dechev, Lock-Free Transactional Adjacency List
, In Proceedings of the 30th International Workshop on Languages and Compilers for Parallel Computing (LCPC), College Station, TX, October 2017.
, Deli Zhang, Damian Dechev, Resource-Based Transaction Management for Best-Effort Hardware Transactional Memory
, In Proceedings of the The First Workshop on Software Engineering for Parallel Systems (SEPS) co-located with SPLASH 2014, Portland, OR, October 2014.