TLDS: Transactional Lock-free Data Structures

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

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.

Tervel

Tervel is a framework and library that unifies methodologies and techniques to enable the efficient implementation of wait-free algorithms. It includes a unified memory reclamation structure, progress assurance scheme, and a construct that limits recursive helping. It advocates a call-back centric design pattern to reduce code duplication, observable states, and improve code readability.