Weak Updates and Separation Logic
Separation logic provides a simple but powerful technique for reasoning about low-level imperative programs that use shared data structures. Unfortunately, separation logic supports only "strong updates," in which mutation to a heap location is safe only if a unique reference is owned. This limits the applicability of separation logic when reasoning about the interaction between many high-level languages (e.g., ML, Java, C#) and low-level ones since the high-level languages do not support strong updates. Instead, they adopt the discipline of "weak updates," in which there is a global "heap type" to enforce the invariant of type-preserving heap updates. We present SLW, a logic that extends separation logic with reference types and elegantly reasons about the interaction between strong and weak updates. We describe a semantic framework for reference types, which is used to prove the soundness of SLW. Finally, we show how to extend SLW with concurrency.
weak updates separation logic type systems mutable references language interoperation