TY - JOUR
T1 - Weak updates and separation logic
AU - Tan, Gang
AU - Shao, Zhong
AU - Feng, Xinyu
AU - Cai, Hongxu
N1 - Funding Information:
We thank Hongseok Yang for pointing out the connection between our work and Pottier’s work. We thank anonymous referees for suggestions and comments on an earlier version of this article. Gang Tan is supported in part by NSF grant CCF-0915157. Zhong Shao is supported in part by a gift from Microsoft and NSF grants CCF-0524545 and CCF-0811665. Xinyu Feng is supported in part by NSF grant CCF-0524545 and National Natural Science Foundation of China (grant No. 90818019).
PY - 2011/1
Y1 - 2011/1
N2 - 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 SL w, 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 SL w. Finally, we show how to extend SL w with concurrency.
AB - 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 SL w, 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 SL w. Finally, we show how to extend SL w with concurrency.
UR - http://www.scopus.com/inward/record.url?scp=79953011584&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=79953011584&partnerID=8YFLogxK
U2 - 10.1007/s00354-010-0097-5
DO - 10.1007/s00354-010-0097-5
M3 - Article
AN - SCOPUS:79953011584
VL - 29
SP - 3
EP - 29
JO - New Generation Computing
JF - New Generation Computing
SN - 0288-3635
IS - 1
ER -