Weak updates and separation logic

Gang Tan, Zhong Shao, Xinyu Feng, Hongxu Cai

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)

Abstract

Separation 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 SL w, 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; this framework is used to prove the soundness of SL w.

Original languageEnglish (US)
Title of host publicationProgramming Languages and Systems - 7th Asian Symposium, APLAS 2009, Proceedings
Pages178-193
Number of pages16
DOIs
StatePublished - Dec 28 2009
Event7th Asian Symposium on Programming Languages and Systems, APLAS 2009 - Seoul, Korea, Republic of
Duration: Dec 14 2009Dec 16 2009

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5904 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other7th Asian Symposium on Programming Languages and Systems, APLAS 2009
CountryKorea, Republic of
CitySeoul
Period12/14/0912/16/09

Fingerprint

Separation Logic
Update
Heap
High level languages
Reasoning
Soundness
Interaction
Java
Data structures
Data Structures
Mutation
Semantics
Logic
Invariant

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Tan, G., Shao, Z., Feng, X., & Cai, H. (2009). Weak updates and separation logic. In Programming Languages and Systems - 7th Asian Symposium, APLAS 2009, Proceedings (pp. 178-193). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5904 LNCS). https://doi.org/10.1007/978-3-642-10672-9_14
Tan, Gang ; Shao, Zhong ; Feng, Xinyu ; Cai, Hongxu. / Weak updates and separation logic. Programming Languages and Systems - 7th Asian Symposium, APLAS 2009, Proceedings. 2009. pp. 178-193 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{2541d21f87f844a8a132f3b264140e60,
title = "Weak updates and separation logic",
abstract = "Separation 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 SL w, 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; this framework is used to prove the soundness of SL w.",
author = "Gang Tan and Zhong Shao and Xinyu Feng and Hongxu Cai",
year = "2009",
month = "12",
day = "28",
doi = "10.1007/978-3-642-10672-9_14",
language = "English (US)",
isbn = "3642106714",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "178--193",
booktitle = "Programming Languages and Systems - 7th Asian Symposium, APLAS 2009, Proceedings",

}

Tan, G, Shao, Z, Feng, X & Cai, H 2009, Weak updates and separation logic. in Programming Languages and Systems - 7th Asian Symposium, APLAS 2009, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5904 LNCS, pp. 178-193, 7th Asian Symposium on Programming Languages and Systems, APLAS 2009, Seoul, Korea, Republic of, 12/14/09. https://doi.org/10.1007/978-3-642-10672-9_14

Weak updates and separation logic. / Tan, Gang; Shao, Zhong; Feng, Xinyu; Cai, Hongxu.

Programming Languages and Systems - 7th Asian Symposium, APLAS 2009, Proceedings. 2009. p. 178-193 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5904 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - Weak updates and separation logic

AU - Tan, Gang

AU - Shao, Zhong

AU - Feng, Xinyu

AU - Cai, Hongxu

PY - 2009/12/28

Y1 - 2009/12/28

N2 - Separation 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 SL w, 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; this framework is used to prove the soundness of SL w.

AB - Separation 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 SL w, 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; this framework is used to prove the soundness of SL w.

UR - http://www.scopus.com/inward/record.url?scp=72449203593&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=72449203593&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-10672-9_14

DO - 10.1007/978-3-642-10672-9_14

M3 - Conference contribution

SN - 3642106714

SN - 9783642106712

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 178

EP - 193

BT - Programming Languages and Systems - 7th Asian Symposium, APLAS 2009, Proceedings

ER -

Tan G, Shao Z, Feng X, Cai H. Weak updates and separation logic. In Programming Languages and Systems - 7th Asian Symposium, APLAS 2009, Proceedings. 2009. p. 178-193. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-10672-9_14