Article ID Journal Published Year Pages File Type
429546 Journal of Computer and System Sciences 2015 30 Pages PDF
Abstract

•Probabilistic model checking for quantitative analysis of low-level OS primitives.•Combine measure-based analysis with formal modelling, spinlock protocol case study.•Report on challenges and methods, tackling state-explosion problem.

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.

Related Topics
Physical Sciences and Engineering Computer Science Computational Theory and Mathematics
Authors
, , , , , , , , ,