Memory management is notoriously difficult in a concurrent setting. The presence of garbage collection greatly simplifies the life of the programmer, eradicating many memory-related bugs. However, the heap space usage of garbage-collected programs can be tricky to understand and reason about, as there is no explicit program point where space is reclaimed.

We recently presented a Separation Logic with Space Credits to reason about heap space under garbage collection in a high-level, yet sequential, language.

In this talk, we scale up to a concurrent language. For this purpose, we introduce new "pointed-by-thread" assertions, which keep track of the existence of stack-to-heap pointers in a reasonably lightweight manner. We illustrate our logic on several lock-free data structures, unveiling their subtle heap space usage.