Describir: Fine-grained Concurrency with Separation Logic.