Lockless data structures can be used with non-volatile memory devices to provide consistency across power loss or system crash. In this talk, Yan Li will briefly introduce existing lockless data structures, like doubly linked list and trees, and how to prove their correctness using PlusCal.