NDLI: Maximal sound predictive race detection with control flow abstraction

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

Maximal sound predictive race detection with control flow abstraction

Content Provider	ACM Digital Library
Author	Meredith, Patrick O'Neil Rosu, Grigore Huang, Jeff
Abstract	Despite the numerous static and dynamic program analysis techniques in the literature, data races remain one of the most common bugs in modern concurrent software. Further, the techniques that do exist either have limited detection capability or are unsound, meaning that they report false positives. We present a sound race detection technique that achieves a provably higher detection capability than existing sound techniques. A key insight of our technique is the inclusion of abstracted control flow information into the execution model, which increases the space of the causal model permitted by classical happens-before or causally-precedes based detectors. By encoding the control flow and a minimal set of feasibility constraints as a group of first-order logic formulae, we formulate race detection as a constraint solving problem. Moreover, we formally prove that our formulation achieves the maximal possible detection capability for any sound dynamic race detector with respect to the same input trace under the sequential consistency memory model. We demonstrate via extensive experimentation that our technique detects more races than the other state-of-the-art sound race detection techniques, and that it is scalable to executions of real world concurrent applications with tens of millions of critical events. These experiments also revealed several previously unknown races in real systems (e.g., Eclipse) that have been confirmed or fixed by the developers. Our tool is also adopted by Eclipse developers.
Starting Page	337
Ending Page	348
Page Count	12
File Format	PDF
ISBN	9781450327848
DOI	10.1145/2594291.2594315
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2014-06-09
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Control flow Data race Maximal sound Prediction
Content Type	Text
Resource Type	Article

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

Maximal sound predictive race detection with control flow abstraction

Sound predictive race detection in polynomial time

Sound predictive race detection in polynomial time.

Sound Predictive Race Detection in Polynomial Time

Precise and maximal race detection from incomplete traces

Simulation for RFID-Based Red Light Violation Detection: Violation Detection and Flow Prediction

Parametric flows: automated behavior equivalencing for symbolic analysis of races in cuda programs.

IPA: improving predictive analysis with pointer analysis

Neural network based VO2max prediction models using maximal exercise and non-exercise data

Maximal sound predictive race detection with control flow abstraction

Similar Documents

Maximal sound predictive race detection with control flow abstraction

Sound predictive race detection in polynomial time

Sound predictive race detection in polynomial time.

Sound Predictive Race Detection in Polynomial Time

Precise and maximal race detection from incomplete traces

Simulation for RFID-Based Red Light Violation Detection: Violation Detection and Flow Prediction

Parametric flows: automated behavior equivalencing for symbolic analysis of races in cuda programs.

IPA: improving predictive analysis with pointer analysis

Neural network based VO2max prediction models using maximal exercise and non-exercise data

Maximal sound predictive race detection with control flow abstraction