Memory management is a challenging problem for many lockfree
and fine-grained locking data structures. In those environments, a
thread that removes a node from a data structure needs to delay the
actual deallocation until no other thread holds a reference to it.
Recently, hardware transactional memory (HTM) became available in
off-the shelf processors. In this talk, I will explore the application
of HTM to the construction of concurrent data structures in general and
memory management problem specifically. I will revisit several known
memory management techniques and discuss a novel technique that is
derived from epochs, a blocking quiescent technique. HTM helps to avoid
a common problem of epochs where delayed or failed threads prevent
memory reclamation. In transactional mode, HTM allows threads to abort
other threads that prevent progress otherwise. I describe this technique
in detail and discuss trade-offs compared to other techniques.
Experiments conducted on Intel Haswell and Power8 architectures will
also be discussed.
A second part of the talk will revisit model checking as a means to
verify the correctness of concurrent software. While model checking is a
powerful tool, scalability remains a concern due to the combinatorial
explosion in size of the state space. To circumvent that, I will present
a tool to translate a static analyzers reports of suspected race
conditions to instrumentation that can be exploited by a model checker
(Java Pathfinder). I will provide details of the instrumentation
algorithm and present experimental results.