Effektiva testningstekniker för att hitta samtidighetsrelaterade fel i mjukvara

Tidsperiod:

1 januari 2018 – 31 december 2021

Projektledare:

KONSTANTINOS SAGONAS

Finansiär:

Vetenskapsrådet

Bidragstyp:

Projektbidrag

Budget:

3 580 000 SEK

Mjukvara som utnyttjar "samtidighet" (eng. concurrency) har flera exekveringstrådar som kan köra samtidigt. Sådan mjukvara finns så gott som överallt idag och användingen kommer troligtvis öka på grund av flera orsaker. En av huvudorsakerna till ökad användning av samtidighet är utvecklingen av processorer med flera kärnor som gör det möjligt att köra flera exekveringstrådar parallellt. Flerkärniga processorer har utvecklas för att kunna tillhandahålla mer datorkraft och samtidigt hålla energiförbrukningen låg. Det är inte ovanligt med mobiltelefoner som har processorer med flera processorkärnor idag och utvecklingen pekar på att vanliga processorer kommer innehålla ännu fler kärnor inom några år. För att utnyttja den fulla potentialen av dessa processorer krävs program som använder samtidighet. En annan orsak till den ökande användningen av datorprogram med samtidighet är programspråk såsom Erlang, Go, Rust och Scala som alla har kraftfulla abstraktioner för att hantera samtidighet. Dessa abstraktioner har även börjat leta sig in i traditionella programspråk såsom Python och C#.Användning av samtidighet passar många typer av program och är nödvändigt för att utnyttja den fulla potentialen i dagens och framtidens processorer, men samtidiga program har fler felkällor än sekventiella program på grund av den stora mängden sätt exekveringstrådar kan samverka med varandra. Hur exekveringstrådar samverkar med varandra påverkas bland annat av hur de schemaläggs av operativsystemet och varierar mellan programkörningar. Detta kan göra det svårt även för experter på området att skriva felfria program och hitta alla fel innan programmet börjar användas. Vanlig testning som används för sekventiella program fungerar inte eftersom sådan testning inte hittar Heisenbuggar, fel som bara inträffar med en viss ovanlig samverkan mellan exekveringstrådar. En ytterligare svårighet är att de "svaga minesmodeller" som används i moderna processorer gör det möjligt för olika exekveringstrådar att se samma förändringar i datorns minne ske i olika ordningar. Allt detta gör att det ofta är svårt att producera felfri mjukvara som använder samtidighet. Vi planerar att beskriva, formalisera, implementera och utvärdera nya testtekniker för program som använder samtidighet och som behöves för att kunna testa större program som använder samtidighet. Vi ska även utöka nuvarande verifieringstekniker så att de effektivt kan testa program som använder moderna abstraktioner för samtidighet. Utöver det ska vi formalisera programsemantik och kriterier för korrekthet under svaga minnesmodeller, vilket kan hjälpa framtida programspråksdesign. Slutligen så planerar vi att implementera praktiskt användbara verktyg för testning av mjukvara som använder samtidighet. För att göra allt detta kommer vi använda oss av erfarenhet från att ha utvecklat testningsverktyg för systematisk testning av program skrivna i Erlang och C (med pthreads). Vi kommer att utöka och förbättra dessa verktyg både för att markant förenkla utvecklingen av program som använder samtidighet för professionella utvecklare och för att bidra till den vetenskapliga forskningen på området.