Concrete and symbolic linearisability checking of non-blocking concurrent data structures
Date
2021-12
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Stellenbosch : Stellenbosch University
Abstract
ENGLISH ABSTRACT: Non-blocking concurrent data structures are developed as a more efficient solution to concurrent
data structures; in non-blocking concurrent data structures hardware-level atomic instructions are
used instead of higher-level, expensive locking mechanisms. Lock-free algorithms, however, are
notoriously hard to design and prone to subtle concurrency errors that are difficult to pick up.
Linearisability Checking is the standard correctness condition for non-blocking concurrent data
structures; a data structure is linearisable if each concurrent execution of the data structure corresponds
to the execution of its correct sequential specification.
In this thesis, the focus is on the linearisability checking of non-blocking data structures using a
model checker. The approaches for checking linearisability using a model checker can be broadly
categorised into linearisation point and automatic linearisability checking. The state-of-the-art
strategies were implemented using the Java PathFinder Model Checker as basis. The linearisation
point linearisability checking strategy of Vechev et al. was extended to include data structures with
operations that act generically on the data structure, and not just on one element in the data structure.
An improved version of Doolan et al.’s external automatic checker was implemented and the
idea of an external checker was extended to the improved linearisation point checking strategy. The
lazy read optimisation, proposed by Long et al., and a hash optimisation, proposed in this thesis,
for the automatic checker was implemented and the effectiveness and benefit of the optimisations
determined. The performance-limiting factor of the automatic checker was investigated and the
claims made by Vechev et al., Liu et al., and Doolan et al. confirmed/falsified.
The concrete checker’s usefulness in finding linearisability errors is constrained by the user’s ability
to hand-craft test cases in which errors are present. A new Symbolic Linearisability Checker
was developed, the major novel contribution in this thesis, that integrates linearisability checking
into Symbolic PathFinder, a symbolic model checker. The symbolic checker performs linearisability
checking on all possible test cases and program paths; it verifies the linearisability of a data structure
in general, constrained only by a user-defined number of operations to be executed by each thread.
Finally, extensive evaluations and comparisons of all checkers were performed, on the same model
checking framework and hardware, considering their manual input required, resource usage, scalability,
and ability to find errors.
AFRIKAANSE OPSOMMING: Nie-blokkerende gelyklopende data strukture is ’n meer effektiewe oplossing as data strukture wat blokkeringsmeganismes gebruik; in nie-blokkerende data strukture word atomiese hardewareinstruksies gebruik in plaas van duur, ho¨er vlak, blokkeringsmeganismes. Nie-blokkerende gelyklopende data strukture is egter ingewikkeld, en is geneig om subtiele gelyklopende foute in te hˆe wat moeilik is om op te spoor. Lineˆeriseerbaarheid is die standaard korrektheidskondisie vir nieblokkerende gelyklopende data strukture; ’n data struktuur is lineˆeriseerbaar as elke uitvoering van die data struktuur ooreenstem met die uitvoering van sy korrekte sekwensi¨ele spesifikasie. Die tesis fokus op die verifikasie van lineˆeriseerbaarheid van nie-blokkerende data strukture deur gebruik te maak van ’n modeltoetser. Die metodes vir die verifikosie van lineˆeriseerbaarheid deur gebruik te maak van ’n modeltoetser kan breedweg gekattegoriseer word in lineˆerisasie-punt en outomatiese lineˆerisasie toetsing. Die jongste tegnieke is implementeer deur gebruik te maak van die Java PathFinder modeltoetser as basis. Die lineˆerisasie-punt lineˆeriseerbaarheids toetsstrategie¨e van Vechev et alis uitgebrei om data strukture wat generiese operasies op die data struktuur uitvoer in plaas van op ’n spesifieke element in die data struktuur, in te sluit. ’n Gevorderde weergawe van Doolan et al. se eksterne outomatiese toetser is ge¨ımplementeer en die idee van ’n eksterne implementasie is gebruik om ook ’n eksterne weergawe van die verbeterde lineˆerisasie-punt toetsstrategie te implementeer. Die lui-lees optimering wat deur Long et al. voorgestel is, en ’n hutsstrategie optimering wat in die tesis voorgestel word, is vir die outomatiese toetser ge¨ımplementeer en die effektiwiteit en voordele van die optimerings is bepaal. Die faktore wat die effektiwiteit van die outomatiese toetser beperk is ondersoek en die stellings wat deur Vechev et al., Liu et al., en Doolan et al. gemaak is, is verifieer. Die konkrete toetser se bruikbaarheid vir die vind van lineˆeriseringsfoute word beperk deur die gebruiker se vermo¨e om toevoergevalle wat foute sal uitwys, op te stel. ’n Nuwe simboliese lineˆerisasie toetser is ontwikkel, ’n groot bydrae van die tesis, wat lineˆerisasie toetsing in die simboliese PathFinder, ’n simboliese modeltoetser, integreer. Die simboliese toetser voer toetsing uit op al die moontlike toevoergevalle en al die moontlike paaie; dit verifieer dus die lineˆeriseerbaarheid van ’n data struktuur vir algemene gevalle, en word slegs beperk deur die gebruikersgespesifiseerde aantal operasies per liggewigproses.
AFRIKAANSE OPSOMMING: Nie-blokkerende gelyklopende data strukture is ’n meer effektiewe oplossing as data strukture wat blokkeringsmeganismes gebruik; in nie-blokkerende data strukture word atomiese hardewareinstruksies gebruik in plaas van duur, ho¨er vlak, blokkeringsmeganismes. Nie-blokkerende gelyklopende data strukture is egter ingewikkeld, en is geneig om subtiele gelyklopende foute in te hˆe wat moeilik is om op te spoor. Lineˆeriseerbaarheid is die standaard korrektheidskondisie vir nieblokkerende gelyklopende data strukture; ’n data struktuur is lineˆeriseerbaar as elke uitvoering van die data struktuur ooreenstem met die uitvoering van sy korrekte sekwensi¨ele spesifikasie. Die tesis fokus op die verifikasie van lineˆeriseerbaarheid van nie-blokkerende data strukture deur gebruik te maak van ’n modeltoetser. Die metodes vir die verifikosie van lineˆeriseerbaarheid deur gebruik te maak van ’n modeltoetser kan breedweg gekattegoriseer word in lineˆerisasie-punt en outomatiese lineˆerisasie toetsing. Die jongste tegnieke is implementeer deur gebruik te maak van die Java PathFinder modeltoetser as basis. Die lineˆerisasie-punt lineˆeriseerbaarheids toetsstrategie¨e van Vechev et alis uitgebrei om data strukture wat generiese operasies op die data struktuur uitvoer in plaas van op ’n spesifieke element in die data struktuur, in te sluit. ’n Gevorderde weergawe van Doolan et al. se eksterne outomatiese toetser is ge¨ımplementeer en die idee van ’n eksterne implementasie is gebruik om ook ’n eksterne weergawe van die verbeterde lineˆerisasie-punt toetsstrategie te implementeer. Die lui-lees optimering wat deur Long et al. voorgestel is, en ’n hutsstrategie optimering wat in die tesis voorgestel word, is vir die outomatiese toetser ge¨ımplementeer en die effektiwiteit en voordele van die optimerings is bepaal. Die faktore wat die effektiwiteit van die outomatiese toetser beperk is ondersoek en die stellings wat deur Vechev et al., Liu et al., en Doolan et al. gemaak is, is verifieer. Die konkrete toetser se bruikbaarheid vir die vind van lineˆeriseringsfoute word beperk deur die gebruiker se vermo¨e om toevoergevalle wat foute sal uitwys, op te stel. ’n Nuwe simboliese lineˆerisasie toetser is ontwikkel, ’n groot bydrae van die tesis, wat lineˆerisasie toetsing in die simboliese PathFinder, ’n simboliese modeltoetser, integreer. Die simboliese toetser voer toetsing uit op al die moontlike toevoergevalle en al die moontlike paaie; dit verifieer dus die lineˆeriseerbaarheid van ’n data struktuur vir algemene gevalle, en word slegs beperk deur die gebruikersgespesifiseerde aantal operasies per liggewigproses.
Description
Thesis (MSc)--Stellenbosch University, 2021
Keywords
Linearisability checking, Model checking (Computer science), Program verification, Computer multitasking, Data structures (Computer science) -- Linearizability, Linearizability checking, Computer programs -- Correctness, UCTD