More Web Proxy on the site http://driver.im/

article

GPS$$+$$+: Reasoning About Fences and Relaxed Atomics

Authors:

Viktor Vafeiadis,

João F. FerreiraAuthors Info & Claims

International Journal of Parallel Programming, Volume 46, Issue 6

Pages 1157 - 1183

https://doi.org/10.1007/s10766-017-0518-x

Published: 01 December 2018 Publication History

Abstract

In order to support efficient compilation to modern architectures, mainstream programming languages, such as C/C$$++$$++ and Java, have adopted weak (or relaxed) memory models. According to these weak memory models, multithreaded programs are allowed to exhibit behaviours that would have been inconsistent under the traditional strong (i.e., sequentially consistent) memory model. This makes the task of reasoning about concurrent programs even more challenging. The GPS framework, developed by Turon et al. (ACM OOPSLA, pp 691---707, 2014), has made a step forward towards tackling this challenge for the release---acquire fragment of the C11 memory model. By integrating ghost states, per-location protocols and separation logic, GPS can successfully verify programs with release---acquire atomics. In this paper, we introduced GPS$$+$$+ to support a larger class of C11 programs, that is, programs with release---acquire atomics, relaxed atomics and release---acquire fences. Key elements of our proposed logic include two new types of assertions, a more expressive resource model and a set of new verification rules.

References

[1]

Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '11, pp. 55---66. ACM, New York (2011)

Digital Library

[2]

Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: a practical system for verifying concurrent C. In: International Conference on Theorem Proving in Higher Order Logics (TPHOLs '09), pp. 23---42 (2009)

Digital Library

[3]

da Rocha Pinto, P., Dinsdale-Young, T., Gardner, P.: TaDA: a logic for time and data abstraction. In: ECOOP, pp. 207---231 (2014)

Digital Library

[4]

Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M.J., Vafeiadis, V.: Concurrent abstract predicates. In: ECOOP, pp. 504---528 (2010)

Digital Library

[5]

Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M.J., Yang, H.: Views: compositional reasoning for concurrent programs. In: ACM POPL, pp. 287---300 (2013)

Digital Library

[6]

Dodds, M., Feng, X., Parkinson, M., Vafeiadis, V.: Deny-guarantee reasoning. In: ESOP, pp. 363---377 (2009)

Digital Library

[7]

Doko, M., Vafeiadis, V.: A Program Logic for C11 Memory Fences, pp. 413---430. Springer, Berlin (2016)

Digital Library

[8]

Feng, X.: Local rely-guarantee Reasoning. In: ACM POPL, pp. 315---327 (2009)

Digital Library

[9]

He, M., Vafeiadis, V., Qin, S., Ferreira, J.F.: GPS+: Reasoning About Fences and Relaxed Atomics (Technical Report) (2017). http://pls.tees.ac.uk/gpsp/report.pdf, School of Computing, Teesside University

[10]

ISO/IEC 9899:2011. Programming Language C (2011)

[11]

Jensen, J.B., Birkedal, L.: Fictional separation logic. In: ESOP, pp. 377---396 (2012)

Digital Library

[12]

Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM TOPLAS 5, 596---619 (1983)

Digital Library

[13]

Jung, R., Swasey, D., Sieczkowski, F., Svendsen, K., Turon, A., Birkedal, L., Dreyer, D.: Iris: monoids and invariants as an orthogonal basis for concurrent reasoning. In: ACM POPL, pp. 637---650 (2015)

Digital Library

[14]

Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. 28(9), 690---691 (1979)

Digital Library

[15]

Leino, K.R., Müller, P., Smans, J.: Verification of concurrent programs with Chalice. In: Foundations of Security Analysis and Design V, pp. 195---222 (2009)

Digital Library

[16]

Ley-Wild, R., Nanevski, A.: Subjective auxiliary state for coarse-grained concurrency. In: ACM POPL, pp. 561---574 (2013)

Digital Library

[17]

Manson, J., Pugh, W., Adve, S.V.: The Java memory model. In: ACM POPL, pp. 378---391 (2005)

Digital Library

[18]

Nanevski, A., Ley-Wild, R., Sergey, I., Delbianco, G.: Communicating state transition systems for fine-grained concurrent resources. In: ESOP, pp. 290---310 (2014)

Digital Library

[19]

O'Hearn, P.W.: Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375(1---3), 271---307 (2007)

Digital Library

[20]

Svendsen, K., Birkedal, L.: Impredicative concurrent abstract predicates. In: ESOP, pp. 149---168 (2014)

Digital Library

[21]

Tassarotti, J., Dreyer, D., Vafeiadis, V.: Verifying read-copy-update in a logic for weak memory. In: ACM PLDI, Portland, OR, USA (2015)

Digital Library

[22]

Turon, A., Dreyer, D., Birkedal, L.: Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. In: ICFP, pp. 377---390 (2013)

Digital Library

[23]

Turon, A., Vafeiadis, V., Dreyer, D.: GPS: Navigating weak memory with ghosts, protocols, and separation. In: ACM OOPSLA, pp. 691---707 (2014)

Digital Library

[24]

Vafeiadis, V., Parkinson, M.J.: A marriage of rely/guarantee and separation logic. In: 18th International Conference on Concurrency Theory (CONCUR'07), volume 4703 of Lecture Notes in Computer Science, pp. 256---271 (2007)

Digital Library

[25]

Vafeiadis, V., Narayan, C.: Relaxed separation logic: a program logic for C11 concurrency. In: ACM OOPSLA, pp. 867---884 (2013)

Digital Library

Cited By

Dang HJung JChoi JNguyen DMansky WKang JDreyer DJhala RDillig I(2022)Compass: strong and compositional library specifications in relaxed memory separation logicProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523451(792-808)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523451
Krishna SGodbole AMeyer RChakraborty SMilani AWoelfel P(2022)Parameterized Verification under Release Acquire is PSPACE-completeProceedings of the 2022 ACM Symposium on Principles of Distributed Computing10.1145/3519270.3538445(482-492)Online publication date: 20-Jul-2022
https://dl.acm.org/doi/10.1145/3519270.3538445
Dang HJourdan JKaiser JDreyer D(2019)RustBelt meets relaxed memoryProceedings of the ACM on Programming Languages10.1145/33711024:POPL(1-29)Online publication date: 20-Dec-2019
https://dl.acm.org/doi/10.1145/3371102

GPS$$+$$+: Reasoning About Fences and Relaxed Atomics
1. Theory of computation

Recommendations

Taming release-acquire consistency
POPL '16

We introduce a strengthening of the release-acquire fragment of the C11 memory model that (i) forbids dubious behaviors that are not observed in any implementation; (ii) supports fence instructions that restore sequential consistency; and (iii) admits ...
Taming release-acquire consistency
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

We introduce a strengthening of the release-acquire fragment of the C11 memory model that (i) forbids dubious behaviors that are not observed in any implementation; (ii) supports fence instructions that restore sequential consistency; and (iii) admits ...
Detecting and Eliminating Potential Violations of Sequential Consistency for Concurrent C/C++ Programs
CGO '09: Proceedings of the 7th annual IEEE/ACM International Symposium on Code Generation and Optimization

When a concurrent shared-memory program written with a sequential consistency (SC) model is run on a machine implemented with a relaxed consistency (RC) model, it could cause SC violations that are very hard to debug. To avoid such violations, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image International Journal of Parallel Programming

International Journal of Parallel Programming Volume 46, Issue 6

December 2018

312 pages

ISSN:0885-7458

Issue’s Table of Contents

Copyright © Copyright © 2018 Springer Science+Business Media, LLC, part of Springer Nature.

Publisher

Kluwer Academic Publishers

United States

Publication History

Published: 01 December 2018

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 06 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Dang HJung JChoi JNguyen DMansky WKang JDreyer DJhala RDillig I(2022)Compass: strong and compositional library specifications in relaxed memory separation logicProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523451(792-808)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523451
Krishna SGodbole AMeyer RChakraborty SMilani AWoelfel P(2022)Parameterized Verification under Release Acquire is PSPACE-completeProceedings of the 2022 ACM Symposium on Principles of Distributed Computing10.1145/3519270.3538445(482-492)Online publication date: 20-Jul-2022
https://dl.acm.org/doi/10.1145/3519270.3538445
Dang HJourdan JKaiser JDreyer D(2019)RustBelt meets relaxed memoryProceedings of the ACM on Programming Languages10.1145/33711024:POPL(1-29)Online publication date: 20-Dec-2019
https://dl.acm.org/doi/10.1145/3371102

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents