Fast bug finding in lock-free data structures with CB-DPOR

This thesis describes CB-DPOR, an algorithm for quickly finding bugs in lock-free data structures. CB-DPOR is a combination of the CHESS and DPOR model checking algorithms. CB-DPOR performs similar to the concurrently developed preemption-bounded BPOR algorithm. CODEX is a tool for finding bugs in lock-free data structures. CODEX implements CBDPOR and this thesis demonstrates how to use CODEX to find bugs. This thesis describes new bugs in open-source lock-free data structures, and compares the performance of CBDPOR with the earlier model checking algorithms CHESS, DPOR, and PCT. CB-DPOR find bugs one to two orders of magnitude faster than earlier algorithms.

Department dc:contributor.department

Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science.

Grantor dc:publisher

Massachusetts Institute of Technology

Year dc:date.issued

2014

Author dc:creator

• Van den Hooff, Jelle (Jelle August)

Advisor dc:contributor.advisor

• M. Frans Kaashoek and Nickolai Zeldovich.

• Electrical Engineering and Computer Science.

Statement dc:rights

• M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission.

Licence dc:rights.uri

• http://dspace.mit.edu/handle/1721.1/7582

Language dc:language.iso

eng

Handle dc:identifier.uri

http://hdl.handle.net/1721.1/92058

OAI identifier oai:identifier

oai:dspace.mit.edu:1721.1/92058