License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.ICCSW.2014.36
URN: urn:nbn:de:0030-drops-47715
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2014/4771/
Go to the corresponding OASIcs Volume Portal

Deligiannis, Pantazis ; Donaldson, Alastair F.

Automatic Verification of Data Race Freedom in Device Drivers

pdf-format:
8.pdf (0.5 MB)

Abstract

Device drivers are notoriously hard to develop and even harder to debug. They are typically prone to many serious issues such as data races. In this paper, we present static pair-wise lock set analysis, a novel sound verification technique for proving data race freedom in device drivers. Our approach not only avoids reasoning about thread interleavings, but also allows the reuse of existing successful sequential verification techniques.

BibTeX - Entry

@InProceedings{deligiannis_et_al:OASIcs:2014:4771,
  author =	{Pantazis Deligiannis and Alastair F. Donaldson},
  title =	{{Automatic Verification of Data Race Freedom in Device Drivers}},
  booktitle =	{2014 Imperial College Computing Student Workshop},
  pages =	{36--39},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-76-7},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{43},
  editor =	{Rumyana Neykova and Nicholas Ng},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2014/4771},
  URN =		{urn:nbn:de:0030-drops-47715},
  doi =		{10.4230/OASIcs.ICCSW.2014.36},
  annote =	{Keywords: Device Drivers, Verification, Concurrency, Data Races}
}

Keywords: Device Drivers, Verification, Concurrency, Data Races
Collection: 2014 Imperial College Computing Student Workshop
Issue Date: 2014
Date of publication: 08.10.2014

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI