Document Open Access Logo

Automatic Verification of Data Race Freedom in Device Drivers

Authors Pantazis Deligiannis, Alastair F. Donaldson

PDF
Thumbnail PDF

File

OASIcs.ICCSW.2014.36.pdf
  • Filesize: 0.49 MB
  • 4 pages

Document Identifiers

Author Details

Pantazis Deligiannis
Alastair F. Donaldson

Cite As Get BibTex

Pantazis Deligiannis and Alastair F. Donaldson. Automatic Verification of Data Race Freedom in Device Drivers. In 2014 Imperial College Computing Student Workshop. Open Access Series in Informatics (OASIcs), Volume 43, pp. 36-39, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014) https://doi.org/10.4230/OASIcs.ICCSW.2014.36

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.

Subject Classification

Keywords
  • Device Drivers
  • Verification
  • Concurrency
  • Data Races

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Thomas Ball, Ella Bounimova, Byron Cook, Vladimir Levin, Jakob Lichtenberg, Con McGarvey, Bohus Ondrusek, Sriram K Rajamani, and Abdullah Ustuner. Thorough static analysis of device drivers. ACM SIGOPS Operating Systems Review, 40(4):73-85, 2006. Google Scholar
  2. Ethel Bardsley, Adam Betts, Nathan Chong, Peter Collingbourne, Pantazis Deligiannis, Alastair F Donaldson, Jeroen Ketema, Daniel Liew, and Shaz Qadeer. Engineering a static verification tool for GPU kernels. In Proceedings of the 26th International Conference on Computer Aided Verification, 2014. Google Scholar
  3. Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K Rustan M Leino. Boogie: A modular reusable verifier for object-oriented programs. In Formal methods for Components and Objects, pages 364-387. Springer, 2006. Google Scholar
  4. Mike Barnett and K Rustan M Leino. Weakest-precondition of unstructured programs. ACM SIGSOFT Software Engineering Notes, 31(1):82-87, 2005. Google Scholar
  5. Adam Betts, Nathan Chong, Alastair Donaldson, Shaz Qadeer, and Paul Thomson. GPUVerify: a verifier for GPU kernels. In Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications, pages 113-132. ACM, 2012. Google Scholar
  6. Andy Chou, Junfeng Yang, Benjamin Chelf, Seth Hallem, and Dawson Engler. An empirical study of operating systems errors. In Proceedings of the eighteenth ACM Symposium on Operating Systems Principles, SOSP '01, pages 73-88. ACM, 2001. Google Scholar
  7. Edmund Clarke, Daniel Kroening, Natasha Sharygina, and Karen Yorav. Predicate abstraction of ANSI-C programs using SAT. Formal Methods in System Design, 25(2-3):105-127, 2004. Google Scholar
  8. Jonathan Corbet. Finding kernel problems automatically. https://lwn.net/Articles/87538/, 2004.
  9. Jonathan Corbet. The kernel lock validator. https://lwn.net/Articles/185666/, 2006.
  10. Jonathan Corbet, Alessandro Rubini, and Greg Kroah-Hartman. Linux device drivers (Third Edition). O'Reilly, 2005. Google Scholar
  11. Tayfun Elmas, Shaz Qadeer, and Serdar Tasiran. Goldilocks: A race and transaction-aware Java runtime. In Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '07, pages 245-255. ACM, 2007. Google Scholar
  12. Dawson Engler, Benjamin Chelf, Andy Chou, and Seth Hallem. Checking system rules using system-specific, programmer-written compiler extensions. In Proceedings of the 4th USENIX Symposium on Operating System Design and Implementation. USENIX, 2000. Google Scholar
  13. Cormac Flanagan and Stephen N Freund. FastTrack: Efficient and precise dynamic race detection. In Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '09, pages 121-133. ACM, 2009. Google Scholar
  14. Thomas A Henzinger, George C Necula, Ranjit Jhala, Gregoire Sutre, Rupak Majumdar, and Westley Weimer. Temporal-safety proofs for systems code. In Computer Aided Verification, pages 526-538. Springer, 2002. Google Scholar
  15. Brian W Kernighan, Dennis M Ritchie, and Per Ejeklint. The C programming language, volume 2. prentice-Hall Englewood Cliffs, 1988. Google Scholar
  16. Volodymyr Kuznetsov, Vitaly Chipounov, and George Candea. Testing closed-source binary device drivers with DDT. In Proceedings of the 2010 USENIX Annual Technical Conference. USENIX, 2010. Google Scholar
  17. Akash Lal, Shaz Qadeer, and Shuvendu K. Lahiri. A solver for reachability modulo theories. In Proceedings of the 24th International Conference on Computer Aided Verification, CAV'12, pages 427-443. Springer, 2012. Google Scholar
  18. Chris Lattner and Vikram Adve. LLVM: A compilation framework for lifelong program analysis &transformation. In International Symposium on Code Generation and Optimization, pages 75-86. IEEE, 2004. Google Scholar
  19. Madanlal Musuvathi, Shaz Qadeer, Thomas Ball, Gerard Basler, Piramanayagam Arumuga Nainar, and Iulian Neamtiu. Finding and reproducing heisenbugs in concurrent programs. In Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation, pages 267-280. USENIX, 2008. Google Scholar
  20. Robert O'Callahan and Jong-Deok Choi. Hybrid dynamic data race detection. In Proceedings of the 9th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP '03, pages 167-178. ACM, 2003. Google Scholar
  21. Oracle Corporation. Analyzing program performance with Sun WorkShop, Chapter 5: Lock analysis tool. http://docs.oracle.com/cd/E19059-01/wrkshp50/805-4947/6j4m8jrnd/index.html, 2010.
  22. Yoann Padioleau, Julia Lawall, René Rydhof Hansen, and Gilles Muller. Documenting and automating collateral evolutions in Linux device drivers. In Proceedings of the 3rd ACM SIGOPS/EuroSys European Conference on Computer Systems, Eurosys '08, pages 247-260. ACM, 2008. Google Scholar
  23. Eli Pozniansky and Assaf Schuster. Efficient on-the-fly data race detection in multithreaded C++ programs. In Proceedings of the 9th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP '03, pages 179-190. ACM, 2003. Google Scholar
  24. Polyvios Pratikakis, Jeffrey S. Foster, and Michael Hicks. LOCKSMITH: Context-sensitive correlation analysis for race detection. In Proceedings of the 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '06, pages 320-331. ACM, 2006. Google Scholar
  25. Shaz Qadeer and Dinghao Wu. KISS: Keep it simple and sequential. In Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation, PLDI '04, pages 14-24. ACM, 2004. Google Scholar
  26. Zvonimir Rakamaric and Alan J Hu. Automatic inference of frame axioms using static analysis. In Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering, pages 89-98. IEEE, 2008. Google Scholar
  27. Matthew J Renzelmann, Asim Kadav, and Michael M Swift. SymDrive: Testing drivers without devices. In Proceedings of the 10th USENIX Symposium on Operating Systems Design and Implementation. USENIX, 2012. Google Scholar
  28. Leonid Ryzhyk, Peter Chubb, Ihor Kuz, and Gernot Heiser. Dingo: Taming device drivers. In Proceedings of the 4th ACM European conference on Computer systems, pages 275-288. ACM, 2009. Google Scholar
  29. Stefan Savage, Michael Burrows, Greg Nelson, Patrick Sobalvarro, and Thomas Anderson. Eraser: A dynamic data race detector for multithreaded programs. ACM Transactions on Computer Systems, 15(4):391-411, 1997. Google Scholar
  30. Nicholas Sterling. WARLOCK - A static data race analysis tool. In Proceedings of the 1993 Winter USENIX Conference, pages 97-106. USENIX, 1993. Google Scholar
  31. Michael M. Swift, Brian N. Bershad, and Henry M. Levy. Improving the reliability of commodity operating systems. In Proceedings of the nineteenth ACM Symposium on Operating Systems Principles, SOSP '03, pages 207-222. ACM, 2003. Google Scholar
  32. Jan Wen Voung, Ranjit Jhala, and Sorin Lerner. RELAY: Static race detection on millions of lines of code. In Proceedings of the the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The Foundations of Software Engineering, pages 205-214. ACM, 2007. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact