Locks: Picking key methods for a scalable quantitative analysis

Publikation: Beitrag in FachzeitschriftForschungsartikelBeigetragenBegutachtung

Abstract

Functional correctness of low-level operating-system (OS) code is an indispensable requirement. However, many applications rely also on quantitative aspects such as speed, energy efficiency, resilience with regards to errors and other cost factors. We report on our experiences of applying probabilistic model-checking techniques for analysing the quantitative long-run behaviour of low-level OS-code. Our approach, illustrated in a case study analysing a simple test-and-test-and-set (TTS) spinlock protocol, combines measure-based simulation with probabilistic model-checking to obtain high-level models of the performance of realistic systems and to tune the models to predict future system behaviour. We report how we obtained a nearly perfect match of analytic results and measurements and how we tackled the state-explosion problem to obtain model-checking results for a large number of processes where measurements are no longer feasible. These results gave us valuable insights in the delicate interplay between lock load, average spinning times and other performance measures.

Details

OriginalspracheEnglisch
Seiten (von - bis)258-287
Seitenumfang30
FachzeitschriftJournal of Computer and System Sciences
Jahrgang81
Ausgabenummer1
PublikationsstatusVeröffentlicht - 2015
Peer-Review-StatusJa

Externe IDs

Scopus 84908118232
ORCID /0000-0002-5321-9343/work/142236670
ORCID /0000-0003-1724-2586/work/165453577

Schlagworte

Ziele für nachhaltige Entwicklung

Schlagwörter

  • Measure-based quantitative analysis, Low-level operating system code, Test-and-test-and-set spinlock, Symmetry reduction, Probabilistic model checking, Conditional long-run probabilities, Quantile-based queries

Bibliotheksschlagworte