Syntactic Control of Interference for Separation Logic

Research output: Contribution to conference (unpublished)Paper

Standard

Syntactic Control of Interference for Separation Logic. / Reddy, Uday; Reynolds, JC.

2012. 323-336 Paper presented at POPL '12 -The 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Philadelphia, United States.

Research output: Contribution to conference (unpublished)Paper

Harvard

Reddy, U & Reynolds, JC 2012, 'Syntactic Control of Interference for Separation Logic', Paper presented at POPL '12 -The 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Philadelphia, United States, 25/01/12 - 27/01/12 pp. 323-336. https://doi.org/10.1145/2103621.2103695

APA

Reddy, U., & Reynolds, JC. (2012). Syntactic Control of Interference for Separation Logic. 323-336. Paper presented at POPL '12 -The 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Philadelphia, United States. https://doi.org/10.1145/2103621.2103695

Vancouver

Reddy U, Reynolds JC. Syntactic Control of Interference for Separation Logic. 2012. Paper presented at POPL '12 -The 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Philadelphia, United States. https://doi.org/10.1145/2103621.2103695

Author

Reddy, Uday ; Reynolds, JC. / Syntactic Control of Interference for Separation Logic. Paper presented at POPL '12 -The 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Philadelphia, United States.14 p.

Bibtex

@conference{dbcfd2913bd3400aad5bc49f55b5d632,
title = "Syntactic Control of Interference for Separation Logic",
abstract = "Separation Logic has witnessed tremendous success in recent years in reasoning about programs that deal with heap storage. Its success owes to the fundamental principle that one should keep separate areas of the heap storage separate in program reasoning. However, the way Separation Logic deals with program variables continues to be based on traditional Hoare Logic without taking any benefit of the separation principle. This has led to unwieldy proof rules suffering from lack of clarity as well as questions surrounding their soundness. In this paper, we extend the separation idea to the treatment of variables in Separation Logic, especially Concurrent Separation Logic, using the system of Syntactic Control of Interference proposed by Reynolds in 1978. We extend the original system with permission algebras, making it more powerful and able to deal with the issues of concurrent programs. The result is a streamined presentation of Concurrent Separation Logic, whose rules are memorable and soundness obvious. We also include a discussion of how the new rules impact the semantics and devise static analysis techniques to infer the required permissions automatically.",
keywords = "Separation Logic, Syntactic Control of Interference, Program Logic, Static Analysis, Conditional Critical Regions, Denotational Semantics, Concurrency, Fractional Permissions, Type Systems",
author = "Uday Reddy and JC Reynolds",
year = "2012",
month = jan
day = "1",
doi = "10.1145/2103621.2103695",
language = "English",
pages = "323--336",
note = "POPL '12 -The 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages ; Conference date: 25-01-2012 Through 27-01-2012",

}

RIS

TY - CONF

T1 - Syntactic Control of Interference for Separation Logic

AU - Reddy, Uday

AU - Reynolds, JC

PY - 2012/1/1

Y1 - 2012/1/1

N2 - Separation Logic has witnessed tremendous success in recent years in reasoning about programs that deal with heap storage. Its success owes to the fundamental principle that one should keep separate areas of the heap storage separate in program reasoning. However, the way Separation Logic deals with program variables continues to be based on traditional Hoare Logic without taking any benefit of the separation principle. This has led to unwieldy proof rules suffering from lack of clarity as well as questions surrounding their soundness. In this paper, we extend the separation idea to the treatment of variables in Separation Logic, especially Concurrent Separation Logic, using the system of Syntactic Control of Interference proposed by Reynolds in 1978. We extend the original system with permission algebras, making it more powerful and able to deal with the issues of concurrent programs. The result is a streamined presentation of Concurrent Separation Logic, whose rules are memorable and soundness obvious. We also include a discussion of how the new rules impact the semantics and devise static analysis techniques to infer the required permissions automatically.

AB - Separation Logic has witnessed tremendous success in recent years in reasoning about programs that deal with heap storage. Its success owes to the fundamental principle that one should keep separate areas of the heap storage separate in program reasoning. However, the way Separation Logic deals with program variables continues to be based on traditional Hoare Logic without taking any benefit of the separation principle. This has led to unwieldy proof rules suffering from lack of clarity as well as questions surrounding their soundness. In this paper, we extend the separation idea to the treatment of variables in Separation Logic, especially Concurrent Separation Logic, using the system of Syntactic Control of Interference proposed by Reynolds in 1978. We extend the original system with permission algebras, making it more powerful and able to deal with the issues of concurrent programs. The result is a streamined presentation of Concurrent Separation Logic, whose rules are memorable and soundness obvious. We also include a discussion of how the new rules impact the semantics and devise static analysis techniques to infer the required permissions automatically.

KW - Separation Logic

KW - Syntactic Control of Interference

KW - Program Logic

KW - Static Analysis

KW - Conditional Critical Regions

KW - Denotational Semantics

KW - Concurrency

KW - Fractional Permissions

KW - Type Systems

U2 - 10.1145/2103621.2103695

DO - 10.1145/2103621.2103695

M3 - Paper

SP - 323

EP - 336

T2 - POPL '12 -The 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Y2 - 25 January 2012 through 27 January 2012

ER -