Symbolic Methods for Transducers and Testing

Loading...
Thumbnail Image
Journal Title
Journal ISSN
Volume Title
School of Science | Doctoral thesis (article-based) | Defence date: 2018-02-16
Date
2017
Major/Subject
Mcode
Degree programme
Language
en
Pages
81 + app. 111
Series
Aalto University publication series DOCTORAL DISSERTATIONS, 255/2017
Abstract
Symbolic methods reason about groups of values. The evolution of modern satisfiability modulo theories (SMT) solvers has enabled an increasing variety of symbolic applications that require efficient reasoning in rich logics, such as bit vectors and arrays. SMT solvers remove barriers for employing solver technology in the development of symbolic methods. This dissertation contributes applications of symbolic methods in the areas of stream processing, test generation and software verification.Symbolic automata and transducers are generalizations of their respective classical models that shift reasoning about inputs to an SMT solver, which allows efficient use of very large alphabets. In the areas of stream processing and Big Data analytics, it is desirable to be able to represent computations as pipelines of modular processing stages. Pipelines represented as symbolic transducers can be efficiently fused into a single stage, which reduces communication overhead and enables further reductions.This dissertation presents a tool that applies fusion to pipelines of symbolic transducers specified in a variety of frontend languages. Fusion is supported by further reductions based on reachability analysis and automata minimization. The tool generates efficient fused code, which is shown to provide comparable performance to a sample of real-world, hand-optimized, monolithic code, as well as greater performance than alternative methods of composing modular pipelines of stream computations.Concolic testing is a popular approach for implementing symbolic execution, which commonly uses SMT solvers to efficiently generate test inputs. The Dash algorithm combines concolic testing with a predicate abstraction. This dissertation presents an implementation of Dash for automati- cally verifying sequential C programs on the LLVM compiler framework. A refinement strategy for the LLVM intermediate representation is presented and design considerations for reducing memory usage and improving verification performance are discussed. The resulting tool LCTD shows competitive results on a set of benchmarks drawn from SV-COMP.Partial order reduction is an approach for exploring reduced sets of interleavings between threads in a multi-threaded program. This dissertation presents an improvement to the dynamic partial order reduction (DPOR) algorithm, which exploits the commutativity of read operations to enable more reduction. The new algorithm DPOR-CR is shown to explore significantly fewer tests. Furthermore, a proof is presented that data races can be cheaply checked for during DPOR.

Symboliset metodit päättelevät joukoilla arvoja. Modernien satisfiability modulo theories (SMT) -ratkaisimien evoluutio on mahdollistanut kasvavan valikoiman symbolisia sovelluksia, jotka vaativat päättelyä rikkailla logiikoilla, kuten bittivektoreilla ja taulukoilla. SMT-ratkaisimet helpottavat ratkaisinteknologian käyttöä symbolisten metodien kehityksessä. Tämä väitöskirja edistää symbolisten metodien sovelluksia tietovirtojen käsittelyssä, testien generoinnissa ja ohjelmistojen verifioinnissa.Symboliset automaatit ja muuntimet ovat vastaavien klassisten mallien yleistyksiä, jotka siirtävät syötteisiin liittyvää päättelyä SMT-ratkaisimelle, mikä mahdollistaa erittäin suurten aakkostojen tehokkaan käytön. Tietovirtojen käsittelyssä ja suuren datan analytiikassa on hyödyllistä pystyä esittämään laskentaa sarjana modulaarisia vaiheita. Sarjana symbolisia muuntimia esitetty ohjelma on mahdollista tehokkaasti yhdistää yhdeksi vaiheeksi, mikä vähentää ylimääräistä kommunikaatiota. Tätä kutsutaan fuusioksi. Lisäksi näin yhdistettyjä muuntimia voidaan edelleen supistaa.Tämä väitöskirja esittelee työkalun, joka soveltaa fuusiota erinäisillä ohjelmointikielillä esitettyjen symbolisien muuntimien sarjoista koostuviin ohjelmiin. Fuusiota täydentävät saavutettavuusanalyysiin ja automaattien minimointiin perustuvat supistusmenetelmät. Työkalu tuottaa tehokasta koodia, jonka näytetään olevan suorituskyvyltään vertailukelpoista näytteeseen käsin optimoitua ei-modulaarista koodia, sekä tehokkaampaa kuin vaihtoehtoisilla menetelmillä fuusioidut ohjelmat.Dynaaminen symbolinen suoritus käyttää SMT-ratkaisimia generoidakseen tehokkaasti syötteitä testaukseen. Dash-algoritmi yhdistää dynaamisen symbolisen suorituksen ja predikaattiabstraktion. Tämä väitöskirja esittelee LLVM kääntäjäkirjastoa käyttävän toteutuksen Dash-algoritmista C-ohjelmien automaattista verifiointia varten. Tämä sisältää selityksen siitä, miten Dash-algoritmi toteutetaan LLVM:n välikielelle, sekä tavan parantaa verifoinnin suorituskykyä. Toteutettu työkalu LCTD on kilpailukykyinen vertailtuna joukolla SV-COMP-kilpailusta haettuja ohjelmia.Osittaisjärjestysreduktio on lähestymistapa, jolla voidaan käydä läpi supistettuja joukkoja rinnakkaisten ohjelmien testisuorituksia menettämättä virheiden saavutettavuutta. Tämä väitöskirja esittelee uuden version dynaamisesta osittaisjärjestysreduktiosta (DPOR), joka mahdollistaa lukuoperaatioiden kommutatiivisuuden hyödyntämisen. Uuden algoritmin DPOR-CR:n näytetään käyvän läpi huomattavasti vähemmän testisuorituksia kuin alkuperäinen. Lisäksi todistetaan, että synkronoimaton jaetun muistin käyttö voidaan tarkistaa edullisesti DPOR:n aikana.
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
symbolic methods, symbolic transducers, stream processing, stream fusion, test generation, software verification, partial order reduction, race detection, symboliset metodit, symboliset muuntimet, tietovirtojen prosessointi, tietovirtojen fuusio, testigenerointi, ohjelmistojen verifiointi, osittaisjärjestysreduktio
Other note
Parts
  • [Publication 1]: Olli Saarikivi, Margus Veanes, Todd Mytkowicz, Madan Musuvathi. Fusing effectful comprehensions. In Proceedings of the 38th Conference on Programming Language Design and Implementation (PLDI 2017), pages 17–32. June 2017.
    DOI: 10.1145/3062341.3062362 View at publisher
  • [Publication 2]: Olli Saarikivi, Margus Veanes. Minimization of symbolic transducers. In Proceedings of the 29th International Conference on Computer Aided Verification (CAV 2017), Part II, LNCS 10427, pages 176–196. July 2017.
    DOI: 10.1007/978-3-319-63390-9_10 View at publisher
  • [Publication 3]: Olli Saarikivi, Margus Veanes. Translating C# to branching symbolic transducers. In 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-21), Short Presentations, pages 86–99, May 2017.
  • [Publication 4]: Olli Saarikivi, Keijo Heljanko. LCTD: test-guided proofs for C programs on LLVM. Journal of Logic and Algebraic Methods in Programming (JLAMP), 85(6), pages 1292–1317. October 2016.
    DOI: 10.1016/j.jlamp.2015.10.010 View at publisher
  • [Publication 5]: Olli Saarikivi, Kari Kahkonen, Keijo Heljanko. Improving dynamic partial order reductions for concolic testing. In Proceedings of the 12th International Conference on Application of Concurrency to System Design (ACSD 2012), pages 132–141. June2012.
    DOI: 10.1109/ACSD.2012.18 View at publisher
  • [Publication 6]: Olli Saarikivi, Keijo Heljanko. Reporting races in dynamic partial order reduction. In Proceedings of NASA Formal Methods - 7th International Symposium (NFM 2015), LNCS 9058, pages 450–456, April 2015.
    DOI: 10.1007/978-3-319-17524-9_35 View at publisher
Citation