poster

SCRATCH: a tool for automatic analysis of dma races

Authors:

Alastair F. Donaldson,

Daniel Kroening,

Philipp RuemmerAuthors Info & Claims

ACM SIGPLAN Notices, Volume 46, Issue 8

Pages 311 - 312

https://doi.org/10.1145/2038037.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

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
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
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: Proceedings of the 16th ACM symposium on Principles and practice of parallel programming

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

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

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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 12 February 2011

Published in SIGPLAN Volume 46, Issue 8

Check for updates

Author Tags

Qualifiers

Poster

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 24 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

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
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

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