2026-08-03T10:54:58Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4771 2024-03-06T10:29:41Z ddc:004 open_access

Automatic Verification of Data Race Freedom in Device Drivers Deligiannis, Pantazis Donaldson, Alastair F. Device Drivers Verification Concurrency Data Races 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Pantazis Deligiannis and Alastair F. Donaldson 2014 Is Part Of OASIcs, Volume 43, 2014 Imperial College Computing Student Workshop InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/OASIcs.ICCSW.2014.36 urn:nbn:de:0030-drops-47715 https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ICCSW.2014.36 eng https://creativecommons.org/licenses/by/3.0/legalcode