2012 | OriginalPaper | Buchkapitel
Demonic Testing of Concurrent Programs
verfasst von : Scott West, Sebastian Nanz, Bertrand Meyer
Erschienen in: Formal Methods and Software Engineering
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Testing presents a daunting challenge for concurrent programs, as non-deterministic scheduling defeats reproducibility. The problem is even harder if, rather than testing entire systems, one tries to test individual components, for example to assess them for thread-safety. We present
demonic testing
, a technique combining the tangible results of unit testing with the rigour of formal rely-guarantee reasoning to provide deterministic unit testing for concurrent programs. Deterministic execution is provided by abstracting threads away via rely-guarantee reasoning, and replacing them with “demonic” sequences of interfering instructions that drive the program to break invariants. Demonic testing reuses existing unit tests to drive the routine under test, using the execution to discover demonic interference. Programs carry contract-based rely-guarantee style specifications to express what sort of thread interference should be tolerated. Aiding the demonic testing technique is an interference synthesis tool we have implemented based on SMT solving. The technique is shown to find errors in contracted versions of several benchmark applications.