poster

SCRATCH: a tool for automatic analysis of dma races

Authors:

Alastair F. Donaldson,

Daniel Kroening,

Philipp RuemmerAuthors Info & Claims

PPoPP '11: Proceedings of the 16th ACM symposium on Principles and practice of parallel programming

Pages 311 - 312

https://doi.org/10.1145/1941553.1941604

Published: 12 February 2011 Publication History

Get Access

Abstract

We present the SCRATCH tool, which uses bounded model checking and k-induction to automatically analyse software for multicore processors such as the Cell BE, in order to detect DMA races.

References

[1]

M. Abadi and L. Lamport. The existence of refinement mappings. Theor. Comput. Sci., 82(2):253--284, 1991.

Digital Library

Google Scholar

[2]

A. Biere, A. Cimatti, E. M. Clarke, O. Strichman, and Y. Zhu. Bounded model checking. Advances in Computers, 58:118--149, 2003.

Google Scholar

[3]

E. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In TACAS, pages 168--176, 2004.

Crossref

Google Scholar

[4]

A. F. Donaldson, D. Kroening, and P. Rümmer. Automatic analysis of scratch-pad memory code for heterogeneous multicore processors. In TACAS, pages 280--295, 2010.

Digital Library

Google Scholar

[5]

IBM. Cell BE resource center, October 2009. http://www.ibm.com/developerworks/power/cell/.

Google Scholar

[6]

M. Sheeran, S. Singh, and G. Stålmarck. Checking safety properties using induction and a SAT-solver. In FMCAD, pages 108--125, 2000.

Digital Library

Google Scholar

Cited By

View all

Gadelha MIsmail HCordeiro L(2017)Handling loops in bounded model checking of C programs via k-inductionInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-015-0407-919:1(97-114)Online publication date: 1-Feb-2017
https://dl.acm.org/doi/10.1007/s10009-015-0407-9
Cordeiro Lde Lima Filho E(2016)SMT-Based Context-Bounded Model Checking for Embedded SystemsACM SIGSOFT Software Engineering Notes10.1145/2934240.293424741:3(1-6)Online publication date: 24-Jun-2016
https://dl.acm.org/doi/10.1145/2934240.2934247
Saidi SFalcone Y(2015)Dynamic Detection and Mitigation of DMA Races in MPSoCsProceedings of the 2015 Euromicro Conference on Digital System Design10.1109/DSD.2015.77(267-270)Online publication date: 26-Aug-2015
https://dl.acm.org/doi/10.1109/DSD.2015.77
Show More Cited By

Index Terms

SCRATCH: a tool for automatic analysis of dma races
1. Theory of computation
  1. Logic
    1. Programming logic
  2. Semantics and reasoning
    1. Program reasoning

Recommendations

Automatic analysis of DMA races using model checking and k-induction

Modern multicore processors, such as the Cell Broadband Engine, achieve high performance by equipping accelerator cores with small "scratch-pad" memories. The price for increased performance is higher programming complexity --- the programmer must ...
SCRATCH: a tool for automatic analysis of dma races
PPoPP '11

We present the SCRATCH tool, which uses bounded model checking and k-induction to automatically analyse software for multicore processors such as the Cell BE, in order to detect DMA races.
Handling loops in bounded model checking of C programs via k-induction

The first attempts to apply the k-induction method to software verification are only recent. In this paper, we present a novel proof by induction algorithm, which is built on the top of a symbolic context-bounded model checker and uses an iterative ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

PPoPP '11: Proceedings of the 16th ACM symposium on Principles and practice of parallel programming

February 2011

326 pages

ISBN:9781450301190

DOI:10.1145/1941553

General Chair:
Calin Cascaval
Qualcomm Research, USA
,
Program Chair:
Pen-Chung Yew
Academia Sinica, Taiwan and University of Minnesota at Twin Cities, USA

ACM SIGPLAN Notices Volume 46, Issue 8
PPoPP '11
August 2011
300 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2038037
Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 12 February 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Poster

Conference

PPoPP '11

Sponsor:

SIGPLAN

PPoPP '11: ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming

February 12 - 16, 2011

TX, San Antonio, USA

Acceptance Rates

Overall Acceptance Rate 230 of 1,014 submissions, 23%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
181
Total Downloads

Downloads (Last 12 months)9
Downloads (Last 6 weeks)3

Reflects downloads up to 23 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Gadelha MIsmail HCordeiro L(2017)Handling loops in bounded model checking of C programs via k-inductionInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-015-0407-919:1(97-114)Online publication date: 1-Feb-2017
https://dl.acm.org/doi/10.1007/s10009-015-0407-9
Cordeiro Lde Lima Filho E(2016)SMT-Based Context-Bounded Model Checking for Embedded SystemsACM SIGSOFT Software Engineering Notes10.1145/2934240.293424741:3(1-6)Online publication date: 24-Jun-2016
https://dl.acm.org/doi/10.1145/2934240.2934247
Saidi SFalcone Y(2015)Dynamic Detection and Mitigation of DMA Races in MPSoCsProceedings of the 2015 Euromicro Conference on Digital System Design10.1109/DSD.2015.77(267-270)Online publication date: 26-Aug-2015
https://dl.acm.org/doi/10.1109/DSD.2015.77
Donaldson AHaller LKroening D(2011)Strengthening induction-based race checking with lightweight static analysisProceedings of the 12th international conference on Verification, model checking, and abstract interpretation10.5555/1946284.1946297(169-183)Online publication date: 23-Jan-2011
https://dl.acm.org/doi/10.5555/1946284.1946297
Botincan MDodds MDonaldson AParkinson M(2011)Safe asynchronous multicore memory operationsProceedings of the 26th IEEE/ACM International Conference on Automated Software Engineering10.1109/ASE.2011.6100049(153-162)Online publication date: 6-Nov-2011
https://dl.acm.org/doi/10.1109/ASE.2011.6100049
Donaldson AKroening DRümmer P(2011)Automatic analysis of DMA races using model checking and k-inductionFormal Methods in System Design10.1007/s10703-011-0124-239:1(83-113)Online publication date: 1-Aug-2011
https://dl.acm.org/doi/10.1007/s10703-011-0124-2
Donaldson AHaller LKroening D(2011)Strengthening Induction-Based Race Checking with Lightweight Static AnalysisVerification, Model Checking, and Abstract Interpretation10.1007/978-3-642-18275-4_13(169-183)Online publication date: 2011
https://doi.org/10.1007/978-3-642-18275-4_13
Alhawi ORocha HGadelha MCordeiro LBatista E(2020)Verification and refutation of C programs based on k-induction and invariant inferenceInternational Journal on Software Tools for Technology Transfer10.1007/s10009-020-00564-1Online publication date: 18-May-2020
https://doi.org/10.1007/s10009-020-00564-1

View Options

Login options

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

Cited By

Index Terms

Recommendations

Automatic analysis of DMA races using model checking and k-induction

SCRATCH: a tool for automatic analysis of dma races

Handling loops in bounded model checking of C programs via k-induction