Static race detection for device drivers: The goblint approach

Vesal Vojdani, Kalmer Apinis, Vootele Rõtov, Helmut Seidl, Varmo Vene, Ralf Vogler

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

63 Scopus citations

Abstract

Device drivers rely on fine-grained locking to ensure safe access to shared data structures. For human testers, concurrency makes such code notoriously hard to debug; for automated reasoning, dynamically allocated memory and low-level pointer manipulation poses significant challenges. We present a flexible approach to data race analysis, implemented in the open source Goblint static analysis framework that combines different pointer and value analyses in order to handle a wide range of locking idioms, including locks allocated dynamically as well as locks stored in arrays. To the best of our knowledge, this is the most ambitious effort, having lasted well over ten years, to create a fully automated static race detection tool that can deal with most of the intricate locking schemes found in Linux device drivers. Our evaluation shows that these analyses are sufficiently precise, but practical use of these techniques requires inferring environmental and domain-specific assumptions.

Original languageEnglish
Title of host publicationASE 2016 - Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering
EditorsSarfraz Khurshid, David Lo, Sven Apel
PublisherAssociation for Computing Machinery, Inc
Pages391-402
Number of pages12
ISBN (Electronic)9781450338455
DOIs
StatePublished - 25 Aug 2016
Event31st IEEE/ACM International Conference on Automated Software Engineering, ASE 2016 - Singapore, Singapore
Duration: 3 Sep 20167 Sep 2016

Publication series

NameASE 2016 - Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering

Conference

Conference31st IEEE/ACM International Conference on Automated Software Engineering, ASE 2016
Country/TerritorySingapore
CitySingapore
Period3/09/167/09/16

Keywords

  • Abstract interpretation
  • Concurrency
  • Race condition

Fingerprint

Dive into the research topics of 'Static race detection for device drivers: The goblint approach'. Together they form a unique fingerprint.

Cite this