Weak Updates and Separation Logic
Last modified: Sat Oct 8 20:30:38 2011 GMT.
AbstractSeparation Logic (SL) provides a simple but powerful technique for reasoning about imperative programs that use shared data structures. Unfortunately, SL 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 SL when reasoning about the interaction between many high-level languages (e.g., ML, Java, C#) and low-level ones since these 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 SL with reference types and elegantly reasons about the interaction between strong and weak updates. We also 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.
PublishedIn New Generation Computing: Computing Paradigms and Computational Intelligence, Volume 29, No. 1, 2011, pages 1-29. © Ohmsha, Ltd. and Springer 2011.
An earlier version appeared in Proc. 7th Asian Symposium on Programming Languages and Systems (APLAS'09), Seoul, Korea, December 2009. Lecture Notes in Computer Science Vol. 5904, pages 178-193.
Copyright © 1996-2021 The FLINT Group
<flint at cs dot yale dot edu>
Yale University Department of Computer Science