NDLI: DoubleChecker: efficient sound and precise atomicity checking

Please wait, while we are loading the content...

What exactly is inexact computation good for?

Taming the parallel effect zoo: extensible deterministic parallelism with LVish

Atomicity refinement for verified compilation

Surgical precision JIT compilers

First-class runtime generation of high-performance types using exotypes

Expressing and verifying probabilistic assertions

A theory of changes for higher-order languages: incrementalizing λ-calculi by static differentiation

Laws of concurrent programming

Adaptive, efficient, parallel execution of parallel programs

Compiler-assisted detection of transient memory errors

On abstraction refinement for program analyses in Datalog

End-to-end verification of stack-space bounds for C programs

Commutativity race detection

Tracelet-based code search in executables

A personal perspective on concurrency

Chlorophyll: synthesis-aided compiler for low-power spatial architectures

Don't sweat the small stuff: formal verification of C code without the pain

Persistent pointer information

Improving JavaScript performance by deconstructing the type system

A lightweight symbolic virtual machine for solver-aided host languages

A model counter for constraints over unbounded strings

Test-driven repair of data races in structured parallel programs

DoubleChecker: efficient sound and precise atomicity checking

Stochastic optimization of floating-point programs with tunable precision

Getting F-bounded polymorphism into shape

Compositional solution space quantification for probabilistic software analysis

Adapton: composable, demand-driven incremental computation

Globally precise-restartable execution of parallel programs

Compiler validation via equivalence modulo inputs

Hybrid top-down and bottom-up interprocedural analysis

VeriCon: towards verifying controller programs in software-defined networks

Race detection for Android applications

Resugaring: lifting evaluation sequences through syntactic sugar

Test-driven synthesis

Natural proofs for data structure manipulation in C using separation logic

Selective context-sensitivity guided by impact pre-analysis

Doppio: breaking the browser language barrier

FlashExtract: a framework for data extraction by examples

Modular control-flow integrity

Æminium: a permission based concurrent-by-default programming language approach

Herding cats: modelling, simulation, testing, and data-mining for weak memory

A framework for enhancing data reuse via associative reordering

Optimal inference of fields in row-polymorphic records

Slicing probabilistic programs

Specialization slicing

Accurate application progress analysis for large-scale parallel debugging

Automatic runtime error repair and containment via recovery shepherding

FlowDroid: precise context, flow, field, object-sensitive and lifecycle-aware taint analysis for Android apps

Verification modulo versions: towards usable verification

Race detection for event-driven mobile applications

SCCharts: sequentially constructive statecharts for safety-critical applications: HW/SW-synthesis for a conservative extension of synchronous statecharts

Code completion with statistical language models

Automating formal proofs for reactive systems

Introspective analysis: context-sensitivity, across the board

Dynamic enforcement of determinism in a parallel scripting language

Consolidation of queries with user-defined functions

Dynamic space limits for Haskell

Maximal sound predictive race detection with control flow abstraction

Fast: a transducer-based language for tree manipulation

DoubleChecker: efficient sound and precise atomicity checking

Content Provider	ACM Digital Library
Author	Sengupta, Aritra Bond, Michael D. Huang, Jipeng Biswas, Swarnendu
Abstract	Atomicity is a key correctness property that allows programmers to reason about code regions in isolation. However, programs often fail to enforce atomicity correctly, leading to atomicity violations that are difficult to detect. Dynamic program analysis can detect atomicity violations based on an atomicity specification, but existing approaches slow programs substantially. This paper presents DoubleChecker, a novel sound and precise atomicity checker whose key insight lies in its use of two new cooperating dynamic analyses. Its imprecise analysis tracks cross-thread dependences soundly but imprecisely with significantly better performance than a fully precise analysis. Its precise analysis is more expensive but only needs to process a subset of the execution identified as potentially involved in atomicity violations by the imprecise analysis. If DoubleChecker operates in single-run mode, the two analyses execute in the same program run, which guarantees soundness and precision but requires logging program accesses to pass from the imprecise to the precise analysis. In multi-run mode, the first program run executes only the imprecise analysis, and a second run executes both analyses. Multi-run mode trades accuracy for performance; each run of multi-run mode outperforms single-run mode, but can potentially miss violations. We have implemented DoubleChecker and an existing state-of-the-art atomicity checker called Velodrome in a high-performance Java virtual machine. DoubleChecker's single-run mode significantly outperforms Velodrome, while still providing full soundness and precision. DoubleChecker's multi-run mode improves performance further, without significantly impacting soundness in practice. These results suggest that DoubleChecker's approach is a promising direction for improving the performance of dynamic atomicity checking over prior work.
Starting Page	28
Ending Page	39
Page Count	12
File Format	PDF
ISBN	9781450327848
DOI	10.1145/2594291.2594323
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2014-06-09
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Atomicity checking Dynamic program analysis
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in