Title: Trace Properties from Separation Logic Specifications,
Abstract: We propose a formal approach for relating abstract separation logic library
specifications with the trace properties they enforce on interactions between a
client and a library. Separation logic with abstract predicates enforces a
resource discipline that constrains when and how calls may be made between a
client and a library. Intuitively, this can enforce a protocol on the
interaction trace. This intuition is broadly used in the separation logic
community but has not previously been formalised. We provide just such a
formalisation. Our approach is based on using wrappers which instrument library
code to induce execution traces for the properties under examination. By
considering a separation logic extended with trace resources, we prove that
when a library satisfies its separation logic specification then its wrapped
version satisfies the same specification and, moreover, maintains the trace
properties as an invariant. Consequently, any client and library implementation
that are correct with respect to the separation logic specification will
satisfy the trace properties.