About The Lab

Lab Projects

TLDS: Transactional Lock-free Data Structures

TLDS provides a framework for developing transactional containers from lock-free ones. It includes two examples of transactional data structures, a lock-free linked list and a lock-free skip list. 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.


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.