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: https://drops.dagstuhl.de/opus/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