Automated Systematic Testing Methods for Multithreaded Programs

Loading...
Thumbnail Image
Journal Title
Journal ISSN
Volume Title
School of Science | Doctoral thesis (monograph) | Defence date: 2015-02-02
Checking the digitized thesis and permission for publishing
Instructions for the author
Date
2015
Major/Subject
Mcode
Degree programme
Language
en
Pages
161
Series
Aalto University publication series DOCTORAL DISSERTATIONS, 4/2015
Abstract
This thesis considers the problem of how the testing of multithreaded programs can be automated.One of the reasons multithreaded programs are difficult to test is that their behavior does not only depend on input values but also on how the executions of threads are interleaved. Typically this results in a number of possible executions through a multithreaded program that is so large that covering them all, even with the help of a computer, is infeasible. Fortunately it is often not necessary to test all combinations of input values and interleavings as many of them cause the program to behave in a similar way. This opens up the research question of how to automatically cover interesting properties of the program under test while trying to keep the number of test executions small.  This work studies how two different approaches, dynamic symbolic execution and net unfoldings, can be combined to automatically test multithreaded programs. Dynamic symbolic execution is a popular approach to automatically generate tests for sequential programs. Net unfoldings, on the other hand, can be used in verification of concurrent systems. The main contributions of this thesis fall under three categories. First, two net unfolding based approaches to systematically cover the local reachable states of threads are presented. Second, the thesis describes how global reachability properties, such as deadlock freedom, can be checked from an unfolding of a program. Third, a lightweight approach to capture abstract states of a multithreaded programs is presented. The method can be used to stop a test execution if it reaches an already covered abstract state.  To evaluate the new approaches, they are compared against an existing partial order reduction based testing algorithm. This is done by applying the algorithms to a number of multithreaded programs. Based on the results, the new algorithms are competitive against more traditional partial order reduction based methods and can in some cases outperform existing approaches by a considerable margin.

Säikeistettyjen ohjelmien testaus on usein haastavaa. Yksi syy tähän on se, että kyseisten ohjelmien käyttäytyminen ei riipu ainoastaan ohjelmalle annettavista syötteistä vaan myös siitä, miten ohjelman säikeiden suoritukset lomittuvat toisiinsa nähden. Tyypillisesti tämä tarkoittaa, että säikestetyn ohjelman suoritukset voivat poiketa toisistaan niin monilla eri tavoilla, että kaikkien suoritusmahdollisuuksien testaaminen ei ole mahdollista kohtuullisessa ajassa edes tietokoneen avustuksella. Onneksi useissa tapauksissa kaikkia syötearvojen ja säikeiden suoritusjärjestysten yhdistelmiä ei tarvitse erikseen testata. Tämä johtuu siitä, että tarkasteltava ohjelma toimii samankaltaisesti useilla kyseisillä yhdistelmillä. Tämä herättää tutkimuskysymyksen siitä, miten kiinnostavia ominaisuuksia säikestetystä ohjelmasta voidaan automaattisesti testata mahdollisimman pienellä testimäärällä.  Tässä työssä tutkitaan kuinka kaksi erillistä menetelmää, dynaaminen symbolinen suoritus ja verkkojen aukikerintä, voidaan yhdistää säikeistettyjen ohjelmien automaattiseksi testausmenetelmäksi. Dynaaminen symbolinen suoritus on suosittu menetelmä testien tuottamiseen yksisäikeisille ohjelmille automaattisesti. Verkkojen aukikerintä on puolestaan menetelmä rinnakkaisten järjestelmien tarkasteluun. Tässä työssä saavutetut tulokset voidaan jakaa korkealla tasolla kolmeen aihepiiriin. Ensimmäiseksi työssä esitetään kaksi verkkojen aukikerintään pohtautuvaa tapaa ohjelman säikeiden saavutettavien paikallisten tilojen systemaattiseen läpikäymiseen. Toiseksi, työssä kuvataan kuinka saavutettavien yhteistilojen ominaisuuksia, kuten säikeiden lukkiutumisia, voidaan etsiä ohjelman unfolding-esityksestä. Kolmanneksi, työssä esitellään säikeisettyjen ohjelmien tilojen vertailumenetelmä, joka perustuu abstraktien tilojen tallentamiseen. Menetelmää voidaan käyttää testiajojen katkaisemiseen silloin, kun testiajo päätyy jo aiemmin tutkittuun abstraktiin tilaan.  Työssä esitettyjen uusien testausalgoritmien arvioimiseksi niitä vertaillaan aiempaan osittaisjärjestysreduktioon pohjautuvaan algoritmiin. Tätä varten kyseisiä algoritmeja käytetään usean säikeistetyn ohjelman testaamiseen. Kokeellisten tulosten perusteella tässä työssä esitetyt menetelmät ovat kilpailukykyisiä perinteisempiin algoritmeihin verrattuna. Joissain tapauksissa uudet menetelmät ovat huomattavasti vanhoja tehokkaampia.
Description
Supervising professor
Heljanko, Keijo, Assoc. Prof., Aalto University, Department of Computer Science, Finland
Thesis advisor
Heljanko, Keijo, Assoc. Prof., Aalto University, Department of Computer Science, Finland
Keywords
dynamic symbolic execution, unfoldings, automated testing, partial order reduction, dynaaminen symbolinen suoritus, verkkojen aukikerintä, automaattinen testaus, osittaisjärjestysreduktio
Other note
Citation