Article

CheckFence: checking consistency of concurrent data types on relaxed memory models

Authors:

Sebastian Burckhardt,

Milo M. K. MartinAuthors Info & Claims

PLDI '07: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation

Pages 12 - 21

https://doi.org/10.1145/1250734.1250737

Published: 10 June 2007 Publication History

Abstract

Concurrency libraries can facilitate the development of multi-threaded programs by providing concurrent implementations of familiar data types such as queues or sets. There exist many optimized algorithms that can achieve superior performance on multiprocessors by allowing concurrent data accesses without using locks. Unfortunately, such algorithms can harbor subtle concurrency bugs. Moreover, they requirememory ordering fences to function correctly on relaxed memory models.

To address these difficulties, we propose a verification approach that can exhaustively check all concurrent executions of a given test program on a relaxed memory model and can verify that they are observationally equivalent to a sequential execution. Our CheckFence prototype automatically translates the C implementation code and the test program into a SAT formula, hands the latter to a standard SAT solver, and constructs counter example traces if there exist incorrect executions. Applying CheckFence to five previously published algorithms, we were able to (1) find several bugs (some not previously known), and (2) determine how to place memory ordering fences for relaxed memory models.

References

[1]

M. Abadi, C. Flanagan, and S. Freund. Types for safe locking: Static race detection for Java. ACM Trans. Program. Lang. Syst., 28(2):207--255, 2006.

Digital Library

[2]

S. Adve and K. Gharachorloo. Shared memory consistency models: a tutorial. Computer, 29(12):66--76, 1996.

Digital Library

[3]

H.-J. Boehm. Threads cannot be implemented as a library. In Programming Language Design and Implementation (PLDI), pages 261--268, 2005.

Digital Library

[4]

S. Burckhardt, R. Alur, and M. Martin. Bounded verification of concurrent data types on relaxed memory models: a case study. In Computer-Aided Verification (CAV), LNCS 4144, pages 489--502. Springer, 2006.

Digital Library

[5]

E. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS 2988, pages 168--176. Springer, 2004.

[6]

R. Colvin, L. Groves, V. Luchangco, and M. Moir. Formal verification of a lazy concurrent list-based set algorithm. In Computer--Aided Verification (CAV), LNCS 4144, pages 475--488. Springer, 2006.

Digital Library

[7]

Compaq Computer Corporation. Alpha Architecture Reference Manual, 4th edition, January 2002.

[8]

D. Detlefs, C. Flood, A. Garthwaite, P. Martin, N. Shavit, and G. Steele. Even better DCAS-based concurrent deques. In Conference on Distributed Computing (DISC), LNCS 1914, pages 59--73. Springer, 2000.

Digital Library

[9]

D. Dill, S. Park, and A. Nowatzyk. Formal specification of abstract memory models. In Symposium on Research on Integrated Systems, pages 38--52. MIT Press, 1993.

Digital Library

[10]

S. Doherty, D. Detlefs, L. Grove, C. Flood, V. Luchangco, P. Martin, M. Moir, N. Shavit, and G. Steele. DCAS is not a silver bullet for nonblocking algorithm design. In Symposium on Parallel Algorithms and Architectures (SPAA), pages 216--224, 2004.

Digital Library

[11]

X. Fang, J. Lee, and S. Midkiff. Automatic fence insertion for shared memory multiprocessing. In International Conference on Supercomputing (ICS), pages 285--294, 2003.

Digital Library

[12]

C. Flanagan and S. Freund. Type-based race detection for Java. In Programming Language Design and Implementation (PLDI), pages 219--232, 2000.

Digital Library

[13]

B. Frey. PowerPC Architecture Book v2.02. International Business Machines Corporation, 2005.

[14]

H. Gao and W. Hesslink. A formal reduction for lock-free parallel algorithms. In Computer--Aided Verification (CAV), LNCS 3114, pages 44--56. Springer, 2004.

[15]

G. Gopalakrishnan, Y. Yang, and H. Sivaraj. QB or not QB: An efficient execution verification tool for memory orderings. In Computer-Aided Verification (CAV), LNCS 3114, pages 401--413, 2004.

[16]

T. Harris. A pragmatic implementation of non-blocking linked-lists. In Conference on Distributed Computing (DISC), LNCS 2180, pages 300--314. Springer, 2001.

Digital Library

[17]

T. Harris, K. Fraser, and I. Pratt. A practical multi-word compare-and swap operation. In Conference on Distributed Computing (DISC), LNCS 2508, pages 265--279. Springer, 2002.

Digital Library

[18]

S. Heller, M. Herlihy, V. Luchangco, M. Moir, W. Scherer, and N. Shavit. A lazy concurrent list-based set algorithm. In Principles of Distributed Systems (OPODIS), 2005.

Digital Library

[19]

T. Henzinger, R. Jhala, and R. Majumdar. Race checking by context inference. In Programming language design and implementation (PLDI), pages 1--13, 2004.

Digital Library

[20]

Intel Corporation. Intel 64 and IA-32 Architectures Software Developer's Manual, Volume 3A, November 2006.

[21]

Intel Corporation. Intel Itanium Architecture Software Developer's Manual, Book 2, rev. 2.2, January 2006.

[22]

Intel Corporation. Intel Threading Building Blocks, September 2006.

[23]

International Business Machines Corporation. Architecture Principles of Operation, first edition, December 2000.

[24]

B. Jacobs, J. Smans, F. Piessens, and W. Schulte. A simple sequential reasoning approach for sound modular verification of mainstream multithreaded programs. In TV'06 Workshop, Federated Logic Conference (FLoC), pages 66--77, 2006.

[25]

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

Digital Library

[26]

L. Lamport. Checking a multithreaded algorithm with +CAL. In Conference on Distributed Computing (DISC), LNCS 4167, pages 151--163. Springer, 2006.

Digital Library

[27]

D. Lea. The java.util.concurrent synchronizer framework. In PODC Workshop on Concurrency and Synchronization in Java Programs (CSJP), 2004.

[28]

V. Luchangco. Personal communications, October 2006.

[29]

J. Manson, W. Pugh, and S. Adve. The Java memory model. In Principles of Programming Languages (POPL), pages 378--391, 2005.

Digital Library

[30]

M. Martin, D. Sorin, H. Cain, M. Hill, and M. Lipasti. Correctly implementing value prediction in microprocessors that support multithreading or multiprocessing. In International Symposium on Microarchitecture (MICRO), pages 328--337, 2001.

Digital Library

[31]

M. Michael. Scalable lock-free dynamic memory allocation. In Programming Language Design and Implementation (PLDI), pages 35--46, 2004.

Digital Library

[32]

M. Michael and M. Scott. Correction of a memory management method for lock-free data structures. Technical Report TR599, University of Rochester, 1995.

Digital Library

[33]

M. Michael and M. Scott. Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In Principles of Distributed Computing (PODC), pages 267--275, 1996.

Digital Library

[34]

M. Moir. Practical implementations of non-blocking synchronization primitives. In Principles of distributed computing (PODC), pages 219--228, 1997.

Digital Library

[35]

M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT solver. In Design Automation Conference (DAC), pages 530--535, 2001.

Digital Library

[36]

M. Naik, A. Aiken, and J. Whaley. Effective static race detection for Java. In Programming Language Design and Implementation (PLDI), pages 308--319, 2006.

Digital Library

[37]

G. Necula, S. McPeak, S. Rahul, and W. Weimer. CIL: Intermediate language and tools for analysis and transformation of C programs. In Conf. on Compiler Constr. (CC), 2002.

Digital Library

[38]

S. Park and D. Dill. An executable specification, analyzer and verifier for RMO. In Symposium on Parallel Algorithms and Architectures (SPAA), pages 34--41, 1995.

Digital Library

[39]

P. Pratikakis, J. Foster, and M. Hicks. LOCKSMITH: contextsensitive correlation analysis for race detection. In Programming Language Design and Implementation (PLDI), pages 320--331, 2006.

Digital Library

[40]

I. Rabinovitz and O. Grumberg. Bounded model checking of concurrent programs. In Computer-Aided Verification (CAV), LNCS 3576, pages 82--97. Springer, 2005.

Digital Library

[41]

S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. Anderson. Eraser: A dynamic data race detector for multithreaded programs. ACM Trans. Comp. Sys., 15(4):391--411, 1997.

Digital Library

[42]

D. Shasha and M. Snir. Efficient and correct execution of parallel programs that share memory. ACM Trans. Program. Lang. Syst., 10(2):282--312, 1988.

Digital Library

[43]

H. Sundell and P. Tsigas. Fast and lock-free concurrent priority queues for multi-thread systems. J. Parallel Distrib. Comput., 65(5):609--627, 2005.

Digital Library

[44]

H. Sutter and J. Larus. Software and the concurrency revolution. ACM Queue, 3(7):54--62, 2005.

Digital Library

[45]

O. Trachsel, C. von Praun, and T. Gross. On the effectiveness of speculative and selective memory fences. In International Parallel and Distributed Processing Symposium (IPDPS), 2006.

Digital Library

[46]

V. Vafeiadis, M. Herlihy, T. Hoare, and M. Shapiro. Proving correctness of highly-concurrent linearisable objects. In Principles and Practice of Parallel Programming (PPoPP), pages 129--136, 2006.

Digital Library

[47]

C. von Praun, T. Cain, J. Choi, and K. Ryu. Conditional memory ordering. In International Symposium on Computer Architecture (ISCA), 2006.

Digital Library

[48]

D. Weaver and T. Germond, editors. The SPARC Architecture Manual Version 9. PTR Prentice Hall, 1994.

Digital Library

[49]

M. Xu, R. Bodik, and M. Hill. A serializability violation detector for shared-memory server programs. In Programming Language Design and Implementation (PLDI), 2005.

Digital Library

[50]

E. Yahav and M. Sagiv. Automatically verifying concurrent queue algorithms. Electr. Notes Theor. Comput. Sci., 89(3), 2003.

[51]

Y. Yang, G. Gopalakrishnan, G. Lindstrom, and K. Slind. Nemos: A framework for axiomatic and executable specifications of memory consistency models. In International Parallel and Distributed Processing Symposium (IPDPS), 2004.

Cited By

Nagar KSahoo AChowdhury RJagannathan S(2024)Automated Robustness Verification of Concurrent Data Structure Libraries against Relaxed Memory ModelsProceedings of the ACM on Programming Languages10.1145/36898028:OOPSLA2(2578-2605)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689802
Margalit RChristakis MPradel M(2024)Robustness against the C/C++11 Memory ModelProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3685549(1881-1885)Online publication date: 11-Sep-2024
https://dl.acm.org/doi/10.1145/3650212.3685549
Haas TMaseli RMeyer RPonce de León H(2023)Static Analysis of Memory Models for SMT EncodingsProceedings of the ACM on Programming Languages10.1145/36228557:OOPSLA2(1618-1647)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622855
Show More Cited By

Recommendations

CheckFence: checking consistency of concurrent data types on relaxed memory models
Proceedings of the 2007 PLDI conference

Concurrency libraries can facilitate the development of multi-threaded programs by providing concurrent implementations of familiar data types such as queues or sets. There exist many optimized algorithms that can achieve superior performance on ...
DRFX: a simple and efficient memory model for concurrent programming languages
PLDI '10: Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation

The most intuitive memory model for shared-memory multithreaded programming is sequential consistency(SC), but it disallows the use of many compiler and hardware optimizations thereby impacting performance. Data-race-free (DRF) models, such as the ...
DRFx: An Understandable, High Performance, and Flexible Memory Model for Concurrent Languages

The most intuitive memory model for shared-memory multi-threaded programming is sequential consistency (SC), but it disallows the use of many compiler and hardware optimizations and thus affects performance. Data-race-free (DRF) models, such as the C++11 ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI '07: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation

June 2007

508 pages

ISBN:9781595936332

DOI:10.1145/1250734

General Chair:
Jeanne Ferrante
University of California, San Diego, USA
,
Program Chair:
Kathryn S. McKinley
University of Texas at Austin, USA

ACM SIGPLAN Notices Volume 42, Issue 6
Proceedings of the 2007 PLDI conference
June 2007
491 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1273442
Issue’s Table of Contents

Copyright © 2007 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 10 June 2007

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

PLDI '07

Sponsor:

PLDI '07: ACM SIGPLAN Conference on Programming Language Design and Implementation

June 10 - 13, 2007

California, San Diego, USA

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

232
Total Citations
View Citations
941
Total Downloads

Downloads (Last 12 months)27
Downloads (Last 6 weeks)14

Reflects downloads up to 19 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Nagar KSahoo AChowdhury RJagannathan S(2024)Automated Robustness Verification of Concurrent Data Structure Libraries against Relaxed Memory ModelsProceedings of the ACM on Programming Languages10.1145/36898028:OOPSLA2(2578-2605)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689802
Margalit RChristakis MPradel M(2024)Robustness against the C/C++11 Memory ModelProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3685549(1881-1885)Online publication date: 11-Sep-2024
https://dl.acm.org/doi/10.1145/3650212.3685549
Haas TMaseli RMeyer RPonce de León H(2023)Static Analysis of Memory Models for SMT EncodingsProceedings of the ACM on Programming Languages10.1145/36228557:OOPSLA2(1618-1647)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622855
Puthoor SLipasti M(2023)Turn-based Spatiotemporal Coherence for GPUsACM Transactions on Architecture and Code Optimization10.1145/359305420:3(1-27)Online publication date: 19-Jul-2023
https://dl.acm.org/doi/10.1145/3593054
Gorjiara HXu GDemsky BSherwood TBerger EKozyrakis C(2021)Jaaru: efficiently model checking persistent memory programsProceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems10.1145/3445814.3446735(415-428)Online publication date: 19-Apr-2021
https://dl.acm.org/doi/10.1145/3445814.3446735
Luo WDemsky BSherwood TBerger EKozyrakis C(2021)C11Tester: a race detector for C/C++ atomicsProceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems10.1145/3445814.3446711(630-646)Online publication date: 19-Apr-2021
https://dl.acm.org/doi/10.1145/3445814.3446711
Margalit RLahav O(2021)Verifying observational robustness against a c11-style memory modelProceedings of the ACM on Programming Languages10.1145/34342855:POPL(1-33)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434285
Gorjiara HXu GDemsky B(2020)Satune: synthesizing efficient SAT encodersProceedings of the ACM on Programming Languages10.1145/34282144:OOPSLA(1-32)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428214
Verma AKalita PPandey ARoy SMars JTang LXue JWu P(2020)Interactive debugging of concurrent programs under relaxed memory modelsProceedings of the 18th ACM/IEEE International Symposium on Code Generation and Optimization10.1145/3368826.3377910(68-80)Online publication date: 22-Feb-2020
https://dl.acm.org/doi/10.1145/3368826.3377910
Lahav OMargalit RMcKinley KFisher K(2019)Robustness against release/acquire semanticsProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3314221.3314604(126-141)Online publication date: 8-Jun-2019
https://dl.acm.org/doi/10.1145/3314221.3314604
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents